]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic_transformations/tacticAst2Box.ml
snapshot
[helm.git] / 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