1 (* Copyright (C) 2002, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
32 (** perform debugging output? *)
34 let debug_print = fun _ -> ()
36 (** debugging print *)
39 debug_print ("TACTICALS WARNING: " ^ s)
42 let id_tac (proof,goal) =
43 let _, metasenv, _, _ = proof in
44 let _, _, _ = CicUtil.lookup_meta goal metasenv in
50 let fail_tac (proof,goal) =
51 let _, metasenv, _, _ = proof in
52 let _, _, _ = CicUtil.lookup_meta goal metasenv in
53 raise (Fail "fail tactical")
63 val mk_tactic : (input_status -> output_status) -> tactic
64 val apply_tactic : tactic -> input_status -> output_status
65 val goals : output_status -> ProofEngineTypes.goal list
66 val set_goals: output_status -> ProofEngineTypes.goal list -> output_status
67 val focus : output_status -> ProofEngineTypes.goal -> input_status
74 val first: tactics: (string * tactic) list -> tactic
76 val thens: start: tactic -> continuations: tactic list -> tactic
78 val then_: start: tactic -> continuation: tactic -> tactic
80 (** "folding" of then_ *)
81 val seq: tactics: tactic list -> tactic
83 val repeat_tactic: tactic: tactic -> tactic
85 val do_tactic: n: int -> tactic: tactic -> tactic
87 val try_tactic: tactic: tactic -> tactic
89 val solve_tactics: tactics: (string * tactic) list -> tactic
92 module Make (S:Status) : T with type tactic = S.tactic =
94 type tactic = S.tactic
97 naive implementation of ORELSE tactical, try a sequence of tactics in turn:
98 if one fails pass to the next one and so on, eventually raises (failure "no
102 let rec first ~(tactics: (string * tactic) list) status =
103 warn "in Tacticals.first";
105 | (descr, tac)::tactics ->
106 warn ("Tacticals.first IS TRYING " ^ descr);
108 let res = S.apply_tactic tac status in
109 warn ("Tacticals.first: " ^ descr ^ " succedeed!!!");
115 | (CicTypeChecker.TypeCheckerFailure _)
116 | (CicUnification.UnificationFailure _) ->
118 "Tacticals.first failed with exn: " ^
119 Printexc.to_string e);
120 first ~tactics status
121 | _ -> raise e (* [e] must not be caught ; let's re-raise it *)
123 | [] -> raise (Fail "first: no tactics left")
125 S.mk_tactic (first ~tactics)
128 let thens ~start ~continuations =
129 let thens ~start ~continuations status =
130 let output_status = S.apply_tactic start status in
131 let new_goals = S.goals output_status in
133 let output_status,goals =
135 (fun (output_status,goals) goal tactic ->
136 let status = S.focus output_status goal in
137 let output_status' = S.apply_tactic tactic status in
138 let new_goals' = S.goals output_status' in
139 (output_status',goals@new_goals')
140 ) (output_status,[]) new_goals continuations
142 S.set_goals output_status goals
144 Invalid_argument _ ->
145 let debug = Printf.sprintf "thens: expected %i new goals, found %i"
146 (List.length continuations) (List.length new_goals)
150 S.mk_tactic (thens ~start ~continuations )
153 let then_ ~start ~continuation =
154 let then_ ~start ~continuation status =
155 let output_status = S.apply_tactic start status in
156 let new_goals = S.goals output_status in
157 let output_status,goals =
159 (fun (output_status,goals) goal ->
160 let status = S.focus output_status goal in
161 let output_status' = S.apply_tactic continuation status in
162 let new_goals' = S.goals output_status' in
163 (output_status',goals@new_goals')
164 ) (output_status,[]) new_goals
166 S.set_goals output_status goals
168 S.mk_tactic (then_ ~start ~continuation)
170 let rec seq ~tactics =
174 | hd :: tl -> then_ ~start:hd ~continuation:(seq ~tactics:tl)
176 (* TODO: x debug: i due tatticali seguenti non contano quante volte hanno applicato la tattica *)
178 (* This keep on appling tactic until it fails *)
179 (* When <tactic> generates more than one goal, you have a tree of
180 application on the tactic, repeat_tactic works in depth on this tree *)
182 let repeat_tactic ~tactic =
183 let rec repeat_tactic ~tactic status =
184 warn "in repeat_tactic";
186 let output_status = S.apply_tactic tactic status in
187 let goallist = S.goals output_status in
188 let rec step output_status goallist =
190 [] -> output_status,[]
192 let status = S.focus output_status head in
193 let output_status' = repeat_tactic ~tactic status in
194 let goallist' = S.goals output_status' in
195 let output_status'',goallist'' = step output_status' tail in
196 output_status'',goallist'@goallist''
198 let output_status,goallist = step output_status goallist in
199 S.set_goals output_status goallist
202 warn ("Tacticals.repeat_tactic failed after nth time with exception: " ^ Printexc.to_string e) ;
203 S.apply_tactic S.id_tac status
205 S.mk_tactic (repeat_tactic ~tactic)
208 (* This tries to apply tactic n times *)
209 let do_tactic ~n ~tactic =
210 let rec do_tactic ~n ~tactic status =
212 S.apply_tactic S.id_tac status
215 let output_status = S.apply_tactic tactic status in
216 let goallist = S.goals output_status in
217 let rec step output_status goallist =
219 [] -> output_status, []
221 let status = S.focus output_status head in
222 let output_status' = do_tactic ~n:(n-1) ~tactic status in
223 let goallist' = S.goals output_status' in
224 let (output_status'', goallist'') = step output_status' tail in
225 output_status'', goallist'@goallist''
227 let output_status,goals = step output_status goallist in
228 S.set_goals output_status goals
231 warn ("Tacticals.do_tactic failed after nth time with exception: " ^ Printexc.to_string e) ;
232 S.apply_tactic S.id_tac status
234 S.mk_tactic (do_tactic ~n ~tactic)
238 (* This applies tactic and catches its possible failure *)
239 let try_tactic ~tactic =
240 let rec try_tactic ~tactic status =
241 warn "in Tacticals.try_tactic";
243 S.apply_tactic tactic status
246 warn ( "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e);
247 S.apply_tactic S.id_tac status
249 S.mk_tactic (try_tactic ~tactic)
251 (* This tries tactics until one of them doesn't _solve_ the goal *)
252 (* TODO: si puo' unificare le 2(due) chiamate ricorsive? *)
253 let solve_tactics ~tactics =
254 let rec solve_tactics ~(tactics: (string * tactic) list) status =
255 warn "in Tacticals.solve_tactics";
257 | (descr, currenttactic)::moretactics ->
258 warn ("Tacticals.solve_tactics is trying " ^ descr);
260 let output_status = S.apply_tactic currenttactic status in
261 let goallist = S.goals output_status in
263 [] -> warn ("Tacticals.solve_tactics: " ^ descr ^
264 " solved the goal!!!");
265 (* questo significa che non ci sono piu' goal, o che current_tactic non ne
266 ha aperti di nuovi? (la 2a!) #####
267 nel secondo caso basta per dire che solve_tactics has solved the goal? (si!) *)
269 | _ -> warn ("Tacticals.solve_tactics: try the next tactic");
270 solve_tactics ~tactics:(moretactics) status
273 warn ("Tacticals.solve_tactics: current tactic failed with exn: " ^
274 Printexc.to_string e);
275 solve_tactics ~tactics status
277 | [] -> raise (Fail "solve_tactics cannot solve the goal");
278 S.apply_tactic S.id_tac status
280 S.mk_tactic (solve_tactics ~tactics)
283 module ProofEngineStatus =
285 type input_status = ProofEngineTypes.status
286 type output_status = ProofEngineTypes.proof * ProofEngineTypes.goal list
287 type tactic = ProofEngineTypes.tactic
289 let mk_tactic = ProofEngineTypes.mk_tactic
290 let apply_tactic = ProofEngineTypes.apply_tactic
291 let goals (_,goals) = goals
292 let set_goals (proof,_) goals = proof,goals
293 let focus (proof,_) goal = proof,goal
296 module ProofEngineTacticals = Make(ProofEngineStatus)
298 include ProofEngineTacticals