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)))
41 module PET = ProofEngineTypes
44 let id_tac (proof,goal) =
45 let _, metasenv, _subst, _, _, _ = proof in
46 let _, _, _ = CicUtil.lookup_meta goal metasenv in
52 let fail_tac (proof,goal) =
53 let _, metasenv, _subst, _ , _, _ = proof in
54 let _, _, _ = CicUtil.lookup_meta goal metasenv in
55 raise (PET.Fail (lazy "fail tactical"))
57 PET.mk_tactic fail_tac
61 (** TODO needed until tactics start returning both opened and closed goals
62 * First part of the function performs a diff among goals ~before tactic
63 * application and ~after it. Second part will add as both opened and closed
64 * the goals which are returned as opened by the tactic *)
65 let goals_diff ~before ~after ~opened =
66 let sort_opened opened add =
67 opened @ (List.filter (fun g -> not (List.mem g opened)) add)
71 (fun remove e -> if List.mem e after then remove else e :: remove)
76 (fun add e -> if List.mem e before then add else e :: add)
80 let add, remove = (* adds goals which have been both opened _and_ closed *)
82 (fun (add, remove) opened_goal ->
83 if List.mem opened_goal before
84 then opened_goal :: add, opened_goal :: remove
89 sort_opened opened add, remove
91 module ProofEngineStatus =
93 module Stack = Continuationals.Stack
95 (* The stack is used and saved only at the very end of the eval function;
96 it is read only at the beginning of the eval;
97 we need it just to apply several times in a row this machine to an
98 initial stack, i.e. to chain several applications of the machine together,
99 i.e. to dump and restore the state of the machine.
100 The stack is never used by the tactics: each tactic of type
101 PET.tactic ignore the stack. To make a tactic from the eval function
102 of a machine we apply the eval on a fresh stack (via the mk_tactic). *)
104 PET.status (* (proof, goal) *) * Stack.t
107 (PET.proof * goal list * goal list) * Stack.t
109 type tactic = PET.tactic
111 (* f is an eval function of a machine;
112 the machine is applied to a fresh stack and the final stack is read
113 back to obtain the result of the tactic *)
116 (fun ((proof, goal) as pstatus) ->
117 let stack = [ [ 1, Stack.Open goal ], [], [], `NoTag ] in
118 let istatus = pstatus, stack in
119 let (proof, _, _), stack = f istatus in
120 let opened = Continuationals.Stack.open_goals stack in
123 (* it applies a tactic ignoring (and preserving) the stack *)
124 let apply_tactic tac ((proof, _) as pstatus, stack) =
125 let proof', opened = PET.apply_tactic tac pstatus in
126 let before = PET.goals_of_proof proof in
127 let after = PET.goals_of_proof proof' in
128 let opened_goals, closed_goals = goals_diff ~before ~after ~opened in
129 (proof', opened_goals, closed_goals), stack
131 let goals ((_, opened, closed), _) = opened, closed
133 (* Done only at the beginning of the eval of the machine *)
135 (* Done only at the end of the eval of the machine *)
136 let set_stack stack (opstatus, _) = opstatus, stack
138 let inject ((proof, _), stack) = ((proof, [], []), stack)
139 let focus goal ((proof, _, _), stack) = (proof, goal), stack
142 module S = ProofEngineStatus
143 module C = Continuationals.Make (S)
145 type tactic = S.tactic
147 let fold_eval status ts =
149 List.fold_left (fun istatus t -> S.focus ~-1 (C.eval t istatus)) status ts
153 (* Tacticals implemented on top of tynycals *)
155 let thens ~start ~continuations =
159 ([ C.Tactical (C.Tactic start); C.Branch ]
160 @ (HExtlib.list_concat ~sep:[ C.Shift ]
161 (List.map (fun t -> [ C.Tactical (C.Tactic t) ]) continuations))
164 let then_ ~start ~continuation =
167 let ostatus = C.eval (C.Tactical (C.Tactic start)) istatus in
168 let opened,closed = S.goals ostatus in
172 fold_eval (S.focus ~-1 ostatus)
174 C.Tactical (C.Tactic continuation) ])
180 (HExtlib.list_concat ~sep:[ C.Semicolon ]
181 (List.map (fun t -> [ C.Tactical (C.Tactic t) ]) tactics)))
183 let if_ ~start ~continuation ~fail =
188 let res = C.eval (C.Tactical (C.Tactic start)) istatus in
189 info (lazy ("Tacticals.if_: succedeed!!!"));
191 with PET.Fail _ -> None
195 let opened,closed = S.goals ostatus in
196 begin match opened with
199 fold_eval (S.focus ~-1 ostatus)
200 [ C.Semicolon; C.Tactical (C.Tactic continuation) ]
202 | None -> C.eval (C.Tactical (C.Tactic fail)) istatus
205 (* Tacticals that cannot be implemented on top of tynycals *)
208 let rec first ~(tactics: tactic list) status =
209 info (lazy "in Tacticals.first");
211 [] -> raise (PET.Fail (lazy "first: no tactics left"))
214 let res = PET.apply_tactic tac status in
215 info (lazy ("Tacticals.first: succedeed!!!"));
218 PET.Fail _ -> first ~tactics status
220 PET.mk_tactic (first ~tactics)
223 let rec do_tactic ~n ~tactic =
227 PET.apply_tactic id_tac status
230 (then_ ~start:tactic ~continuation:(do_tactic ~n:(n-1) ~tactic))
233 (* This applies tactic and catches its possible failure *)
234 let try_tactic ~tactic =
235 let try_tactic status =
237 PET.apply_tactic tactic status
238 with (PET.Fail _) as e ->
240 "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e));
241 PET.apply_tactic id_tac status
243 PET.mk_tactic try_tactic
245 let rec repeat_tactic ~tactic =
246 ProofEngineTypes.mk_tactic
248 ProofEngineTypes.apply_tactic
250 ~continuation:(try_tactic (repeat_tactic ~tactic))) status)
252 (* This tries tactics until one of them solves the goal *)
253 let solve_tactics ~tactics =
254 let rec solve_tactics ~(tactics: tactic list) status =
255 info (lazy "in Tacticals.solve_tactics");
257 | currenttactic::moretactics ->
259 let (proof, opened) as output_status =
260 PET.apply_tactic currenttactic status
263 | [] -> info (lazy ("Tacticals.solve_tactics: solved the goal!!!"));
265 | _ -> info (lazy ("Tacticals.solve_tactics: try the next tactic"));
266 raise (PET.Fail (lazy "Goal not solved"))
267 with (PET.Fail _) as e ->
269 "Tacticals.solve_tactics: current tactic failed with exn: "
270 ^ Printexc.to_string e));
271 solve_tactics ~tactics:moretactics status)
274 (lazy "solve_tactics cannot solve the goal"))
276 PET.mk_tactic (solve_tactics ~tactics)
278 let progress_tactic ~tactic =
279 let msg = lazy "Failed to progress" in
280 let progress_tactic (((_,metasenv,_subst,_,_,_),_) as istatus) =
281 let ((_,metasenv',_subst,_,_,_),_) as ostatus =
282 PET.apply_tactic tactic istatus
285 If just the index of some metas changes the tactic is recognized
286 as a progressing one. This is wrong. *)
287 if metasenv' = metasenv then
292 PET.mk_tactic progress_tactic