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 *)
37 let warn s = debug_print (lazy ("TACTICALS WARNING: " ^ (Lazy.force s)))
40 let id_tac (proof,goal) =
41 let _, metasenv, _, _ = proof in
42 let _, _, _ = CicUtil.lookup_meta goal metasenv in
48 let fail_tac (proof,goal) =
49 let _, metasenv, _, _ = proof in
50 let _, _, _ = CicUtil.lookup_meta goal metasenv in
51 raise (Fail "fail tactical")
61 val mk_tactic : (input_status -> output_status) -> tactic
62 val apply_tactic : tactic -> input_status -> output_status
63 val goals : output_status -> ProofEngineTypes.goal list
64 val set_goals: output_status -> ProofEngineTypes.goal list -> output_status
65 val focus : output_status -> ProofEngineTypes.goal -> input_status
72 val first: tactics: (string * tactic) list -> tactic
74 val thens: start: tactic -> continuations: tactic list -> tactic
76 val then_: start: tactic -> continuation: tactic -> tactic
78 (** "folding" of then_ *)
79 val seq: tactics: tactic list -> tactic
81 val repeat_tactic: tactic: tactic -> tactic
83 val do_tactic: n: int -> tactic: tactic -> tactic
85 val try_tactic: tactic: tactic -> tactic
87 val solve_tactics: tactics: (string * tactic) list -> tactic
90 module Make (S:Status) : T with type tactic = S.tactic =
92 type tactic = S.tactic
95 naive implementation of ORELSE tactical, try a sequence of tactics in turn:
96 if one fails pass to the next one and so on, eventually raises (failure "no
100 let rec first ~(tactics: (string * tactic) list) status =
101 warn (lazy "in Tacticals.first");
103 | (descr, tac)::tactics ->
104 warn (lazy ("Tacticals.first IS TRYING " ^ descr));
106 let res = S.apply_tactic tac status in
107 warn (lazy ("Tacticals.first: " ^ descr ^ " succedeed!!!"));
113 | (CicTypeChecker.TypeCheckerFailure _)
114 | (CicUnification.UnificationFailure _) ->
116 "Tacticals.first failed with exn: " ^
117 Printexc.to_string e));
118 first ~tactics status
119 | _ -> raise e (* [e] must not be caught ; let's re-raise it *)
121 | [] -> raise (Fail "first: no tactics left")
123 S.mk_tactic (first ~tactics)
126 let thens ~start ~continuations =
127 let thens ~start ~continuations status =
128 let output_status = S.apply_tactic start status in
129 let new_goals = S.goals output_status in
131 let output_status,goals =
133 (fun (output_status,goals) goal tactic ->
134 let status = S.focus output_status goal in
135 let output_status' = S.apply_tactic tactic status in
136 let new_goals' = S.goals output_status' in
137 (output_status',goals@new_goals')
138 ) (output_status,[]) new_goals continuations
140 S.set_goals output_status goals
142 Invalid_argument _ ->
143 let debug = Printf.sprintf "thens: expected %i new goals, found %i"
144 (List.length continuations) (List.length new_goals)
148 S.mk_tactic (thens ~start ~continuations )
151 let then_ ~start ~continuation =
152 let then_ ~start ~continuation status =
153 let output_status = S.apply_tactic start status in
154 let new_goals = S.goals output_status in
155 let output_status,goals =
157 (fun (output_status,goals) goal ->
158 let status = S.focus output_status goal in
159 let output_status' = S.apply_tactic continuation status in
160 let new_goals' = S.goals output_status' in
161 (output_status',goals@new_goals')
162 ) (output_status,[]) new_goals
164 S.set_goals output_status goals
166 S.mk_tactic (then_ ~start ~continuation)
168 let rec seq ~tactics =
172 | hd :: tl -> then_ ~start:hd ~continuation:(seq ~tactics:tl)
174 (* TODO: x debug: i due tatticali seguenti non contano quante volte hanno applicato la tattica *)
176 (* This keep on appling tactic until it fails *)
177 (* When <tactic> generates more than one goal, you have a tree of
178 application on the tactic, repeat_tactic works in depth on this tree *)
180 let repeat_tactic ~tactic =
181 let rec repeat_tactic ~tactic status =
182 warn (lazy "in repeat_tactic");
184 let output_status = S.apply_tactic tactic status in
185 let goallist = S.goals output_status in
186 let rec step output_status goallist =
188 [] -> output_status,[]
190 let status = S.focus output_status head in
191 let output_status' = repeat_tactic ~tactic status in
192 let goallist' = S.goals output_status' in
193 let output_status'',goallist'' = step output_status' tail in
194 output_status'',goallist'@goallist''
196 let output_status,goallist = step output_status goallist in
197 S.set_goals output_status goallist
200 warn (lazy ("Tacticals.repeat_tactic failed after nth time with exception: " ^ Printexc.to_string e)) ;
201 S.apply_tactic S.id_tac status
203 S.mk_tactic (repeat_tactic ~tactic)
206 (* This tries to apply tactic n times *)
207 let do_tactic ~n ~tactic =
208 let rec do_tactic ~n ~tactic status =
210 S.apply_tactic S.id_tac status
213 let output_status = S.apply_tactic tactic status in
214 let goallist = S.goals output_status in
215 let rec step output_status goallist =
217 [] -> output_status, []
219 let status = S.focus output_status head in
220 let output_status' = do_tactic ~n:(n-1) ~tactic status in
221 let goallist' = S.goals output_status' in
222 let (output_status'', goallist'') = step output_status' tail in
223 output_status'', goallist'@goallist''
225 let output_status,goals = step output_status goallist in
226 S.set_goals output_status goals
229 warn (lazy ("Tacticals.do_tactic failed after nth time with exception: " ^ Printexc.to_string e)) ;
230 S.apply_tactic S.id_tac status
232 S.mk_tactic (do_tactic ~n ~tactic)
236 (* This applies tactic and catches its possible failure *)
237 let try_tactic ~tactic =
238 let rec try_tactic ~tactic status =
239 warn (lazy "in Tacticals.try_tactic");
241 S.apply_tactic tactic status
244 warn (lazy ( "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e));
245 S.apply_tactic S.id_tac status
247 S.mk_tactic (try_tactic ~tactic)
249 (* This tries tactics until one of them doesn't _solve_ the goal *)
250 (* TODO: si puo' unificare le 2(due) chiamate ricorsive? *)
251 let solve_tactics ~tactics =
252 let rec solve_tactics ~(tactics: (string * tactic) list) status =
253 warn (lazy "in Tacticals.solve_tactics");
255 | (descr, currenttactic)::moretactics ->
256 warn (lazy ("Tacticals.solve_tactics is trying " ^ descr));
258 let output_status = S.apply_tactic currenttactic status in
259 let goallist = S.goals output_status in
261 [] -> warn (lazy ("Tacticals.solve_tactics: " ^ descr ^
262 " solved the goal!!!"));
263 (* questo significa che non ci sono piu' goal, o che current_tactic non ne
264 ha aperti di nuovi? (la 2a!) #####
265 nel secondo caso basta per dire che solve_tactics has solved the goal? (si!) *)
267 | _ -> warn (lazy ("Tacticals.solve_tactics: try the next tactic"));
268 solve_tactics ~tactics:(moretactics) status
271 warn (lazy ("Tacticals.solve_tactics: current tactic failed with exn: " ^
272 Printexc.to_string e));
273 solve_tactics ~tactics status
275 | [] -> raise (Fail "solve_tactics cannot solve the goal");
276 S.apply_tactic S.id_tac status
278 S.mk_tactic (solve_tactics ~tactics)
281 module ProofEngineStatus =
283 type input_status = ProofEngineTypes.status
284 type output_status = ProofEngineTypes.proof * ProofEngineTypes.goal list
285 type tactic = ProofEngineTypes.tactic
287 let mk_tactic = ProofEngineTypes.mk_tactic
288 let apply_tactic = ProofEngineTypes.apply_tactic
289 let goals (_,goals) = goals
290 let set_goals (proof,_) goals = proof,goals
291 let focus (proof,_) goal = proof,goal
294 module ProofEngineTacticals = Make(ProofEngineStatus)
296 include ProofEngineTacticals