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       LocatedTactic (_, tac) -> count_tactic current_size tac
  43     | Absurd term -> countterm (current_size + 6) term
  44     | Apply term -> countterm (current_size + 6) term
  45     | Auto -> current_size + 4
  46     | Assumption -> current_size + 10
  47     | Change (t1, t2, where) ->
  48         let size1 = countterm (current_size + 12) t1 in (* change, with *)
  49         let size2 = countterm size1 t2 in
  50         (match where with
  51              None -> size2
  52            | Some ident -> size2 + 3 + String.length ident)
  53     | Change_pattern (_, _, _) -> assert false  (* TODO *)
  54     | Contradiction -> current_size + 13
  55     | Cut term -> countterm (current_size + 4) term
  56     | Decompose (ident, principles) ->
  57         List.fold_left
  58           (fun size s -> size + (String.length s))
  59           (current_size + 11 + String.length ident) principles
  60     | Discriminate ident -> current_size + 12 + (String.length ident)
  61     | Elim (term, using) ->
  62         let size1 = countterm (current_size + 5) term in
  63           (match using with
  64            None -> size1
  65              | Some term -> countterm (size1 + 7) term)
  66     | ElimType term -> countterm (current_size + 10) term
  67     | Exact term -> countterm (current_size + 6) term
  68     | Exists -> current_size + 6
  69     | Fold (kind, term) ->
  70         countterm (current_size + 5) term
  71     | Fourier -> current_size + 7
  72     | Hint -> current_size + 4
  73     | Injection ident -> current_size + 10 + (String.length ident)
  74     | Intros (num, idents) ->
  75         List.fold_left
  76           (fun size s -> size + (String.length s))
  77           (current_size + 7) idents
  78     | Left -> current_size + 4
  79     | LetIn (term, ident) ->
  80         countterm (current_size + 5 + String.length ident) term
  81     | Reduce (_, _) -> assert false  (* TODO *)
  82     | Reflexivity -> current_size + 11
  83     | Replace (t1, t2) ->
  84         let size1 = countterm (current_size + 14) t1 in (* replace, with *)
  85           countterm size1 t2
  86     | Replace_pattern (_, _) -> assert false  (* TODO *)
  87     | Rewrite (_, _, _) -> assert false (* TODO *)
  88     | Right -> current_size + 5
  89     | Ring -> current_size + 4
  90     | Split -> current_size + 5
  91     | Symmetry -> current_size + 8
  92     | Transitivity term ->
  93         countterm (current_size + 13) term
  94 ;;
  95
  96 let is_big_tac tac =
  97   let n = (count_tactic 0 tac) in
  98 (*   prerr_endline ("Lunghezza: " ^ (string_of_int n)); *)
  99   n > maxsize
 100 ;;
 101
 102 (* prova *)
 103 let rec small_tactic2box tac =
 104   Box.Text([], TacticAstPp.pp_tactic tac)
 105
 106 let string_of_kind = function
 107   | `Reduce -> "reduce"
 108   | `Simpl -> "simplify"
 109   | `Whd -> "whd"
 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     LocatedTactic (loc, tac) ->
 130       big_tactic2box tac
 131   | Absurd term ->
 132       Box.V([],[Box.Text([],"absurd");
 133                 ast2astBox term])
 134   | Apply term ->
 135       Box.V([],[Box.Text([],"apply");
 136                 ast2astBox term])
 137   | Assumption -> Box.Text([],"assumption")
 138   | Auto -> Box.Text([],"auto")
 139   | Change (t1, t2, where) ->
 140       let where =
 141         (match where with
 142              None -> []
 143            | Some ident ->
 144                [Box.Text([],"in");
 145                 Box.smallskip;
 146                 Box.Text([],ident)]) in
 147         Box.V([],
 148               (pretty_append
 149                  [Box.Text([],"change")]
 150                  t1)@
 151               (pretty_append
 152                  [Box.Text([],"with")]
 153                  t2)@where)
 154   | Change_pattern (_, _, _) -> assert false  (* TODO *)
 155   | Contradiction -> Box.Text([],"contradiction")
 156   | Cut term ->
 157       Box.V([],[Box.Text([],"cut");
 158                 Box.indent(ast2astBox term)])
 159   | Decompose (ident, principles) ->
 160       let principles =
 161         List.map (fun x -> Box.Text([],x)) principles in
 162       Box.V([],[Box.Text([],"decompose");
 163                 Box.H([],[Box.Text([],"[");
 164                           Box.V([],principles);
 165                           Box.Text([],"]")]);
 166                 Box.Text([],ident)])
 167   | Discriminate ident ->
 168       Box.V([],[Box.Text([],"discriminate");
 169                 Box.Text([],ident)])
 170   | Elim (term, using) ->
 171       let using =
 172         (match using with
 173              None -> []
 174            | Some term ->
 175                (pretty_append
 176                   [Box.Text([],"using")]
 177                   term)) in
 178       Box.V([],
 179             (pretty_append
 180                [Box.Text([],"elim")]
 181                term)@using)
 182   | ElimType term ->
 183       Box.V([],[Box.Text([],"elim type");
 184                 Box.indent(ast2astBox term)])
 185   | Exact term ->
 186       Box.V([],[Box.Text([],"exact");
 187                 Box.indent(ast2astBox term)])
 188   | Exists -> Box.Text([],"exists")
 189   | Fold (kind, term) ->
 190       Box.V([],[Box.H([],[Box.Text([],"fold");
 191                           Box.smallskip;
 192                           Box.Text([],string_of_kind kind)]);
 193                 Box.indent(ast2astBox term)])
 194   | Fourier -> Box.Text([],"fourier")
 195   | Hint -> Box.Text([],"hint")
 196   | Injection ident ->
 197       Box.V([],[Box.Text([],"transitivity");
 198                 Box.indent (Box.Text([],ident))])
 199   | Intros (num, idents) ->
 200       let num =
 201         (match num with
 202              None -> []
 203            | Some num -> [Box.Text([],string_of_int num)]) in
 204       let idents =
 205         List.map (fun x -> Box.Text([],x)) idents in
 206       Box.V([],[Box.Text([],"decompose");
 207                 Box.H([],[Box.smallskip;
 208                           Box.V([],idents)])])
 209   | Left -> Box.Text([],"left")
 210   | LetIn (term, ident) ->
 211       Box.V([],[Box.H([],[Box.Text([],"let");
 212                           Box.smallskip;
 213                           Box.Text([],ident);
 214                           Box.smallskip;
 215                           Box.Text([],"=")]);
 216                 Box.indent (ast2astBox term)])
 217   | Reduce (_, _) -> assert false  (* TODO *)
 218   | Reflexivity -> Box.Text([],"reflexivity")
 219   | Replace (t1, t2) ->
 220       Box.V([],
 221             (pretty_append
 222                [Box.Text([],"replace")]
 223                t1)@
 224             (pretty_append
 225                [Box.Text([],"with")]
 226                t2))
 227   | Replace_pattern (_, _) -> assert false  (* TODO *)
 228   | Rewrite (_, _, _) -> assert false (* TODO *)
 229   | Right -> Box.Text([],"right")
 230   | Ring ->  Box.Text([],"ring")
 231   | Split -> Box.Text([],"split")
 232   | Symmetry -> Box.Text([],"symmetry")
 233   | Transitivity term ->
 234       Box.V([],[Box.Text([],"transitivity");
 235                 Box.indent (ast2astBox term)])
 236 ;;
 237
 238 open TacticAst
 239
 240 let rec tactical2box = function
 241   | LocatedTactical (loc, tac) -> tactical2box tac
 242
 243   | Tactic tac -> tactic2box tac
 244   | Command cmd -> (* TODO dummy implementation *)
 245       Box.Text([], TacticAstPp.pp_tactical (Command cmd))
 246
 247   | Fail -> Box.Text([],"fail")
 248   | Do (count, tac) ->
 249       Box.V([],[Box.Text([],"do " ^ string_of_int count);
 250                 Box.indent (tactical2box tac)])
 251   | IdTac -> Box.Text([],"id")
 252   | Repeat tac ->
 253       Box.V([],[Box.Text([],"repeat");
 254                 Box.indent (tactical2box tac)])
 255   | Seq tacs ->
 256       Box.V([],tacticals2box tacs)
 257   | Then (tac, tacs) ->
 258       Box.V([],[tactical2box tac;
 259                 Box.H([],[Box.skip;
 260                           Box.Text([],"[");
 261                           Box.V([],tacticals2box tacs);
 262                           Box.Text([],"]");])])
 263   | Tries tacs ->
 264       Box.V([],[Box.Text([],"try");
 265                 Box.H([],[Box.skip;
 266                           Box.Text([],"[");
 267                           Box.V([],tacticals2box tacs);
 268                           Box.Text([],"]");])])
 269   | Try tac ->
 270       Box.V([],[Box.Text([],"try");
 271                 Box.indent (tactical2box tac)])
 272
 273 and tacticals2box tacs =
 274   List.map
 275     (function tac -> Box.H([],[tactical2box tac; Box.Text([],";")])) tacs
 276 ;;
 277
 278 let tacticalPp tac =
 279   String.concat "\n"
 280     (BoxPp.to_string CicAstPp.pp_term (tactical2box tac));;
 281
 282