]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/tactics/tacticals.ml
matitadep: we now handle the inline of an uri, we removed the -exclude option
[helm.git] / helm / software / components / tactics / 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 (* $Id$ *)
27
28 (* open CicReduction
29 open ProofEngineTypes
30 open UriManager *)
31
32 (** DEBUGGING *)
33
34   (** perform debugging output? *)
35 let debug = false
36 let debug_print = fun _ -> ()
37
38   (** debugging print *)
39 let info s = debug_print (lazy ("TACTICALS INFO: " ^ (Lazy.force s)))
40
41 module PET = ProofEngineTypes
42
43 let id_tac = 
44  let id_tac (proof,goal) = 
45   let _, metasenv, _subst, _, _, _ = proof in
46   let _, _, _ = CicUtil.lookup_meta goal metasenv in
47   (proof,[goal])
48  in 
49   PET.mk_tactic id_tac
50
51 let fail_tac =
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"))
56  in
57   PET.mk_tactic fail_tac
58
59 type goal = PET.goal
60
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)
68   in
69   let remove =
70     List.fold_left
71       (fun remove e -> if List.mem e after then remove else e :: remove)
72       [] before
73   in
74   let add =
75     List.fold_left
76       (fun add e -> if List.mem e before then add else e :: add)
77       []
78       after
79   in
80   let add, remove = (* adds goals which have been both opened _and_ closed *)
81     List.fold_left
82       (fun (add, remove) opened_goal ->
83         if List.mem opened_goal before
84         then opened_goal :: add, opened_goal :: remove
85         else add, remove)
86       (add, remove)
87       opened
88   in
89   sort_opened opened add, remove
90
91 module ProofEngineStatus =
92 struct
93   module Stack = Continuationals.Stack
94
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). *)
103   type input_status =
104     PET.status (* (proof, goal) *) * Stack.t
105
106   type output_status =
107     (PET.proof * goal list * goal list) * Stack.t
108
109   type tactic = PET.tactic
110
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 *)
114   let mk_tactic f =
115     PET.mk_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
121         proof, opened)
122
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
130
131   let goals ((_, opened, closed), _) = opened, closed
132
133   (* Done only at the beginning of the eval of the machine *)
134   let get_stack = snd
135   (* Done only at the end of the eval of the machine *)
136   let set_stack stack (opstatus, _) = opstatus, stack
137
138   let inject ((proof, _), stack) = ((proof, [], []), stack)
139   let focus goal ((proof, _, _), stack) = (proof, goal), stack
140 end
141
142 module S = ProofEngineStatus
143 module C = Continuationals.Make (S)
144
145 type tactic = S.tactic
146
147 let fold_eval status ts =
148   let istatus =
149     List.fold_left (fun istatus t -> S.focus ~-1 (C.eval t istatus)) status ts
150   in
151   S.inject istatus
152
153 (* Tacticals implemented on top of tynycals *)
154
155 let thens ~start ~continuations =
156   S.mk_tactic
157     (fun istatus ->
158       fold_eval istatus
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))
162         @ [ C.Merge ]))
163
164 let then_ ~start ~continuation =
165   S.mk_tactic
166     (fun istatus ->
167       let ostatus = C.eval (C.Tactical (C.Tactic start)) istatus in
168       let opened,closed = S.goals ostatus in
169        match opened with
170           [] -> ostatus
171         | _ ->
172           fold_eval (S.focus ~-1 ostatus)
173             [ C.Semicolon;
174               C.Tactical (C.Tactic continuation) ])
175
176 let seq ~tactics =
177   S.mk_tactic
178     (fun istatus ->
179       fold_eval istatus
180         (HExtlib.list_concat ~sep:[ C.Semicolon ]
181           (List.map (fun t -> [ C.Tactical (C.Tactic t) ]) tactics)))
182
183 (* Tacticals that cannot be implemented on top of tynycals *)
184
185 let const_tac res = PET.mk_tactic (fun _ -> res)
186
187 let if_ ~start ~continuation ~fail =
188    let if_ status =
189       let xoutput = 
190          try
191             let result = PET.apply_tactic start status in
192             info (lazy ("Tacticals.if_: succedeed!!!"));
193             Some result 
194          with PET.Fail _ -> None
195       in
196       let tactic = match xoutput with
197          | Some res -> then_ ~start:(const_tac res) ~continuation
198          | None     -> fail
199       in 
200       PET.apply_tactic tactic status
201    in
202    PET.mk_tactic if_
203
204 let ifs ~start ~continuations ~fail =
205    let ifs status =
206       let xoutput = 
207          try
208             let result = PET.apply_tactic start status in
209             info (lazy ("Tacticals.ifs: succedeed!!!"));
210             Some result 
211          with PET.Fail _ -> None
212       in
213       let tactic = match xoutput with
214          | Some res -> thens ~start:(const_tac res) ~continuations
215          | None     -> fail
216       in 
217       PET.apply_tactic tactic status
218    in
219    PET.mk_tactic ifs
220
221 let first ~tactics =
222   let rec first ~(tactics: tactic list) status =
223     info (lazy "in Tacticals.first");
224     match tactics with
225       [] -> raise (PET.Fail (lazy "first: no tactics left"))
226     | tac::tactics ->
227         try
228          let res = PET.apply_tactic tac status in
229           info (lazy ("Tacticals.first: succedeed!!!"));
230           res
231         with 
232          PET.Fail _ -> first ~tactics status
233   in
234   PET.mk_tactic (first ~tactics)
235
236 let rec do_tactic ~n ~tactic =
237  PET.mk_tactic
238   (function status ->
239     if n = 0 then
240      PET.apply_tactic id_tac status
241     else
242      PET.apply_tactic
243       (then_ ~start:tactic ~continuation:(do_tactic ~n:(n-1) ~tactic))
244       status)
245
246 (* This applies tactic and catches its possible failure *)
247 let try_tactic ~tactic =
248  let try_tactic status =
249   try
250     PET.apply_tactic tactic status
251   with (PET.Fail _) as e -> 
252     info (lazy (
253       "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e));
254     PET.apply_tactic id_tac status
255  in
256   PET.mk_tactic try_tactic
257
258 let rec repeat_tactic ~tactic =
259  ProofEngineTypes.mk_tactic
260   (fun status ->
261     ProofEngineTypes.apply_tactic
262      (then_ ~start:tactic
263        ~continuation:(try_tactic (repeat_tactic ~tactic))) status)
264
265 (* This tries tactics until one of them solves the goal *)
266 let solve_tactics ~tactics =
267  let rec solve_tactics ~(tactics: tactic list) status =
268   info (lazy "in Tacticals.solve_tactics");
269   match tactics with
270   | currenttactic::moretactics ->
271       (try
272         let (proof, opened) as output_status =
273          PET.apply_tactic currenttactic status 
274         in
275         match opened with 
276           | [] -> info (lazy ("Tacticals.solve_tactics: solved the goal!!!"));
277                   output_status
278           | _ -> info (lazy ("Tacticals.solve_tactics: try the next tactic"));
279                  raise (PET.Fail (lazy "Goal not solved"))
280        with (PET.Fail _) as e ->
281          info (lazy (
282             "Tacticals.solve_tactics: current tactic failed with exn: "
283             ^ Printexc.to_string e));
284          solve_tactics ~tactics:moretactics status)
285   | [] ->
286       raise (PET.Fail
287         (lazy "solve_tactics cannot solve the goal"))
288  in
289   PET.mk_tactic (solve_tactics ~tactics)
290
291 let progress_tactic ~tactic =
292   let msg = lazy "Failed to progress" in
293   let progress_tactic (((_,metasenv,_subst,_,_,_),g) as istatus) =
294     let ((_,metasenv',_subst,_,_,_),opened) as ostatus =
295      PET.apply_tactic tactic istatus
296     in
297     match opened with
298     | [g1] ->
299         let _,oc,oldty = CicUtil.lookup_meta g metasenv in
300         let _,nc,newty = CicUtil.lookup_meta g1 metasenv' in
301         if oldty = newty && oc = nc then
302           raise (PET.Fail msg)
303         else
304           ostatus
305     | _ -> ostatus
306   in
307   PET.mk_tactic progress_tactic