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/.
34 (** perform debugging output? *)
36 let debug_print = fun _ -> ()
38 (** debugging print *)
39 let info s = debug_print (lazy ("TACTICALS INFO: " ^ (Lazy.force s)))
42 let id_tac (proof,goal) =
43 let _, metasenv, _, _ = proof in
44 let _, _, _ = CicUtil.lookup_meta goal metasenv in
47 ProofEngineTypes.mk_tactic id_tac
50 let fail_tac (proof,goal) =
51 let _, metasenv, _, _ = proof in
52 let _, _, _ = CicUtil.lookup_meta goal metasenv in
53 raise (ProofEngineTypes.Fail (lazy "fail tactical"))
55 ProofEngineTypes.mk_tactic fail_tac
57 type goal = ProofEngineTypes.goal
59 (** TODO needed until tactics start returning both opened and closed goals
60 * First part of the function performs a diff among goals ~before tactic
61 * application and ~after it. Second part will add as both opened and closed
62 * the goals which are returned as opened by the tactic *)
63 let goals_diff ~before ~after ~opened =
64 let sort_opened opened add =
65 opened @ (List.filter (fun g -> not (List.mem g opened)) add)
69 (fun remove e -> if List.mem e after then remove else e :: remove)
74 (fun add e -> if List.mem e before then add else e :: add)
78 let add, remove = (* adds goals which have been both opened _and_ closed *)
80 (fun (add, remove) opened_goal ->
81 if List.mem opened_goal before
82 then opened_goal :: add, opened_goal :: remove
87 sort_opened opened add, remove
92 val first: tactics: (string * tactic) list -> tactic
93 val thens: start: tactic -> continuations: tactic list -> tactic
94 val then_: start: tactic -> continuation: tactic -> tactic
95 val seq: tactics: tactic list -> tactic
96 val repeat_tactic: tactic: tactic -> tactic
97 val do_tactic: n: int -> tactic: tactic -> tactic
98 val try_tactic: tactic: tactic -> tactic
99 val solve_tactics: tactics: (string * tactic) list -> tactic
101 val tactic: tactic -> tactic
104 val semicolon: tactic
107 val pos: int list -> tactic
110 val focus: int list -> tactic
114 module Make (S: Continuationals.Status) : T with type tactic = S.tactic =
116 module C = Continuationals.Make (S)
118 type tactic = S.tactic
120 let fold_eval status ts =
122 List.fold_left (fun istatus t -> S.focus ~-1 (C.eval t istatus)) status ts
127 naive implementation of ORELSE tactical, try a sequence of tactics in turn:
128 if one fails pass to the next one and so on, eventually raises (failure "no
132 let rec first ~(tactics: (string * tactic) list) istatus =
133 info (lazy "in Tacticals.first");
135 | (descr, tac)::tactics ->
136 info (lazy ("Tacticals.first IS TRYING " ^ descr));
138 let res = S.apply_tactic tac istatus in
139 info (lazy ("Tacticals.first: " ^ descr ^ " succedeed!!!"));
144 | (ProofEngineTypes.Fail _)
145 | (CicTypeChecker.TypeCheckerFailure _)
146 | (CicUnification.UnificationFailure _) ->
148 "Tacticals.first failed with exn: " ^
149 Printexc.to_string e));
150 first ~tactics istatus
151 | _ -> raise e) (* [e] must not be caught ; let's re-raise it *)
152 | [] -> raise (ProofEngineTypes.Fail (lazy "first: no tactics left"))
154 S.mk_tactic (first ~tactics)
156 let thens ~start ~continuations =
160 ([ C.Tactical (C.Tactic start); C.Branch ]
161 @ (HExtlib.list_concat ~sep:[ C.Shift ]
162 (List.map (fun t -> [ C.Tactical (C.Tactic t) ]) continuations))
165 let then_ ~start ~continuation =
168 let ostatus = C.eval (C.Tactical (C.Tactic start)) istatus in
169 let opened,closed = S.goals ostatus in
173 fold_eval (S.focus ~-1 ostatus)
175 C.Tactical (C.Tactic continuation) ])
181 (HExtlib.list_concat ~sep:[ C.Semicolon ]
182 (List.map (fun t -> [ C.Tactical (C.Tactic t) ]) tactics)))
184 (* TODO: x debug: i due tatticali seguenti non contano quante volte hanno
185 * applicato la tattica *)
187 let rec step f output_status opened closed =
189 | [] -> output_status, [], closed
191 let status = S.focus head output_status in
192 let output_status' = f status in
193 let opened', closed' = S.goals output_status' in
194 let output_status'', opened'', closed'' =
195 step f output_status' tail []
197 output_status'', opened' @ opened'', closed' @ closed''
199 (* This keep on appling tactic until it fails. When <tactic> generates more
200 * than one goal, you have a tree of application on the tactic, repeat_tactic
201 * works in depth on this tree *)
202 let repeat_tactic ~tactic =
203 let rec repeat_tactic ~tactic status =
204 info (lazy "in repeat_tactic");
206 let output_status = S.apply_tactic tactic status in
207 let opened, closed = S.goals output_status in
208 let output_status, opened', closed' =
209 step (repeat_tactic ~tactic) output_status opened closed
211 S.set_goals (opened', closed') output_status
213 (ProofEngineTypes.Fail _) as e ->
215 ("Tacticals.repeat_tactic failed after nth time with exception: "
216 ^ Printexc.to_string e));
217 S.apply_tactic S.id_tactic status
219 S.mk_tactic (repeat_tactic ~tactic)
221 (* This tries to apply tactic n times *)
222 let do_tactic ~n ~tactic =
223 let rec do_tactic ~n ~tactic status =
225 S.apply_tactic S.id_tactic status
228 let output_status = S.apply_tactic tactic status in
229 let opened, closed = S.goals output_status in
230 let output_status, opened', closed' =
231 step (do_tactic ~n:(n-1) ~tactic) output_status opened closed
233 S.set_goals (opened', closed') output_status
235 (ProofEngineTypes.Fail _) as e ->
237 ("Tacticals.do_tactic failed after nth time with exception: "
238 ^ Printexc.to_string e)) ;
239 S.apply_tactic S.id_tactic status
241 S.mk_tactic (do_tactic ~n ~tactic)
243 (* This applies tactic and catches its possible failure *)
244 let try_tactic ~tactic =
245 let rec try_tactic ~tactic status =
246 info (lazy "in Tacticals.try_tactic");
248 S.apply_tactic tactic status
250 (ProofEngineTypes.Fail _) as e ->
252 "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e));
253 S.apply_tactic S.id_tactic status
255 S.mk_tactic (try_tactic ~tactic)
257 (* This tries tactics until one of them doesn't _solve_ the goal *)
258 (* TODO: si puo' unificare le 2(due) chiamate ricorsive? *)
259 let solve_tactics ~tactics =
260 let rec solve_tactics ~(tactics: (string * tactic) list) status =
261 info (lazy "in Tacticals.solve_tactics");
263 | (descr, currenttactic)::moretactics ->
264 info (lazy ("Tacticals.solve_tactics is trying " ^ descr));
266 let output_status = S.apply_tactic currenttactic status in
267 let opened, closed = S.goals output_status in
269 | [] -> info (lazy ("Tacticals.solve_tactics: " ^ descr ^
270 " solved the goal!!!"));
271 (* questo significa che non ci sono piu' goal, o che current_tactic non ne ha
272 * aperti di nuovi? (la 2a!) ##### nel secondo caso basta per dire che
273 * solve_tactics has solved the goal? (si!) *)
275 | _ -> info (lazy ("Tacticals.solve_tactics: try the next tactic"));
276 solve_tactics ~tactics:(moretactics) status
278 (ProofEngineTypes.Fail _) as e ->
280 "Tacticals.solve_tactics: current tactic failed with exn: "
281 ^ Printexc.to_string e));
282 solve_tactics ~tactics status
285 raise (ProofEngineTypes.Fail
286 (lazy "solve_tactics cannot solve the goal"))
288 S.mk_tactic (solve_tactics ~tactics)
290 let cont_proxy cont = S.mk_tactic (C.eval cont)
292 let tactic t = cont_proxy (C.Tactical (C.Tactic t))
293 let skip = cont_proxy (C.Tactical C.Skip)
294 let dot = cont_proxy C.Dot
295 let semicolon = cont_proxy C.Semicolon
296 let branch = cont_proxy C.Branch
297 let shift = cont_proxy C.Shift
298 let pos i = cont_proxy (C.Pos i)
299 let wildcard = cont_proxy C.Wildcard
300 let merge = cont_proxy C.Merge
301 let focus goals = cont_proxy (C.Focus goals)
302 let unfocus = cont_proxy C.Unfocus
305 module ProofEngineStatus =
307 module Stack = Continuationals.Stack
310 ProofEngineTypes.status (* (proof, goal) *) * Stack.t
313 (ProofEngineTypes.proof * goal list * goal list) * Stack.t
315 type tactic = ProofEngineTypes.tactic
317 let id_tactic = id_tac
320 ProofEngineTypes.mk_tactic
321 (fun (proof, goal) as pstatus ->
322 let stack = [ [ 1, Stack.Open goal ], [], [], `NoTag ] in
323 let istatus = pstatus, stack in
324 (* let ostatus = f istatus in
325 let ((proof, opened, _), _) = ostatus in *)
326 let (proof, _, _), stack = f istatus in
327 let opened = Continuationals.Stack.open_goals stack in
330 let apply_tactic tac ((proof, _) as pstatus, stack) =
331 let proof', opened = ProofEngineTypes.apply_tactic tac pstatus in
332 (* let _ = prerr_endline ("goal aperti dalla tattica " ^ String.concat "," (List.map string_of_int opened)) in *)
333 let before = ProofEngineTypes.goals_of_proof proof in
334 let after = ProofEngineTypes.goals_of_proof proof' in
335 let opened_goals, closed_goals = goals_diff ~before ~after ~opened in
336 (* let _ = prerr_endline ("goal ritornati dalla tattica " ^ String.concat "," (List.map string_of_int opened_goals)) in *)
337 (proof', opened_goals, closed_goals), stack
339 let goals ((_, opened, closed), _) = opened, closed
340 let set_goals (opened, closed) ((proof, _, _), stack) =
341 (proof, opened, closed), stack
344 let set_stack stack (opstatus, _) = opstatus, stack
346 let inject ((proof, _), stack) = ((proof, [], []), stack)
347 let focus goal ((proof, _, _), stack) = (proof, goal), stack
350 module ProofEngineTacticals = Make (ProofEngineStatus)
352 include ProofEngineTacticals