helm/ocaml/cic_transformations/tacticAst2Box.ml

   1 (* Copyright (C) 2004, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 (**************************************************************************)
  27 (*                                                                        *)
  28 (*                           PROJECT HELM                                 *)
  29 (*                                                                        *)
  30 (*                Andrea Asperti <asperti@cs.unibo.it>                    *)
  31 (*                             18/2/2004                                  *)
  32 (*                                                                        *)
  33 (**************************************************************************)
  34
  35
  36 open Ast2pres
  37 open TacticAst
  38
  39 let rec count_tactic current_size tac =
  40   if current_size > maxsize then current_size
  41   else match tac with
  42     | Absurd (_, term) -> countterm (current_size + 6) term
  43     | Apply (_, term) -> countterm (current_size + 6) term
  44     | Auto _ -> current_size + 4
  45     | Assumption _ -> current_size + 10
  46     | Change (_, t1, t2, where) ->
  47         let size1 = countterm (current_size + 12) t1 in (* change, with *)
  48         let size2 = countterm size1 t2 in
  49         (match where with
  50              None -> size2
  51            | Some ident -> size2 + 3 + String.length ident)
  52     | Change_pattern _ -> assert false  (* TODO *)
  53     | Contradiction _ -> current_size + 13
  54     | Cut (_, term) -> countterm (current_size + 4) term
  55     | Decompose (_, ident, principles) ->
  56         List.fold_left
  57           (fun size s -> size + (String.length s))
  58           (current_size + 11 + String.length ident) principles
  59     | Discriminate (_, ident) -> current_size + 12 + (String.length ident)
  60     | Elim (_, term, using) ->
  61         let size1 = countterm (current_size + 5) term in
  62           (match using with
  63            None -> size1
  64              | Some term -> countterm (size1 + 7) term)
  65     | ElimType (_, term) -> countterm (current_size + 10) term
  66     | Exact (_, term) -> countterm (current_size + 6) term
  67     | Exists _ -> current_size + 6
  68     | Fold (_, kind, term) ->
  69         countterm (current_size + 5) term
  70     | Fourier _ -> current_size + 7
  71     | Goal (_, n) -> current_size + 4 + int_of_float (ceil (log10 (float n)))
  72     | Injection (_, ident) -> current_size + 10 + (String.length ident)
  73     | Intros (_, num, idents) ->
  74         List.fold_left
  75           (fun size s -> size + (String.length s))
  76           (current_size + 7) idents
  77     | Left _ -> current_size + 4
  78     | LetIn (_, term, ident) ->
  79         countterm (current_size + 5 + String.length ident) term
  80     | Reduce _ -> assert false  (* TODO *)
  81     | Reflexivity _ -> current_size + 11
  82     | Replace (_, t1, t2) ->
  83         let size1 = countterm (current_size + 14) t1 in (* replace, with *)
  84           countterm size1 t2
  85     | Replace_pattern _ -> assert false  (* TODO *)
  86     | Rewrite _ -> assert false (* TODO *)
  87     | Right _ -> current_size + 5
  88     | Ring _ -> current_size + 4
  89     | Split _ -> current_size + 5
  90     | Symmetry _ -> current_size + 8
  91     | Transitivity (_, term) ->
  92         countterm (current_size + 13) term
  93 ;;
  94
  95 let is_big_tac tac =
  96   let n = (count_tactic 0 tac) in
  97 (*   prerr_endline ("Lunghezza: " ^ (string_of_int n)); *)
  98   n > maxsize
  99 ;;
 100
 101 (* prova *)
 102 let rec small_tactic2box tac =
 103   Box.Text([], TacticAstPp.pp_tactic tac)
 104
 105 let string_of_kind = function
 106   | `Reduce -> "reduce"
 107   | `Simpl -> "simplify"
 108   | `Whd -> "whd"
 109   | `Normalize -> "normalize"
 110
 111 let dummy_tbl = Hashtbl.create 0
 112
 113 let ast2astBox ast = Ast2pres.ast2astBox (ast, dummy_tbl)
 114
 115 let pretty_append l ast =
 116   if is_big ast then
 117     [Box.H([],l);
 118      Box.H([],[Box.skip; ast2astBox ast])]
 119   else
 120     [Box.H([],l@[Box.smallskip; ast2astBox ast])]
 121
 122 let rec tactic2box tac =
 123   if (is_big_tac tac) then
 124     big_tactic2box tac
 125   else
 126     small_tactic2box tac
 127
 128 and big_tactic2box = function
 129   | Absurd (_, term) ->
 130       Box.V([],[Box.Text([],"absurd");
 131                 ast2astBox term])
 132   | Apply (_, term) ->
 133       Box.V([],[Box.Text([],"apply");
 134                 ast2astBox term])
 135   | Assumption _ -> Box.Text([],"assumption")
 136   | Auto _ -> Box.Text([],"auto")
 137   | Change (_, t1, t2, where) ->
 138       let where =
 139         (match where with
 140              None -> []
 141            | Some ident ->
 142                [Box.Text([],"in");
 143                 Box.smallskip;
 144                 Box.Text([],ident)]) in
 145         Box.V([],
 146               (pretty_append
 147                  [Box.Text([],"change")]
 148                  t1)@
 149               (pretty_append
 150                  [Box.Text([],"with")]
 151                  t2)@where)
 152   | Change_pattern _ -> assert false  (* TODO *)
 153   | Contradiction _ -> Box.Text([],"contradiction")
 154   | Cut (_, term) ->
 155       Box.V([],[Box.Text([],"cut");
 156                 Box.indent(ast2astBox term)])
 157   | Decompose (_, ident, principles) ->
 158       let principles =
 159         List.map (fun x -> Box.Text([],x)) principles in
 160       Box.V([],[Box.Text([],"decompose");
 161                 Box.H([],[Box.Text([],"[");
 162                           Box.V([],principles);
 163                           Box.Text([],"]")]);
 164                 Box.Text([],ident)])
 165   | Discriminate (_, ident) ->
 166       Box.V([],[Box.Text([],"discriminate");
 167                 Box.Text([],ident)])
 168   | Elim (_, term, using) ->
 169       let using =
 170         (match using with
 171              None -> []
 172            | Some term ->
 173                (pretty_append
 174                   [Box.Text([],"using")]
 175                   term)) in
 176       Box.V([],
 177             (pretty_append
 178                [Box.Text([],"elim")]
 179                term)@using)
 180   | ElimType (_, term) ->
 181       Box.V([],[Box.Text([],"elim type");
 182                 Box.indent(ast2astBox term)])
 183   | Exact (_, term) ->
 184       Box.V([],[Box.Text([],"exact");
 185                 Box.indent(ast2astBox term)])
 186   | Exists _ -> Box.Text([],"exists")
 187   | Fold (_, kind, term) ->
 188       Box.V([],[Box.H([],[Box.Text([],"fold");
 189                           Box.smallskip;
 190                           Box.Text([],string_of_kind kind)]);
 191                 Box.indent(ast2astBox term)])
 192   | Fourier _ -> Box.Text([],"fourier")
 193   | Goal (_, n) -> Box.Text([],"goal " ^ string_of_int n)
 194   | Injection (_, ident) ->
 195       Box.V([],[Box.Text([],"transitivity");
 196                 Box.indent (Box.Text([],ident))])
 197   | Intros (_, num, idents) ->
 198       let num =
 199         (match num with
 200              None -> []
 201            | Some num -> [Box.Text([],string_of_int num)]) in
 202       let idents =
 203         List.map (fun x -> Box.Text([],x)) idents in
 204       Box.V([],[Box.Text([],"decompose");
 205                 Box.H([],[Box.smallskip;
 206                           Box.V([],idents)])])
 207   | Left _ -> Box.Text([],"left")
 208   | LetIn (_, term, ident) ->
 209       Box.V([],[Box.H([],[Box.Text([],"let");
 210                           Box.smallskip;
 211                           Box.Text([],ident);
 212                           Box.smallskip;
 213                           Box.Text([],"=")]);
 214                 Box.indent (ast2astBox term)])
 215   | Reduce _ -> assert false  (* TODO *)
 216   | Reflexivity _ -> Box.Text([],"reflexivity")
 217   | Replace (_, t1, t2) ->
 218       Box.V([],
 219             (pretty_append
 220                [Box.Text([],"replace")]
 221                t1)@
 222             (pretty_append
 223                [Box.Text([],"with")]
 224                t2))
 225   | Replace_pattern _ -> assert false  (* TODO *)
 226   | Rewrite _ -> assert false (* TODO *)
 227   | Right _ -> Box.Text([],"right")
 228   | Ring _ ->  Box.Text([],"ring")
 229   | Split _ -> Box.Text([],"split")
 230   | Symmetry _ -> Box.Text([],"symmetry")
 231   | Transitivity (_, term) ->
 232       Box.V([],[Box.Text([],"transitivity");
 233                 Box.indent (ast2astBox term)])
 234 ;;
 235
 236 open TacticAst
 237
 238 let rec tactical2box = function
 239   | Tactic (_, tac) -> tactic2box tac
 240 (*
 241   | Command cmd -> (* TODO dummy implementation *)
 242       Box.Text([], TacticAstPp.pp_tactical (Command cmd))
 243 *)
 244
 245   | Fail _ -> Box.Text([],"fail")
 246   | Do (_, count, tac) ->
 247       Box.V([],[Box.Text([],"do " ^ string_of_int count);
 248                 Box.indent (tactical2box tac)])
 249   | IdTac _ -> Box.Text([],"id")
 250   | Repeat (_, tac) ->
 251       Box.V([],[Box.Text([],"repeat");
 252                 Box.indent (tactical2box tac)])
 253   | Seq (_, tacs) ->
 254       Box.V([],tacticals2box tacs)
 255   | Then (_, tac, tacs) ->
 256       Box.V([],[tactical2box tac;
 257                 Box.H([],[Box.skip;
 258                           Box.Text([],"[");
 259                           Box.V([],tacticals2box tacs);
 260                           Box.Text([],"]");])])
 261   | Tries (_, tacs) ->
 262       Box.V([],[Box.Text([],"try");
 263                 Box.H([],[Box.skip;
 264                           Box.Text([],"[");
 265                           Box.V([],tacticals2box tacs);
 266                           Box.Text([],"]");])])
 267   | Try (_, tac) ->
 268       Box.V([],[Box.Text([],"try");
 269                 Box.indent (tactical2box tac)])
 270
 271 and tacticals2box tacs =
 272   List.map
 273     (function tac -> Box.H([],[tactical2box tac; Box.Text([],";")])) tacs
 274 ;;
 275
 276 let tacticalPp tac =
 277   String.concat "\n"
 278     (BoxPp.to_string CicAstPp.pp_term (tactical2box tac));;
 279
 280