]> matita.cs.unibo.it Git - helm.git/blob - tacticals.ml
8414698e783f25c0a4da517720caa5602a52e0f9
[helm.git] / tacticals.ml
1 (* Copyright (C) 2002, 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://cs.unibo.it/helm/.
24  *)
25
26 open CicReduction
27 open ProofEngineTypes
28 open UriManager
29
30 (** DEBUGGING *)
31
32   (** perform debugging output? *)
33 let debug = false
34
35   (** debugging print *)
36 let warn s =
37   if debug then
38     prerr_endline ("TACTICALS WARNING: " ^ s)
39
40
41 (** TACTIC{,AL}S *)
42
43   (* not a tactical, but it's used only here (?) *)
44
45 let id_tac ~status:(proof,goal) =
46   (proof,[goal])
47
48
49   (**
50     naive implementation of ORELSE tactical, try a sequence of tactics in turn:
51     if one fails pass to the next one and so on, eventually raises (failure "no
52     tactics left")
53     TODO warning: not tail recursive due to "try .. with" boxing
54
55     Galla: is this exactly Coq's "First"?
56
57   *)
58 let rec try_tactics ~(tactics: (string * tactic) list) ~status =
59   warn "in Tacticals.try_tactics";
60   match tactics with
61   | (descr, tac)::tactics ->
62       warn ("Tacticals.try_tactics IS TRYING " ^ descr);
63       (try
64         let res = tac ~status in
65         warn ("Tacticals.try_tactics: " ^ descr ^ " succedeed!!!");
66         res
67        with
68         e ->
69          match e with
70             (Fail _)
71           | (CicTypeChecker.TypeCheckerFailure _)
72           | (CicUnification.UnificationFailure _) ->
73               warn (
74                 "Tacticals.try_tactics failed with exn: " ^
75                 Printexc.to_string e);
76               try_tactics ~tactics ~status
77         | _ -> raise e (* [e] must not be caught ; let's re-raise it *)
78       )
79   | [] -> raise (Fail "try_tactics: no tactics left")
80
81
82
83 let thens ~start ~continuations ~status =
84  let (proof,new_goals) = start ~status in
85   try
86    List.fold_left2
87     (fun (proof,goals) goal tactic ->
88       let (proof',new_goals') = tactic ~status:(proof,goal) in
89        (proof',goals@new_goals')
90     ) (proof,[]) new_goals continuations
91   with
92    Invalid_argument _ -> raise (Fail "thens: wrong number of new goals")
93
94
95
96 let then_ ~start ~continuation ~status =
97  let (proof,new_goals) = start ~status in
98   List.fold_left
99    (fun (proof,goals) goal ->
100      let (proof',new_goals') = continuation ~status:(proof,goal) in
101       (proof',goals@new_goals')
102    ) (proof,[]) new_goals
103
104
105 (* Galla *)
106 (* si suppone che tutte le tattiche sollevino solamente Fail? *)
107
108
109 (* TODO: x debug: i due tatticali seguenti non contano quante volte hanno applicato la tattica *)
110
111 (* This keep on appling tactic until it fails *)
112 (* When <tactic> generates more than one goal, you have a tree of
113    application on the tactic, repeat_tactic works in depth on this tree *)
114
115 let rec repeat_tactic ~tactic ~status =
116   warn "in repeat_tactic";
117   try let (proof, goallist) = tactic ~status in
118    let rec step proof goallist =
119     match goallist with
120        [] -> (proof, [])
121      | head::tail -> 
122         let (proof', goallist') = repeat_tactic ~tactic ~status:(proof, head) in
123          let (proof'', goallist'') = step proof' tail in
124           proof'', goallist'@goallist''
125    in
126     step proof goallist
127   with 
128    (Fail _) as e ->
129     warn ("Tacticals.repeat_tactic failed after nth time with exception: " ^ Printexc.to_string e) ;
130     id_tac ~status
131 ;;
132
133
134
135 (* This tries to apply tactic n times *)
136
137 let rec do_tactic ~n ~tactic ~status =
138   warn "in do_tactic";
139   try 
140    let (proof, goallist) = 
141     if (n>0) then tactic ~status 
142              else id_tac ~status in
143 (*             else (proof, []) in *)(* perche' non va bene questo? stessa questione di ##### ? *)
144    let rec step proof goallist =
145     match goallist with
146        [] -> (proof, [])
147      | head::tail -> 
148         let (proof', goallist') = do_tactic ~n:(n-1) ~tactic ~status:(proof, head) in
149         let (proof'', goallist'') = step proof' tail in
150          proof'', goallist'@goallist''
151    in
152     step proof goallist
153   with 
154    (Fail _) as e ->
155     warn ("Tacticals.do_tactic failed after nth time with exception: " ^ Printexc.to_string e) ;
156     id_tac ~status
157 ;;
158
159
160
161 (* This applies tactic and catches its possible failure *)
162
163 let rec try_tactic ~tactic ~status =
164   warn "in Tacticals.try_tactic";
165   try
166    tactic ~status
167   with
168    (Fail _) as e -> 
169     warn ( "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e);
170     id_tac ~status
171 ;;
172
173
174 (* This tries tactics until one of them doesn't _solve_ the goal *)
175 (* TODO: si puo' unificare le 2(due) chiamate ricorsive? *)
176
177 let rec solve_tactics ~(tactics: (string * tactic) list) ~status =
178   warn "in Tacticals.solve_tactics";
179   match tactics with
180   | (descr, currenttactic)::moretactics ->
181       warn ("Tacticals.solve_tactics is trying " ^ descr);
182       (try
183         let (proof, goallist) = currenttactic ~status in
184          match goallist with 
185             [] -> warn ("Tacticals.solve_tactics: " ^ descr ^ " solved the goal!!!");
186 (* questo significa che non ci sono piu' goal, o che current_tactic non ne ha aperti di nuovi? (la 2a!) ##### *)
187 (* nel secondo caso basta per dire che solve_tactics has solved the goal? (si!) *)
188                   (proof, goallist)
189           | _ -> warn ("Tacticals.solve_tactics: try the next tactic");
190                  solve_tactics ~tactics:(moretactics) ~status
191        with
192         (Fail _) as e ->
193          warn ("Tacticals.solve_tactics: current tactic failed with exn: " ^ Printexc.to_string e);
194          solve_tactics ~tactics ~status
195       )
196   | [] -> raise (Fail "solve_tactics cannot solve the goal");
197           id_tac ~status
198 ;;
199
200
201
202
203
204
205
206
207
208
209   (** tattica di prova per debuggare i tatticali *)
210 (*
211 let thens' ~start ~continuations ~status =
212  let (proof,new_goals) = start ~status in
213   try
214    List.fold_left2
215     (fun (proof,goals) goal tactic ->
216       let (proof',new_goals') = tactic ~status:(proof,goal) in
217        (proof',goals@new_goals')
218     ) (proof,[]) new_goals continuations
219   with
220    Invalid_argument _ -> raise (Fail "thens: wrong number of new goals")
221
222 let prova_tac =
223  let apply_T_tac ~status:((proof,goal) as status) =
224   let curi,metasenv,pbo,pty = proof in
225   let metano,context,gty = CicUtil.lookup_meta goal metasenv in
226    let rel =
227     let rec find n =
228      function
229         [] -> assert false
230       | (Some (Cic.Name name,_))::_ when name = "T" -> n
231       | _::tl -> find (n+1) tl
232     in
233      prerr_endline ("eseguo find");
234      find 1 context
235    in
236     prerr_endline ("eseguo apply");    
237     apply_tac ~term:(Cic.Rel rel) ~status
238  in
239 (*  do_tactic ~n:2 *)
240   repeat_tactic
241    ~tactic:
242     (then_
243       ~start:(intros_tac ~name:"pippo")
244       ~continuation:(thens' ~start:apply_T_tac ~continuations:[id_tac ; apply_tac ~term:(Cic.Rel 1)]))
245 (* id_tac *)
246 ;;
247 *)
248
249