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     | Compare (_, term) -> countterm (current_size + 7) term
  47     | Constructor (_, n) -> current_size + 12
  48     | Contradiction _ -> current_size + 13
  49     | Cut (_, ident, term) ->
  50        let id_size =
  51         match ident with
  52            None -> 0
  53          | Some id -> String.length id + 4
  54        in
  55         countterm (current_size + 4 + id_size) term
  56     | DecideEquality _ -> current_size + 15
  57     | Decompose (_, term) ->
  58        countterm (current_size + 11) term
  59     | Discriminate (_, term) -> countterm (current_size + 12) term
  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     | Fourier _ -> current_size + 7
  69     | Goal (_, n) -> current_size + 4 + int_of_float (ceil (log10 (float n)))
  70     | Injection (_, term) ->
  71        countterm (current_size + 10) term
  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     | Reflexivity _ -> current_size + 11
  80     | Right _ -> current_size + 5
  81     | Ring _ -> current_size + 4
  82     | Split _ -> current_size + 5
  83     | Symmetry _ -> current_size + 8
  84     | Transitivity (_, term) ->
  85         countterm (current_size + 13) term
  86 ;;
  87
  88 let is_big_tac tac =
  89   let n = (count_tactic 0 tac) in
  90 (*   prerr_endline ("Lunghezza: " ^ (string_of_int n)); *)
  91   n > maxsize
  92 ;;
  93
  94 (* prova *)
  95 let rec small_tactic2box tac =
  96   Box.Text([], TacticAstPp.pp_tactic tac)
  97
  98 let string_of_kind = function
  99   | `Reduce -> "reduce"
 100   | `Simpl -> "simplify"
 101   | `Whd -> "whd"
 102   | `Normalize -> "normalize"
 103
 104 let dummy_tbl = Hashtbl.create 0
 105
 106 let ast2astBox ast = Ast2pres.ast2astBox (ast, dummy_tbl)
 107
 108 let pretty_append l ast =
 109   if is_big ast then
 110     [Box.H([],l);
 111      Box.H([],[Box.skip; ast2astBox ast])]
 112   else
 113     [Box.H([],l@[Box.smallskip; ast2astBox ast])]
 114
 115 let rec tactic2box tac =
 116   if (is_big_tac tac) then
 117     big_tactic2box tac
 118   else
 119     small_tactic2box tac
 120
 121 and big_tactic2box = function
 122   | Absurd (_, term) ->
 123       Box.V([],[Box.Text([],"absurd");
 124                 ast2astBox term])
 125   | Apply (_, term) ->
 126       Box.V([],[Box.Text([],"apply");
 127                 ast2astBox term])
 128   | Assumption _ -> Box.Text([],"assumption")
 129   | Auto _ -> Box.Text([],"auto")
 130   | Compare (_, term) ->
 131       Box.V([],[Box.Text([],"compare");
 132                 Box.indent(ast2astBox term)])
 133   | Constructor (_,n) -> Box.Text ([],"constructor " ^ string_of_int n)
 134   | Contradiction _ -> Box.Text([],"contradiction")
 135   | DecideEquality _ -> Box.Text([],"decide equality")
 136   | Decompose (_, term) ->
 137       Box.V([],[Box.Text([],"decompose");
 138                 Box.indent(ast2astBox term)])
 139   | Discriminate (_, term) ->
 140       Box.V([],pretty_append [Box.Text([],"discriminate")] term)
 141   | Elim (_, term, using) ->
 142       let using =
 143         (match using with
 144              None -> []
 145            | Some term ->
 146                (pretty_append
 147                   [Box.Text([],"using")]
 148                   term)) in
 149       Box.V([],
 150             (pretty_append
 151                [Box.Text([],"elim")]
 152                term)@using)
 153   | ElimType (_, term) ->
 154       Box.V([],[Box.Text([],"elim type");
 155                 Box.indent(ast2astBox term)])
 156   | Exact (_, term) ->
 157       Box.V([],[Box.Text([],"exact");
 158                 Box.indent(ast2astBox term)])
 159   | Exists _ -> Box.Text([],"exists")
 160   | Fourier _ -> Box.Text([],"fourier")
 161   | Goal (_, n) -> Box.Text([],"goal " ^ string_of_int n)
 162   | Intros (_, num, idents) ->
 163       let num =
 164         (match num with
 165              None -> []
 166            | Some num -> [Box.Text([],string_of_int num)]) in
 167       let idents =
 168         List.map (fun x -> Box.Text([],x)) idents in
 169       Box.V([],[Box.Text([],"decompose");
 170                 Box.H([],[Box.smallskip;
 171                           Box.V([],idents)])])
 172   | Left _ -> Box.Text([],"left")
 173   | LetIn (_, term, ident) ->
 174       Box.V([],[Box.H([],[Box.Text([],"let");
 175                           Box.smallskip;
 176                           Box.Text([],ident);
 177                           Box.smallskip;
 178                           Box.Text([],"=")]);
 179                 Box.indent (ast2astBox term)])
 180   | Reflexivity _ -> Box.Text([],"reflexivity")
 181   | Right _ -> Box.Text([],"right")
 182   | Ring _ ->  Box.Text([],"ring")
 183   | Split _ -> Box.Text([],"split")
 184   | Symmetry _ -> Box.Text([],"symmetry")
 185   | Transitivity (_, term) ->
 186       Box.V([],[Box.Text([],"transitivity");
 187                 Box.indent (ast2astBox term)])
 188 ;;
 189
 190 open TacticAst
 191
 192 let rec tactical2box = function
 193   | Tactic (_, tac) -> tactic2box tac
 194   | Do (_, count, tac) ->
 195       Box.V([],[Box.Text([],"do " ^ string_of_int count);
 196                 Box.indent (tactical2box tac)])
 197   | Repeat (_, tac) ->
 198       Box.V([],[Box.Text([],"repeat");
 199                 Box.indent (tactical2box tac)])
 200   | Seq (_, tacs) ->
 201       Box.V([],tacticals2box tacs)
 202   | Then (_, tac, tacs) ->
 203       Box.V([],[tactical2box tac;
 204                 Box.H([],[Box.skip;
 205                           Box.Text([],"[");
 206                           Box.V([],tacticals2box tacs);
 207                           Box.Text([],"]");])])
 208   | Tries (_, tacs) ->
 209       Box.V([],[Box.Text([],"try");
 210                 Box.H([],[Box.skip;
 211                           Box.Text([],"[");
 212                           Box.V([],tacticals2box tacs);
 213                           Box.Text([],"]");])])
 214   | Try (_, tac) ->
 215       Box.V([],[Box.Text([],"try");
 216                 Box.indent (tactical2box tac)])
 217
 218 and tacticals2box tacs =
 219   List.map
 220     (function tac -> Box.H([],[tactical2box tac; Box.Text([],";")])) tacs
 221 ;;
 222
 223 let tacticalPp tac =
 224   String.concat "\n"
 225     (BoxPp.to_string CicAstPp.pp_term (tactical2box tac));;
 226
 227