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