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 count_pattern current_size p =
  40  if current_size > maxsize then current_size
  41  else
  42 assert false
  43
  44 let count_kind =
  45  function
  46     `Reduce -> 6
  47   | `Simpl -> 8
  48   | `Whd -> 3
  49   | `Normalize -> 9
  50
  51 let rec count_tactic current_size tac =
  52   if current_size > maxsize then current_size
  53   else match tac with
  54     | Absurd (_, term) -> countterm (current_size + 6) term
  55     | Apply (_, term) -> countterm (current_size + 6) term
  56     | Auto _ -> current_size + 4
  57     | Assumption _ -> current_size + 10
  58     | Change (_,p,term) ->
  59        count_pattern (countterm (current_size + 13) term) p
  60     | Clear (_,id) -> current_size + 6 + String.length id
  61     | ClearBody (_,id) -> current_size + 10 + String.length id
  62     | Compare (_, term) -> countterm (current_size + 7) term
  63     | Constructor (_, n) -> current_size + 12
  64     | Contradiction _ -> current_size + 13
  65     | Cut (_, ident, term) ->
  66        let id_size =
  67         match ident with
  68            None -> 0
  69          | Some id -> String.length id + 4
  70        in
  71         countterm (current_size + 4 + id_size) term
  72     | DecideEquality _ -> current_size + 15
  73     | Decompose (_, term) ->
  74        countterm (current_size + 11) term
  75     | Discriminate (_, term) -> countterm (current_size + 12) term
  76     | Elim (_, term, using) ->
  77         let size1 = countterm (current_size + 5) term in
  78           (match using with
  79            None -> size1
  80              | Some term -> countterm (size1 + 7) term)
  81     | ElimType (_, term) -> countterm (current_size + 10) term
  82     | Exact (_, term) -> countterm (current_size + 6) term
  83     | Exists _ -> current_size + 6
  84     | Fail _ -> current_size + 4
  85     | Fold (_,kind,term,p) ->
  86        count_pattern (countterm (current_size + count_kind kind + 6) term) p
  87     | Fourier _ -> current_size + 7
  88     | FwdSimpl (_,id,idl) ->
  89         List.fold_left (fun s id -> s + String.length id)
  90          (current_size + 4 + String.length id) idl
  91     | Generalize (_,p,id) ->
  92        let id_size =
  93         match id with
  94            None -> 0
  95          | Some id -> 4 + String.length id
  96        in
  97         count_pattern (current_size + 11 + id_size) p
  98     | Goal (_, n) -> current_size + 4 + int_of_float (ceil (log10 (float n)))
  99     | IdTac _ -> current_size + 2
 100     | Injection (_, term) ->
 101        countterm (current_size + 10) term
 102     | Intros (_, num, idents) ->
 103         List.fold_left
 104           (fun size s -> size + (String.length s))
 105           (current_size + 7) idents
 106     | LApply (_,depth,terml,term,idopt) ->
 107        let idopt_size =
 108         match idopt with
 109            None -> 0
 110          | Some id -> 6 + String.length id in
 111        let terml_size =
 112         if terml = [] then 0
 113         else
 114          List.fold_left (fun s t -> countterm (s + 1) t) 3 terml in
 115        let depth_size =
 116         match depth with
 117            None -> 0
 118          | Some n -> 8 + n / 10
 119        in
 120         countterm (current_size + 7 + idopt_size + terml_size + depth_size) term
 121     | Left _ -> current_size + 4
 122     | LetIn (_, term, ident) ->
 123         countterm (current_size + 5 + String.length ident) term
 124     | Reduce (_,kind,p) ->
 125        count_pattern (current_size + count_kind kind + 1) p
 126     | Reflexivity _ -> current_size + 11
 127     | Replace (_,p,term) ->
 128        count_pattern (countterm (current_size + 11) term) p
 129     | Rewrite (_,dir,term,p) ->
 130        count_pattern (countterm (current_size + 10) term) p
 131     | Right _ -> current_size + 5
 132     | Ring _ -> current_size + 4
 133     | Split _ -> current_size + 5
 134     | Symmetry _ -> current_size + 8
 135     | Transitivity (_, term) ->
 136         countterm (current_size + 13) term
 137 ;;
 138
 139 let is_big_tac tac =
 140   let n = (count_tactic 0 tac) in
 141 (*   prerr_endline ("Lunghezza: " ^ (string_of_int n)); *)
 142   n > maxsize
 143 ;;
 144
 145 (* prova *)
 146 let rec small_tactic2box tac =
 147   Box.Text([], TacticAstPp.pp_tactic tac)
 148
 149 let string_of_kind = function
 150   | `Reduce -> "reduce"
 151   | `Simpl -> "simplify"
 152   | `Whd -> "whd"
 153   | `Normalize -> "normalize"
 154
 155 let dummy_tbl = Hashtbl.create 0
 156
 157 let ast2astBox ast = Ast2pres.ast2astBox (ast, dummy_tbl)
 158
 159 let pretty_append l ast =
 160   if is_big ast then
 161     [Box.H([],l);
 162      Box.H([],[Box.skip; ast2astBox ast])]
 163   else
 164     [Box.H([],l@[Box.smallskip; ast2astBox ast])]
 165
 166 let rec tactic2box tac =
 167   if (is_big_tac tac) then
 168     big_tactic2box tac
 169   else
 170     small_tactic2box tac
 171
 172 and big_tactic2box = function
 173   | Absurd (_, term) ->
 174       Box.V([],[Box.Text([],"absurd");
 175                 ast2astBox term])
 176   | Apply (_, term) ->
 177       Box.V([],[Box.Text([],"apply");
 178                 ast2astBox term])
 179   | Assumption _ -> Box.Text([],"assumption")
 180   | Auto _ -> Box.Text([],"auto")
 181   | Compare (_, term) ->
 182       Box.V([],[Box.Text([],"compare");
 183                 Box.indent(ast2astBox term)])
 184   | Constructor (_,n) -> Box.Text ([],"constructor " ^ string_of_int n)
 185   | Contradiction _ -> Box.Text([],"contradiction")
 186   | DecideEquality _ -> Box.Text([],"decide equality")
 187   | Decompose (_, term) ->
 188       Box.V([],[Box.Text([],"decompose");
 189                 Box.indent(ast2astBox term)])
 190   | Discriminate (_, term) ->
 191       Box.V([],pretty_append [Box.Text([],"discriminate")] term)
 192   | Elim (_, term, using) ->
 193       let using =
 194         (match using with
 195              None -> []
 196            | Some term ->
 197                (pretty_append
 198                   [Box.Text([],"using")]
 199                   term)) in
 200       Box.V([],
 201             (pretty_append
 202                [Box.Text([],"elim")]
 203                term)@using)
 204   | ElimType (_, term) ->
 205       Box.V([],[Box.Text([],"elim type");
 206                 Box.indent(ast2astBox term)])
 207   | Exact (_, term) ->
 208       Box.V([],[Box.Text([],"exact");
 209                 Box.indent(ast2astBox term)])
 210   | Exists _ -> Box.Text([],"exists")
 211   | Fourier _ -> Box.Text([],"fourier")
 212   | Goal (_, n) -> Box.Text([],"goal " ^ string_of_int n)
 213   | Intros (_, num, idents) ->
 214       let num =
 215         (match num with
 216              None -> []
 217            | Some num -> [Box.Text([],string_of_int num)]) in
 218       let idents =
 219         List.map (fun x -> Box.Text([],x)) idents in
 220       Box.V([],[Box.Text([],"decompose");
 221                 Box.H([],[Box.smallskip;
 222                           Box.V([],idents)])])
 223   | Left _ -> Box.Text([],"left")
 224   | LetIn (_, term, ident) ->
 225       Box.V([],[Box.H([],[Box.Text([],"let");
 226                           Box.smallskip;
 227                           Box.Text([],ident);
 228                           Box.smallskip;
 229                           Box.Text([],"=")]);
 230                 Box.indent (ast2astBox term)])
 231   | Reflexivity _ -> Box.Text([],"reflexivity")
 232   | Right _ -> Box.Text([],"right")
 233   | Ring _ ->  Box.Text([],"ring")
 234   | Split _ -> Box.Text([],"split")
 235   | Symmetry _ -> Box.Text([],"symmetry")
 236   | Transitivity (_, term) ->
 237       Box.V([],[Box.Text([],"transitivity");
 238                 Box.indent (ast2astBox term)])
 239 ;;
 240
 241 open TacticAst
 242
 243 let rec tactical2box = function
 244   | Tactic (_, tac) -> tactic2box tac
 245   | Do (_, count, tac) ->
 246       Box.V([],[Box.Text([],"do " ^ string_of_int count);
 247                 Box.indent (tactical2box tac)])
 248   | Repeat (_, tac) ->
 249       Box.V([],[Box.Text([],"repeat");
 250                 Box.indent (tactical2box tac)])
 251   | Seq (_, tacs) ->
 252       Box.V([],tacticals2box tacs)
 253   | Then (_, tac, tacs) ->
 254       Box.V([],[tactical2box tac;
 255                 Box.H([],[Box.skip;
 256                           Box.Text([],"[");
 257                           Box.V([],tacticals2box tacs);
 258                           Box.Text([],"]");])])
 259   | Tries (_, tacs) ->
 260       Box.V([],[Box.Text([],"try");
 261                 Box.H([],[Box.skip;
 262                           Box.Text([],"[");
 263                           Box.V([],tacticals2box tacs);
 264                           Box.Text([],"]");])])
 265   | Try (_, tac) ->
 266       Box.V([],[Box.Text([],"try");
 267                 Box.indent (tactical2box tac)])
 268
 269 and tacticals2box tacs =
 270   List.map
 271     (function tac -> Box.H([],[tactical2box tac; Box.Text([],";")])) tacs
 272 ;;
 273
 274 let tacticalPp tac =
 275   String.concat "\n"
 276     (BoxPp.to_string CicAstPp.pp_term (tactical2box tac));;
 277
 278