open Printf
-exception Error of string
+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)
-module type Engine =
+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 =
sig
- type goal
- type proof
+ type input_status
+ type output_status
+
type tactic
- val is_goal_closed: goal -> proof -> bool
- val goals_of_proof: proof -> goal list
+ val id_tactic : tactic
+ val mk_tactic : (input_status -> output_status) -> tactic
+ val apply_tactic : tactic -> input_status -> output_status
- val apply_tactic:
- tactic -> proof -> goal ->
- proof * goal list * goal list
-end
+ val goals : output_status -> goal list * goal list (** opened, closed goals *)
+ val set_goals: goal list * goal list -> output_status -> output_status
+ val get_stack : input_status -> Stack.t
+ val set_stack : Stack.t -> output_status -> output_status
-(** like List.assoc returning a pair: binding matching the given key,
- * associative list without the returned binding
- * @raise Not_found *)
-let list_assoc_extract key =
- let rec aux acc =
- function
- | [] -> raise Not_found
- | (key', _) as hd :: tl when key = key' -> hd, (List.rev acc @ tl)
- | hd :: tl -> aux (hd :: acc) tl
- in
- aux []
+ val inject : input_status -> output_status
+ val focus : goal -> output_status -> input_status
+end
-module Make (E:Engine) =
-struct
- type goal_switch = Open of E.goal | Closed of E.goal
- type 'a stack = 'a list
- type status =
- E.proof * ((int * goal_switch) list * E.goal list * E.goal list) stack
+module type C =
+sig
+ type input_status
+ type output_status
+ type tactic
type tactical =
- | Tactic of E.tactic
+ | Tactic of tactic
| Skip
type t =
| Dot
| Semicolon
+
| Branch
- | Shift of int option
+ | Shift
+ | Pos of int
| Merge
- | Select of E.goal list
- | End_select
+
+ | Focus of goal list
+ | Unfocus
+
| Tactical of tactical
- | Qed
-
- let goal_of = function _, Open g -> g | _, Closed g -> g
- let is_open = function _, Open _ -> true | _, Closed _ -> false
- let open_all = List.map (fun p, g -> p, Open g)
-
- let union a b = a @ b
-
- let complementary part full = (* not really efficient *)
- List.fold_left (fun acc g -> if List.mem g part then acc else g::acc)
- full []
-
- let close to_close =
- List.map
- (function
- | p, Open g when List.mem g to_close -> p, Closed g
- | g -> g)
- let map_stack f g h = List.map (fun (a,b,c) -> f a, g b, h c)
+ val eval: t -> input_status -> output_status
+end
+
+module Make (S: Status) =
+struct
+ open Stack
- let dummy_pos = ~-1
- let add_dummy_pos g = dummy_pos, g
- let map_dummy_pos = List.map add_dummy_pos
+ type input_status = S.input_status
+ type output_status = S.output_status
+ type tactic = S.tactic
- let map_open_pos =
- let rec aux pos =
- function
- | [] -> []
- | g :: tl -> (pos, Open g) :: aux (pos + 1) tl
- in
- aux 1
+ type tactical =
+ | Tactic of tactic
+ | Skip
- let eval_tactical tactical proof switch =
+ type t =
+ | Dot
+ | Semicolon
+ | Branch
+ | Shift
+ | Pos of int
+ | Merge
+ | Focus of goal list
+ | Unfocus
+ | Tactical of tactical
+
+ let pp_t =
+ function
+ | Dot -> "Dot"
+ | Semicolon -> "Semicolon"
+ | Branch -> "Branch"
+ | Shift -> "Shift"
+ | Pos i -> "Pos " ^ string_of_int i
+ | Merge -> "Merge"
+ | Focus gs ->
+ sprintf "Focus [%s]" (String.concat "; " (List.map string_of_int gs))
+ | Unfocus -> "Unfocus"
+ | Tactical _ -> "Tactical <abs>"
+
+ let eval_tactical tactical ostatus switch =
match tactical, switch with
- | Tactic tac, Open n -> E.apply_tactic tac proof n
- | Skip, Closed n -> proof, [], [n]
- | Tactic _, Closed _ -> fail "can't apply tactic to a closed goal"
- | Skip, Open _ -> fail "can't skip an open goal"
-
- let eval continuational status =
- match continuational, status with
- | _, (_, []) -> assert false
- | Tactical t, (proof, (env, todo, left)::tail) ->
- assert (List.length env > 1);
- let proof, opened, closed =
- List.fold_left
- (fun (proof, opened, closed) cur_goal ->
- if List.exists ((=) (goal_of cur_goal)) closed then
- proof, opened, closed
- else
- let proof, newopened, newclosed =
- eval_tactical t proof (snd cur_goal)
+ | Tactic tac, Open n ->
+ let ostatus = S.apply_tactic tac (S.focus n ostatus) in
+ let opened, closed = S.goals ostatus in
+ ostatus, opened, closed
+ | Skip, Closed n -> ostatus, [], [n]
+ | Tactic _, Closed _ -> fail (lazy "can't apply tactic to a closed goal")
+ | Skip, Open _ -> fail (lazy "can't skip an open goal")
+
+ let eval cmd istatus =
+ let stack = S.get_stack istatus in
+ debug_print (lazy (sprintf "EVAL CONT %s <- %s" (pp_t cmd) (pp stack)));
+ let new_stack stack = S.inject istatus, stack in
+ let ostatus, stack =
+ match cmd, stack with
+ | _, [] -> assert false
+ | Tactical tac, (g, t, k, tag) :: s ->
+ if g = [] then fail (lazy "can't apply a tactic to zero goals");
+ debug_print (lazy ("context length " ^string_of_int (List.length g)));
+ let rec aux s go gc =
+ function
+ | [] -> s, go, gc
+ | loc :: loc_tl ->
+ debug_print (lazy "inner eval tactical");
+ let s, go, gc =
+ if List.exists ((=) (goal_of_loc loc)) gc then
+ s, go, gc
+ else
+ let s, go', gc' = eval_tactical tac s (switch_of_loc loc) in
+ s, (go @- gc') @+ go', gc @+ gc'
in
- 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)
- :: map_stack
- (close closed) (complementary closed) (complementary opened) tail
- | Semicolon, (proof, stack) -> proof, stack
- | Dot, (proof, (env, todo, left)::tail) ->
- let env, left =
- match List.filter is_open env, left with
- | [], [] -> fail "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)::tail
- | Branch, (proof, (g1::tl, todo, left)::tail) ->
- assert (List.length tl >= 1);
- proof, ([g1], [], [])::(tl, todo, left)::tail
- | Branch, (_, _) -> fail "can't branch on a singleton context"
- | Shift opt_pos, (proof, (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 -> fail (sprintf "position %d not found" pos))
- | None, [] -> fail "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, [])::(rem_goals, todo,left)::tail
- | Shift _, (_, _) -> fail "no more goals to shift"
- | Merge, (proof, (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 (List.filter is_open leftopen))))
- in
- proof, (env,todo,left)::tail
- | Merge, (_, [_]) -> fail "can't merge here"
- | Select gl, (proof, stack) ->
- List.iter
- (fun g ->
- if not (E.is_goal_closed g proof) then
- fail "you can't select a closed goal")
- gl;
- (proof, (open_all (map_dummy_pos gl),[],[])::stack)
- | End_select, (proof, stack) ->
- (match stack with
- | ([], [], [])::tail -> proof, tail
- | _ -> fail "select left some goals open")
- | Qed, (proof, [[], [], []]) -> status
- | Qed, _ -> fail "can't qed an unfinished proof"
-
- let init proof =
- proof,
- [ map_open_pos (E.goals_of_proof proof), [], [] ]
+ 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
end
projects / helm.git / blobdiff