+let debug = false
+let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
+
+exception Error of string lazy_t
+let fail msg = raise (Error msg)
+
+type goal = ProofEngineTypes.goal
+
+module Stack =
+struct
+ type switch = Open of goal | Closed of goal
+ type locator = int * switch
+ type tag = [ `BranchTag | `FocusTag | `NoTag ]
+ type entry = locator list * locator list * locator list * tag
+ type t = entry list
+
+ let empty = [ [], [], [], `NoTag ]
+
+ let fold ~env ~cont ~todo init stack =
+ let rec aux acc depth =
+ function
+ | [] -> acc
+ | (locs, todos, conts, tag) :: tl ->
+ let acc = List.fold_left (fun acc -> env acc depth tag) acc locs in
+ let acc = List.fold_left (fun acc -> cont acc depth tag) acc conts in
+ let acc = List.fold_left (fun acc -> todo acc depth tag) acc todos in
+ aux acc (depth + 1) tl
+ in
+ assert (stack <> []);
+ aux init 0 stack
+
+ let iter ~env ~cont ~todo =
+ fold ~env:(fun _ -> env) ~cont:(fun _ -> cont) ~todo:(fun _ -> todo) ()
+
+ let map ~env ~cont ~todo =
+ let depth = ref ~-1 in
+ List.map
+ (fun (s, t, c, tag) ->
+ incr depth;
+ let d = !depth in
+ env d tag s, todo d tag t, cont d tag c, tag)
+
+ let is_open = function _, Open _ -> true | _ -> false
+ let close = function n, Open g -> n, Closed g | l -> l
+ let filter_open = List.filter is_open
+ let is_fresh = function n, Open _ when n > 0 -> true | _ -> false
+ let goal_of_loc = function _, Open g | _, Closed g -> g
+ let goal_of_switch = function Open g | Closed g -> g
+ let switch_of_loc = snd
+
+ let zero_pos = List.map (fun g -> 0, Open g)
+
+ let init_pos locs =
+ let pos = ref 0 in (* positions are 1-based *)
+ List.map (function _, sw -> incr pos; !pos, sw) locs
+
+ let extract_pos i =
+ let rec aux acc =
+ function
+ | [] -> fail (lazy (sprintf "relative position %d not found" i))
+ | (i', _) as loc :: tl when i = i' -> loc, (List.rev acc) @ tl
+ | hd :: tl -> aux (hd :: acc) tl
+ in
+ aux []
+
+ let deep_close gs =
+ let close _ _ =
+ List.map (fun l -> if List.mem (goal_of_loc l) gs then close l else l)
+ in
+ let rm _ _ = List.filter (fun l -> not (List.mem (goal_of_loc l) gs)) in
+ map ~env:close ~cont:rm ~todo:rm
+
+ let rec find_goal =
+ function
+ | [] -> raise (Failure "Continuationals.find_goal")
+ | (l :: _, _ , _ , _) :: _ -> goal_of_loc l
+ | ( _ , _ , l :: _, _) :: _ -> goal_of_loc l
+ | ( _ , l :: _, _ , _) :: _ -> goal_of_loc l
+ | _ :: tl -> find_goal tl
+
+ let is_empty =
+ function
+ | [] -> assert false
+ | [ [], [], [], `NoTag ] -> true
+ | _ -> false
+
+ let of_metasenv metasenv =
+ let goals = List.map (fun (g, _, _) -> g) metasenv in
+ [ zero_pos goals, [], [], `NoTag ]
+
+ let head_switches =
+ function
+ | (locs, _, _, _) :: _ -> List.map switch_of_loc locs
+ | [] -> assert false
+
+ let head_goals =
+ function
+ | (locs, _, _, _) :: _ -> List.map goal_of_loc locs
+ | [] -> assert false
+
+ let head_tag =
+ function
+ | (_, _, _, tag) :: _ -> tag
+ | [] -> assert false
+
+ let shift_goals =
+ function
+ | _ :: (locs, _, _, _) :: _ -> List.map goal_of_loc locs
+ | [] -> assert false
+ | _ -> []
+
+ let open_goals stack =
+ let add_open acc _ _ l = if is_open l then goal_of_loc l :: acc else acc in
+ List.rev (fold ~env:add_open ~cont:add_open ~todo:add_open [] stack)
+
+ let (@+) = (@) (* union *)
+
+ let (@-) s1 s2 = (* difference *)
+ List.fold_right
+ (fun e acc -> if List.mem e s2 then acc else e :: acc)
+ s1 []
+
+ let (@~-) locs gs = (* remove some goals from a locators list *)
+ List.fold_right
+ (fun loc acc -> if List.mem (goal_of_loc loc) gs then acc else loc :: acc)
+ locs []
+
+ let pp stack =
+ let pp_goal = string_of_int in
+ let pp_switch =
+ function Open g -> "o" ^ pp_goal g | Closed g -> "c" ^ pp_goal g
+ in
+ let pp_loc (i, s) = string_of_int i ^ pp_switch s in
+ let pp_env env = sprintf "[%s]" (String.concat ";" (List.map pp_loc env)) in
+ let pp_tag = function `BranchTag -> "B" | `FocusTag -> "F" | `NoTag -> "N" in
+ let pp_stack_entry (env, todo, cont, tag) =
+ sprintf "(%s, %s, %s, %s)" (pp_env env) (pp_env todo) (pp_env cont)
+ (pp_tag tag)
+ in
+ String.concat " :: " (List.map pp_stack_entry stack)
+end
+
+module type Status =