]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/tactics/continuationals.ml
- transcript: patched to generate CoRN_notation.ma instead of CoRN.ma
[helm.git] / helm / software / components / tactics / continuationals.ml
1 (* Copyright (C) 2005, 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://helm.cs.unibo.it/
24  *)
25
26 (* $Id$ *)
27
28 open Printf
29
30 let debug = false
31 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
32
33 exception Error of string lazy_t
34 let fail msg = raise (Error msg)
35
36 type goal = ProofEngineTypes.goal
37
38 module Stack =
39 struct
40   type switch = Open of goal | Closed of goal
41   type locator = int * switch
42   type tag = [ `BranchTag | `FocusTag | `NoTag ]
43   type entry = locator list * locator list * locator list * tag
44   type t = entry list
45
46   let empty = [ [], [], [], `NoTag ]
47
48   let fold ~env ~cont ~todo init stack =
49     let rec aux acc depth =
50       function
51       | [] -> acc
52       | (locs, todos, conts, tag) :: tl ->
53           let acc = List.fold_left (fun acc -> env acc depth tag)  acc locs in
54           let acc = List.fold_left (fun acc -> cont acc depth tag) acc conts in
55           let acc = List.fold_left (fun acc -> todo acc depth tag) acc todos in
56           aux acc (depth + 1) tl
57     in
58     assert (stack <> []);
59     aux init 0 stack
60
61   let iter ~env ~cont ~todo =
62     fold ~env:(fun _ -> env) ~cont:(fun _ -> cont) ~todo:(fun _ -> todo) ()
63
64   let map ~env ~cont ~todo =
65     let depth = ref ~-1 in
66     List.map
67       (fun (s, t, c, tag) ->
68         incr depth;
69         let d = !depth in
70         env d tag s, todo d tag t, cont d tag c, tag)
71
72   let is_open = function _, Open _ -> true | _ -> false
73   let close = function n, Open g -> n, Closed g | l -> l
74   let filter_open = List.filter is_open
75   let is_fresh = function n, Open _ when n > 0 -> true | _ -> false
76   let goal_of_loc = function _, Open g | _, Closed g -> g
77   let goal_of_switch = function Open g | Closed g -> g
78   let switch_of_loc = snd
79
80   let zero_pos = List.map (fun g -> 0, Open g)
81
82   let init_pos locs =
83     let pos = ref 0 in  (* positions are 1-based *)
84     List.map (function _, sw -> incr pos; !pos, sw) locs
85
86   let extract_pos i =
87     let rec aux acc =
88       function
89       | [] -> fail (lazy (sprintf "relative position %d not found" i))
90       | (i', _) as loc :: tl when i = i' -> loc, (List.rev acc) @ tl
91       | hd :: tl -> aux (hd :: acc) tl
92     in
93     aux []
94
95   let deep_close gs =
96     let close _ _ =
97       List.map (fun l -> if List.mem (goal_of_loc l) gs then close l else l)
98     in
99     let rm _ _ = List.filter (fun l -> not (List.mem (goal_of_loc l) gs)) in
100     map ~env:close ~cont:rm ~todo:rm
101
102   let rec find_goal =
103     function
104     | [] -> raise (Failure "Continuationals.find_goal")
105     | (l :: _,   _   ,   _   , _) :: _ -> goal_of_loc l
106     | (  _   ,   _   , l :: _, _) :: _ -> goal_of_loc l
107     | (  _   , l :: _,   _   , _) :: _ -> goal_of_loc l
108     | _ :: tl -> find_goal tl
109
110   let is_empty =
111     function
112     | [] -> assert false
113     | [ [], [], [], `NoTag ] -> true
114     | _ -> false
115
116   let of_metasenv metasenv =
117     let goals = List.map (fun (g, _, _) -> g) metasenv in
118     [ zero_pos goals, [], [], `NoTag ]
119
120   let head_switches =
121     function
122     | (locs, _, _, _) :: _ -> List.map switch_of_loc locs
123     | [] -> assert false
124
125   let head_goals =
126     function
127     | (locs, _, _, _) :: _ -> List.map goal_of_loc locs
128     | [] -> assert false
129
130   let head_tag =
131     function
132     | (_, _, _, tag) :: _ -> tag
133     | [] -> assert false
134
135   let shift_goals =
136     function
137     | _ :: (locs, _, _, _) :: _ -> List.map goal_of_loc locs
138     | [] -> assert false
139     | _ -> []
140
141   let open_goals stack =
142     let add_open acc _ _ l = if is_open l then goal_of_loc l :: acc else acc in
143     List.rev (fold ~env:add_open ~cont:add_open ~todo:add_open [] stack)
144
145   let (@+) = (@)  (* union *)
146
147   let (@-) s1 s2 =  (* difference *)
148     List.fold_right
149       (fun e acc -> if List.mem e s2 then acc else e :: acc)
150       s1 []
151
152   let (@~-) locs gs = (* remove some goals from a locators list *)
153     List.fold_right
154       (fun loc acc -> if List.mem (goal_of_loc loc) gs then acc else loc :: acc)
155       locs []
156
157   let pp stack =
158     let pp_goal = string_of_int in
159     let pp_switch =
160       function Open g -> "o" ^ pp_goal g | Closed g -> "c" ^ pp_goal g
161     in
162     let pp_loc (i, s) = string_of_int i ^ pp_switch s in
163     let pp_env env = sprintf "[%s]" (String.concat ";" (List.map pp_loc env)) in
164     let pp_tag = function `BranchTag -> "B" | `FocusTag -> "F" | `NoTag -> "N" in
165     let pp_stack_entry (env, todo, cont, tag) =
166       sprintf "(%s, %s, %s, %s)" (pp_env env) (pp_env todo) (pp_env cont)
167         (pp_tag tag)
168     in
169     String.concat " :: " (List.map pp_stack_entry stack)
170 end
171
172 module type Status =
173 sig
174   type input_status
175   type output_status
176
177   type tactic
178
179   val id_tactic : tactic
180   val mk_tactic : (input_status -> output_status) -> tactic
181   val apply_tactic : tactic -> input_status -> output_status
182
183   val get_status: input_status -> ProofEngineTypes.status
184   val get_proof: output_status -> ProofEngineTypes.proof
185   val goals : output_status -> goal list * goal list (** opened, closed goals *)
186   val set_goals: goal list * goal list -> output_status -> output_status
187   val get_stack : input_status -> Stack.t
188   val set_stack : Stack.t -> output_status -> output_status
189
190   val inject : input_status -> output_status
191   val focus : goal -> output_status -> input_status
192 end
193
194 module type C =
195 sig
196   type input_status
197   type output_status
198   type tactic
199
200   type tactical =
201     | Tactic of tactic
202     | Skip
203
204   type t =
205     | Dot
206     | Semicolon
207
208     | Branch
209     | Shift
210     | Pos of int list
211     | Wildcard
212     | Merge
213
214     | Focus of goal list
215     | Unfocus
216
217     | Tactical of tactical
218
219   val eval: t -> input_status -> output_status
220 end
221
222 module Make (S: Status) =
223 struct
224   open Stack
225
226   type input_status = S.input_status
227   type output_status = S.output_status
228   type tactic = S.tactic
229
230   type tactical =
231     | Tactic of tactic
232     | Skip
233
234   type t =
235     | Dot
236     | Semicolon
237     | Branch
238     | Shift
239     | Pos of int list
240     | Wildcard
241     | Merge
242     | Focus of goal list
243     | Unfocus
244     | Tactical of tactical
245
246   let pp_t =
247     function
248     | Dot -> "Dot"
249     | Semicolon -> "Semicolon"
250     | Branch -> "Branch"
251     | Shift -> "Shift"
252     | Pos i -> "Pos " ^ (String.concat "," (List.map string_of_int i))
253     | Wildcard -> "Wildcard"
254     | Merge -> "Merge"
255     | Focus gs ->
256         sprintf "Focus [%s]" (String.concat "; " (List.map string_of_int gs))
257     | Unfocus -> "Unfocus"
258     | Tactical _ -> "Tactical <abs>"
259
260   let eval_tactical tactical ostatus switch =
261     match tactical, switch with
262     | Tactic tac, Open n ->
263         let ostatus = S.apply_tactic tac (S.focus n ostatus) in
264         let opened, closed = S.goals ostatus in
265         ostatus, opened, closed
266     | Skip, Closed n -> ostatus, [], [n]
267     | Tactic _, Closed _ -> fail (lazy "can't apply tactic to a closed goal")
268     | Skip, Open _ -> fail (lazy "can't skip an open goal")
269
270   let eval cmd istatus =
271     let stack = S.get_stack istatus in
272     debug_print (lazy (sprintf "EVAL CONT %s <- %s" (pp_t cmd) (pp stack)));
273     let new_stack stack = S.inject istatus, stack in
274     let ostatus, stack =
275       match cmd, stack with
276       | _, [] -> assert false
277       | Tactical tac, (g, t, k, tag) :: s ->
278 (* COMMENTED OUT TO ALLOW PARAMODULATION TO DO A 
279  *   auto paramodulation.try assumption.
280  * EVEN IF NO GOALS ARE LEFT OPEN BY AUTO.
281   
282   if g = [] then fail (lazy "can't apply a tactic to zero goals");
283   
284 *)
285           debug_print (lazy ("context length " ^string_of_int (List.length g)));
286           let rec aux s go gc =
287             function
288             | [] -> s, go, gc
289             | loc :: loc_tl ->
290                 debug_print (lazy "inner eval tactical");
291                 let s, go, gc =
292                   if List.exists ((=) (goal_of_loc loc)) gc then
293                     s, go, gc
294                   else
295                     let s, go', gc' = eval_tactical tac s (switch_of_loc loc) in
296                     s, (go @- gc') @+ go', gc @+ gc'
297                 in
298                 aux s go gc loc_tl
299           in
300           let s0, go0, gc0 = S.inject istatus, [], [] in
301           let sn, gon, gcn = aux s0 go0 gc0 g in
302           debug_print (lazy ("opened: "
303             ^ String.concat " " (List.map string_of_int gon)));
304           debug_print (lazy ("closed: "
305             ^ String.concat " " (List.map string_of_int gcn)));
306           let stack =
307             (zero_pos gon, t @~- gcn, k @~- gcn, tag) :: deep_close gcn s
308           in
309           sn, stack
310       | Dot, ([], _, [], _) :: _ ->
311           (* backward compatibility: do-nothing-dot *)
312           new_stack stack
313       | Dot, (g, t, k, tag) :: s ->
314           (match filter_open g, k with
315           | loc :: loc_tl, _ -> new_stack (([ loc ], t, loc_tl @+ k, tag) :: s)
316           | [], loc :: k ->
317               assert (is_open loc);
318               new_stack (([ loc ], t, k, tag) :: s)
319           | _ -> fail (lazy "can't use \".\" here"))
320       | Semicolon, _ -> new_stack stack
321       | Branch, (g, t, k, tag) :: s ->
322           (match init_pos g with
323           | [] | [ _ ] -> fail (lazy "too few goals to branch");
324           | loc :: loc_tl ->
325               new_stack
326                 (([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s))
327       | Shift, (g, t, k, `BranchTag) :: (g', t', k', tag) :: s ->
328           (match g' with
329           | [] -> fail (lazy "no more goals to shift")
330           | loc :: loc_tl ->
331               new_stack
332                 (([ loc ], t @+ filter_open g @+ k, [],`BranchTag)
333                 :: (loc_tl, t', k', tag) :: s))
334       | Shift, _ -> fail (lazy "can't shift goals here")
335       | Pos i_s, ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s
336         when is_fresh loc ->
337           let l_js = List.filter (fun (i, _) -> List.mem i i_s) ([loc] @+ g') in
338           new_stack
339             ((l_js, t , [],`BranchTag)
340              :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s)
341       | Pos _, _ -> fail (lazy "can't use relative positioning here")
342       | Wildcard, ([ loc ] , t, [], `BranchTag) :: (g', t', k', tag) :: s
343           when is_fresh loc ->
344             new_stack
345               (([loc] @+ g', t, [], `BranchTag)
346                 :: ([], t', k', tag) :: s)
347       | Wildcard, _ -> fail (lazy "can't use wildcard here")
348       | Merge, (g, t, k,`BranchTag) :: (g', t', k', tag) :: s ->
349           new_stack ((t @+ filter_open g @+ g' @+ k, t', k', tag) :: s)
350       | Merge, _ -> fail (lazy "can't merge goals here")
351       | Focus [], _ -> assert false
352       | Focus gs, s ->
353           let stack_locs =
354             let add_l acc _ _ l = if is_open l then l :: acc else acc in
355             Stack.fold ~env:add_l ~cont:add_l ~todo:add_l [] s
356           in
357           List.iter
358             (fun g ->
359               if not (List.exists (fun l -> goal_of_loc l = g) stack_locs) then
360                 fail (lazy (sprintf "goal %d not found (or closed)" g)))
361             gs;
362           new_stack ((zero_pos gs, [], [], `FocusTag) :: deep_close gs s)
363       | Unfocus, ([], [], [], `FocusTag) :: s -> new_stack s
364       | Unfocus, _ -> fail (lazy "can't unfocus, some goals are still open")
365     in
366     debug_print (lazy (sprintf "EVAL CONT %s -> %s" (pp_t cmd) (pp stack)));
367     S.set_stack stack ostatus
368 end
369