- metasenv,
- union (complementary newclosed opened) newopened,
- union closed newclosed
- ) (metasenv, [],[]) env
- in
- let pos = ref 0 in
- let stack_opened = List.map (fun g -> incr pos; !pos, g) opened in
- metasenv,
- (open_all stack_opened,
- complementary closed todo,
- complementary opened left)
- :: stack_map
- (close closed) (complementary closed) (complementary opened) tail
- | Semicolon, (metasenv, stack) -> metasenv, stack
- | Dot, (metasenv, (env, todo, left)::tail) ->
- let env, left =
- match L.filter is_open env, left with
- | [], [] -> raise (Error "There is nothig to do for '.'")
- | g::env,left -> [g], union (L.map goal_of env) left
- | [], g::left -> [dummy_pos, Open g], left
- in
- metasenv, (env, todo, left)::tail
- | Branch, (metasenv, (g1::tl, todo, left)::tail) ->
- assert (L.length tl >= 1);
- metasenv, ([g1], [], [])::(tl, todo, left)::tail
- | Branch, (_, _) -> raise (Error "can't branch on a singleton context")
- | Shift opt_pos, (metasenv, (leftopen, t, l)::(goals, todo, left)::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 (Printf.sprintf "position %d not found" pos)))
- | None, [] -> raise (Error "no more goals to shift")
- in
- let t = union t (union (L.map goal_of (L.filter is_open leftopen)) l) in
- metasenv, ([next_goal], t, [])::(rem_goals, todo,left)::tail
- | Shift _, (_, _) -> raise (Error "no more goals to shift")
- | Merge, (metasenv, (leftopen,t,l)::(not_processed,todo,left)::tail) ->
- let env =
- (union (open_all (map_dummy_pos t))
- (union (open_all (map_dummy_pos l))
- (union not_processed (L.filter is_open leftopen ))))
- in
- metasenv, (env,todo,left)::tail
- | Merge, (_, [_]) -> raise (Error "can't merge here")
- | Select gl, (metasenv, stack) ->
- List.iter
- (fun g -> if not (E.goal_mem g metasenv) then
- raise (Error "you can't select a closed goal")) gl;
- (metasenv, (open_all (map_dummy_pos gl),[],[])::stack)
- | End_select, (metasenv, stack) ->
- (match stack with
- | ([], [], [])::tail -> metasenv, tail
- | _ -> raise (Error "select left some goals open"))
- | Qed, (metasenv, [[], [], []]) -> status
- | Qed, _ -> raise (Error "can't qed an unfinished proof")
-
- let init metasenv =
- metasenv,
- [ map_open_pos (List.map E.goal_of_conjecture metasenv), [], [] ]
+ 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