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