1 (* Copyright (C) 2005, 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://helm.cs.unibo.it/
31 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
33 exception Error of string lazy_t
34 let fail msg = raise (Error msg)
38 type parameters = (string * string) list
42 type switch = Open of goal | Closed of goal
43 type locator = int * switch
44 type tag = [ `BranchTag | `FocusTag | `NoTag ]
45 type entry = locator list * locator list * locator list * tag * parameters
48 let empty = [ [], [], [], `NoTag , []]
50 let fold ~env ~cont ~todo init stack =
51 let rec aux acc depth =
54 | (locs, todos, conts, tag, _p) :: tl ->
55 let acc = List.fold_left (fun acc -> env acc depth tag) acc locs in
56 let acc = List.fold_left (fun acc -> cont acc depth tag) acc conts in
57 let acc = List.fold_left (fun acc -> todo acc depth tag) acc todos in
58 aux acc (depth + 1) tl
63 let iter ~env ~cont ~todo =
64 fold ~env:(fun _ -> env) ~cont:(fun _ -> cont) ~todo:(fun _ -> todo) ()
66 let map ~env ~cont ~todo =
67 let depth = ref ~-1 in
69 (fun (s, t, c, tag, p) ->
72 env d tag s, todo d tag t, cont d tag c, tag, p)
74 let is_open = function _, Open _ -> true | _ -> false
75 let close = function n, Open g -> n, Closed g | l -> l
76 let filter_open = List.filter is_open
78 function n, Open _ when n > 0 -> true | _,Closed _ -> true | _ -> false
79 let goal_of_loc = function _, Open g | _, Closed g -> g
80 let goal_of_switch = function Open g | Closed g -> g
81 let switch_of_loc = snd
83 let zero_pos = List.map (fun g -> 0, Open g)
86 let pos = ref 0 in (* positions are 1-based *)
87 List.map (function _, sw -> incr pos; !pos, sw) locs
92 | [] -> fail (lazy (sprintf "relative position %d not found" i))
93 | (i', _) as loc :: tl when i = i' -> loc, (List.rev acc) @ tl
94 | hd :: tl -> aux (hd :: acc) tl
100 List.map (fun l -> if List.mem (goal_of_loc l) gs then close l else l)
102 let rm _ _ = List.filter (fun l -> not (List.mem (goal_of_loc l) gs)) in
103 map ~env:close ~cont:rm ~todo:rm
107 | [] -> raise (Failure "Continuationals.find_goal")
108 | (l :: _, _ , _ , _, _) :: _ -> goal_of_loc l
109 | ( _ , _ , l :: _, _, _) :: _ -> goal_of_loc l
110 | ( _ , l :: _, _ , _, _) :: _ -> goal_of_loc l
111 | _ :: tl -> find_goal tl
116 | [ [], [], [], `NoTag , _] -> true
119 let of_nmetasenv metasenv =
120 let goals = List.map (fun (g, _) -> g) metasenv in
121 [ zero_pos goals, [], [], `NoTag , []]
125 | (locs, _, _, _, _) :: _ -> List.map switch_of_loc locs
130 | (locs, _, _, _, _) :: _ -> List.map goal_of_loc locs
135 | (_, _, _, tag, _) :: _ -> tag
140 | _ :: (locs, _, _, _, _) :: _ -> List.map goal_of_loc locs
144 let open_goals stack =
145 let add_open acc _ _ l = if is_open l then goal_of_loc l :: acc else acc in
146 List.rev (fold ~env:add_open ~cont:add_open ~todo:add_open [] stack)
148 let (@+) = (@) (* union *)
150 let (@-) s1 s2 = (* difference *)
152 (fun e acc -> if List.mem e s2 then acc else e :: acc)
155 let (@~-) locs gs = (* remove some goals from a locators list *)
157 (fun loc acc -> if List.mem (goal_of_loc loc) gs then acc else loc :: acc)
161 let pp_goal = string_of_int in
163 function Open g -> "o" ^ pp_goal g | Closed g -> "c" ^ pp_goal g
165 let pp_loc (i, s) = string_of_int i ^ pp_switch s in
166 let pp_env env = sprintf "[%s]" (String.concat ";" (List.map pp_loc env)) in
167 let pp_tag = function `BranchTag -> "B" | `FocusTag -> "F" | `NoTag -> "N" in
168 let pp_par = function [] -> "" | _ as l -> List.fold_left (fun acc (k,v) -> acc ^ "K: " ^ k ^ " V: " ^ v ^ "; ") "" l in
169 let pp_stack_entry (env, todo, cont, tag, parameters) =
170 sprintf "(%s, %s, %s, %s, %s)" (pp_env env) (pp_env todo) (pp_env cont)
171 (pp_tag tag) (pp_par parameters)
173 String.concat " :: " (List.map pp_stack_entry stack)
182 val mk_tactic : (input_status -> output_status) -> tactic
183 val apply_tactic : tactic -> input_status -> output_status
185 val goals : output_status -> goal list * goal list (** opened, closed goals *)
186 val get_stack : input_status -> Stack.t
187 val set_stack : Stack.t -> output_status -> output_status
189 val inject : input_status -> output_status
190 val focus : goal -> output_status -> input_status
216 | Tactical of tactical
218 val eval: t -> input_status -> output_status
221 module Make (S: Status) =
225 type input_status = S.input_status
226 type output_status = S.output_status
227 type tactic = S.tactic
243 | Tactical of tactical
248 | Semicolon -> "Semicolon"
251 | Pos i -> "Pos " ^ (String.concat "," (List.map string_of_int i))
252 | Wildcard -> "Wildcard"
255 sprintf "Focus [%s]" (String.concat "; " (List.map string_of_int gs))
256 | Unfocus -> "Unfocus"
257 | Tactical _ -> "Tactical <abs>"
259 let eval_tactical tactical ostatus switch =
260 match tactical, switch with
261 | Tactic tac, Open n ->
262 let ostatus = S.apply_tactic tac (S.focus n ostatus) in
263 let opened, closed = S.goals ostatus in
264 ostatus, opened, closed
265 | Skip, Closed n -> ostatus, [], [n]
266 | Tactic _, Closed _ -> fail (lazy "can't apply tactic to a closed goal")
267 | Skip, Open _ -> fail (lazy "can't skip an open goal")
269 let eval cmd istatus =
270 let stack = S.get_stack istatus in
271 debug_print (lazy (sprintf "EVAL CONT %s <- %s" (pp_t cmd) (pp stack)));
272 let new_stack stack = S.inject istatus, stack in
274 match cmd, stack with
275 | _, [] -> assert false
276 | Tactical tac, (g, t, k, tag, p) :: s ->
277 (* COMMENTED OUT TO ALLOW PARAMODULATION TO DO A
278 * auto paramodulation.try assumption.
279 * EVEN IF NO GOALS ARE LEFT OPEN BY AUTO.
281 if g = [] then fail (lazy "can't apply a tactic to zero goals");
284 debug_print (lazy ("context length " ^string_of_int (List.length g)));
285 let rec aux s go gc =
289 debug_print (lazy "inner eval tactical");
291 if List.exists ((=) (goal_of_loc loc)) gc then
294 let s, go', gc' = eval_tactical tac s (switch_of_loc loc) in
295 s, (go @- gc') @+ go', gc @+ gc'
299 let s0, go0, gc0 = S.inject istatus, [], [] in
300 let sn, gon, gcn = aux s0 go0 gc0 g in
301 debug_print (lazy ("opened: "
302 ^ String.concat " " (List.map string_of_int gon)));
303 debug_print (lazy ("closed: "
304 ^ String.concat " " (List.map string_of_int gcn)));
306 (zero_pos gon, t @~- gcn, k @~- gcn, tag, p) :: deep_close gcn s
309 | Dot, ([], _, [], _, _) :: _ ->
310 (* backward compatibility: do-nothing-dot *)
312 | Dot, (g, t, k, tag, p) :: s ->
313 (match filter_open g, k with
314 | loc :: loc_tl, _ -> new_stack (([ loc ], t, loc_tl @+ k, tag, p) :: s)
316 assert (is_open loc);
317 new_stack (([ loc ], t, k, tag, p) :: s)
318 | _ -> fail (lazy "can't use \".\" here"))
319 | Semicolon, _ -> new_stack stack
320 | Branch, (g, t, k, tag, p) :: s ->
321 (match init_pos g with
322 | [] | [ _ ] -> fail (lazy "too few goals to branch");
325 (([ loc ], [], [], `BranchTag, []) :: (loc_tl, t, k, tag,p) :: s))
326 | Shift, (g, t, k, `BranchTag, p) :: (g', t', k', tag, p') :: s ->
328 | [] -> fail (lazy "no more goals to shift")
331 (([ loc ], t @+ filter_open g @+ k, [],`BranchTag, p)
332 :: (loc_tl, t', k', tag, p') :: s))
333 | Shift, _ -> fail (lazy "can't shift goals here")
334 | Pos i_s, ([ loc ], t, [],`BranchTag, p) :: (g', t', k', tag, p') :: s
336 let l_js = List.filter (fun (i, _) -> List.mem i i_s) ([loc] @+ g') in
338 ((l_js, t , [],`BranchTag, p)
339 :: (([ loc ] @+ g') @- l_js, t', k', tag, p') :: s)
340 | Pos _, _ -> fail (lazy "can't use relative positioning here")
341 | Wildcard, ([ loc ] , t, [], `BranchTag, p) :: (g', t', k', tag, p') :: s
344 (([loc] @+ g', t, [], `BranchTag, p)
345 :: ([], t', k', tag, p') :: s)
346 | Wildcard, _ -> fail (lazy "can't use wildcard here")
347 | Merge, (g, t, k,`BranchTag,_) :: (g', t', k', tag,p') :: s ->
348 new_stack ((t @+ filter_open g @+ g' @+ k, t', k', tag, p') :: s)
349 | Merge, _ -> fail (lazy "can't merge goals here")
350 | Focus [], _ -> assert false
353 let add_l acc _ _ l = if is_open l then l :: acc else acc in
354 Stack.fold ~env:add_l ~cont:add_l ~todo:add_l [] s
358 if not (List.exists (fun l -> goal_of_loc l = g) stack_locs) then
359 fail (lazy (sprintf "goal %d not found (or closed)" g)))
361 new_stack ((zero_pos gs, [], [], `FocusTag, []) :: deep_close gs s)
362 | Unfocus, ([], [], [], `FocusTag, _) :: s -> new_stack s
363 | Unfocus, _ -> fail (lazy "can't unfocus, some goals are still open")
365 debug_print (lazy (sprintf "EVAL CONT %s -> %s" (pp_t cmd) (pp stack)));
366 S.set_stack stack ostatus