- proof,
- union (complementary newclosed opened) newopened,
- union closed newclosed
- ) (proof, [],[]) env
- in
- let pos = ref 0 in
- let stack_opened = List.map (fun g -> incr pos; !pos, g) opened in
- proof,
- (open_all stack_opened,
- complementary closed todo,
- complementary opened left, tag)
- :: map_stack
- (close closed) (complementary closed) (complementary opened) tail
- | Semicolon, (proof, stack) -> proof, stack
- | Dot, (proof, (env, todo, left, tag)::tail) ->
- let env, left =
- match List.filter is_open env, left with
- | [], [] -> raise (Error (lazy "There is nothig to do for '.'"))
- | g::env,left -> [g], union (List.map goal_of env) left
- | [], g::left -> [dummy_pos, Open g], left
- in
- proof, (env, todo, left, tag)::tail
- | Branch, (proof, (g1::tl, todo, left, tag)::tail) ->
- assert (List.length tl >= 1);
- proof, ([g1], [], [], BranchTag)::(tl, todo, left, tag)::tail
- | Branch, (_, _) -> raise (Error (lazy "can't branch on a singleton context"))
- | Shift opt_pos, (proof, (leftopen, t, l,BranchTag)::
- (goals, todo, left,tag)::tail) ->
- let next_goal, rem_goals =
- match opt_pos, goals with
- | None, g1 :: tl -> g1, tl
- | Some pos, _ ->
- (try
- list_assoc_extract pos goals
- with Not_found -> raise (Error (lazy (sprintf "position %d not found" pos))))
- | None, [] -> raise (Error (lazy "no more goals to shift"))
- in
- let t =
- union t (union (List.map goal_of (List.filter is_open leftopen)) l)
- in
- proof, ([next_goal], t, [], BranchTag)::(rem_goals, todo,left,tag)::tail
- | Shift _, (_, _) -> raise (Error (lazy "no more goals to shift"))
- | Select gl, (proof, stack) ->
- List.iter
- (fun g ->
- if E.is_goal_closed g proof then
- raise (Error (lazy "you can't select a closed goal")))
- gl;
- (proof, (open_all (map_dummy_pos gl),[],[],SelectTag)::stack)
- | End, (proof, stack) ->
- (match stack with
- | ([], [], [], SelectTag)::tail -> proof, tail
- | (leftopen,t,l,BranchTag)::(not_processed,todo,left,tag)::tail ->
- let env =
- (union (open_all (map_dummy_pos t))
- (union (open_all (map_dummy_pos l))
- (union not_processed (List.filter is_open leftopen))))
- in
- proof, (env,todo,left,tag)::tail
- | _ -> raise (Error (lazy "can't end here")))
-
- let init proof =
- proof,
- [ map_open_pos (E.goals_of_proof proof), [], [], NoTag ]
-
- let is_completed =
- function
- | (_, [[],[],[],NoTag]) -> true
- | _ -> false
+ aux s go gc loc_tl
+ in
+ let s0, go0, gc0 = S.inject istatus, [], [] in
+ let sn, gon, gcn = aux s0 go0 gc0 g in
+ debug_print (lazy ("opened: "
+ ^ String.concat " " (List.map string_of_int gon)));
+ debug_print (lazy ("closed: "
+ ^ String.concat " " (List.map string_of_int gcn)));
+ let stack =
+ (zero_pos gon, t @~- gcn, k @~- gon, tag) :: deep_close gcn s
+ in
+ sn, stack
+ | Dot, ([], _, [], _) :: _ ->
+ (* backward compatibility: do-nothing-dot *)
+ new_stack stack
+ | Dot, (g, t, k, tag) :: s ->
+ (match filter_open g, k with
+ | loc :: loc_tl, _ -> new_stack (([ loc ], t, loc_tl @+ k, tag) :: s)
+ | [], loc :: k ->
+ assert (is_open loc);
+ new_stack (([ loc ], t, k, tag) :: s)
+ | _ -> fail (lazy "can't use \".\" here"))
+ | Semicolon, _ -> new_stack stack
+ | Branch, (g, t, k, tag) :: s ->
+ (match init_pos g with
+ | [] | [ _ ] -> fail (lazy "too few goals to branch");
+ | loc :: loc_tl ->
+ new_stack
+ (([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s))
+ | Shift, (g, t, k, `BranchTag) :: (g', t', k', tag) :: s ->
+ (match g' with
+ | [] -> fail (lazy "no more goals to shift")
+ | loc :: loc_tl ->
+ new_stack
+ (([ loc ], t @+ filter_open g, [],`BranchTag)
+ :: (loc_tl, t', k', tag) :: s))
+ | Shift, _ -> fail (lazy "can't shift goals here")
+ | Pos i, ([ loc ], [], [],`BranchTag) :: (g', t', k', tag) :: s
+ when is_fresh loc ->
+ let loc_i, g' = extract_pos i g' in
+ new_stack
+ (([ loc_i ], [], [],`BranchTag)
+ :: ([ loc ] @+ g', t', k', tag) :: s)
+ | Pos i, (g, t, k,`BranchTag) :: (g', t', k', tag) :: s ->
+ let loc_i, g' = extract_pos i g' in
+ new_stack
+ (([ loc_i ], [], [],`BranchTag)
+ :: (g', t' @+ filter_open g, k', tag) :: s)
+ | Pos _, _ -> fail (lazy "can't use relative positioning here")
+ | Merge, (g, t, k,`BranchTag) :: (g', t', k', tag) :: s ->
+ new_stack ((t @+ filter_open g @+ g' @+ k, t', k', tag) :: s)
+ | Merge, _ -> fail (lazy "can't merge goals here")
+ | Focus [], _ -> assert false
+ | Focus gs, s ->
+ let stack_locs =
+ let add_l acc _ _ l = if is_open l then l :: acc else acc in
+ Stack.fold ~env:add_l ~cont:add_l ~todo:add_l [] s
+ in
+ List.iter
+ (fun g ->
+ if not (List.exists (fun l -> goal_of_loc l = g) stack_locs) then
+ fail (lazy (sprintf "goal %d not found (or closed)" g)))
+ gs;
+ new_stack ((zero_pos gs, [], [], `FocusTag) :: deep_close gs s)
+ | Unfocus, ([], [], [], `FocusTag) :: s -> new_stack s
+ | Unfocus, _ -> fail (lazy "can't unfocus, some goals are still open")
+ in
+ debug_print (lazy (sprintf "EVAL CONT %s -> %s" (pp_t cmd) (pp stack)));
+ S.set_stack stack ostatus