* http://helm.cs.unibo.it/
*)
-exception Error of string
+open Printf
-module L = List
+exception Error of string Lazy.t
module type Engine =
sig
type goal
- type conjecture
- type metasenv = conjecture list
+ type proof
type tactic
- val goal_of_conjecture: conjecture -> goal
- val goal_mem: goal -> metasenv -> bool
+ val is_goal_closed: goal -> proof -> bool
+ val goals_of_proof: proof -> goal list
val apply_tactic:
- tactic -> metasenv -> goal ->
- metasenv * goal list * goal list
+ tactic -> proof -> goal ->
+ proof * goal list * goal list
end
(** like List.assoc returning a pair: binding matching the given key,
in
aux []
+module type C =
+sig
+ type goal
+ type proof
+ type tactic
+
+ type status
+
+ type tactical =
+ | Tactic of tactic
+ | Skip
+
+ type t =
+ | Dot
+ | Semicolon
+
+ | Branch
+ | Shift of int option
+ | Select of goal list
+ | End
+
+ | Tactical of tactical
+
+ val eval: t -> status -> status
+ val init: proof -> status
+
+ val get_proof: status -> proof
+ val set_proof: proof -> status -> status
+
+ type goal_switch = Open of goal | Closed of goal
+ val get_goals: status -> goal_switch list
+
+ val is_completed: status -> bool
+end
+
module Make (E:Engine) =
struct
- type goal_switch = Open of E.goal | Closed of E.goal
+ type goal = E.goal
+ type proof = E.proof
+ type tactic = E.tactic
+
+ type goal_switch = Open of goal | Closed of goal
type 'a stack = 'a list
- type status =
- E.metasenv * ((int * goal_switch) list * E.goal list * E.goal list) stack
+ type stack_tag = BranchTag | SelectTag | NoTag
+ type stack_entry =
+ (int * goal_switch) list * goal list * goal list * stack_tag
+ type status = proof * stack_entry stack
+
+ let get_proof = fst
+ let set_proof p (_, s) = p, s
+ let get_goals (_, stack) =
+ match stack with
+ | (goals, _, _, _) :: _ -> List.map snd goals
+ | [] -> assert false
type tactical =
- | Tactic of E.tactic
+ | Tactic of tactic
| Skip
type t =
| Semicolon
| Branch
| Shift of int option
- | Merge
- | Select of E.goal list
- | End_select
+ | Select of goal list
+ | End
| 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 = L.map (fun p, g -> p, Open g)
+ let open_all = List.map (fun p, g -> p, Open g)
let union a b = a @ b
let complementary part full = (* not really efficient *)
- L.fold_left (fun acc g -> if L.mem g part then acc else g::acc) full []
+ List.fold_left (fun acc g -> if List.mem g part then acc else g::acc)
+ full []
- let close to_close l =
- L.map (function p, Open g when L.mem g to_close -> p, Closed g | g -> g) l
+ let close to_close =
+ List.map
+ (function
+ | p, Open g when List.mem g to_close -> p, Closed g
+ | g -> g)
- let stack_map f g h stack =
- L.map (fun (a,b,c) -> f a, g b, h c) stack
+ let map_stack f g h = List.map (fun (a,b,c,tag) -> f a, g b, h c, tag)
let dummy_pos = ~-1
let add_dummy_pos g = dummy_pos, g
in
aux 1
- let eval_tactical tactical metasenv switch =
+ let eval_tactical tactical proof switch =
match tactical, switch with
- | Tactic tac, Open n -> E.apply_tactic tac metasenv n
- | Skip, Closed n -> metasenv, [], [n]
- | Tactic _, Closed _ -> raise (Error "can't apply tactic to a closed goal")
- | Skip, Open _ -> raise (Error "can't skip an open goal")
+ | Tactic tac, Open n -> E.apply_tactic tac proof n
+ | Skip, Closed n -> proof, [], [n]
+ | Tactic _, Closed _ -> raise (Error (lazy "can't apply tactic to a closed goal"))
+ | Skip, Open _ -> raise (Error (lazy "can't skip an open goal"))
let eval continuational status =
match continuational, status with
| _, (_, []) -> assert false
- | Tactical t, (metasenv, (env, todo, left)::tail) ->
- assert (L.length env > 1);
- let metasenv, opened, closed =
- L.fold_left
- (fun (metasenv, opened, closed) cur_goal ->
- if L.exists ((=) (goal_of cur_goal)) closed then
- metasenv, opened, closed
+ | Tactical t, (proof, (env, todo, left,tag)::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 metasenv, newopened, newclosed =
- eval_tactical t metasenv (snd cur_goal)
+ let proof, newopened, newclosed =
+ eval_tactical t proof (snd cur_goal)
in
- metasenv,
+ proof,
union (complementary newclosed opened) newopened,
union closed newclosed
- ) (metasenv, [],[]) env
+ ) (proof, [],[]) env
in
let pos = ref 0 in
let stack_opened = List.map (fun g -> incr pos; !pos, g) opened in
- metasenv,
+ proof,
(open_all stack_opened,
complementary closed todo,
- complementary opened left)
- :: stack_map
+ complementary opened left, tag)
+ :: map_stack
(close closed) (complementary closed) (complementary opened) tail
- | Semicolon, (metasenv, stack) -> metasenv, stack
- | Dot, (metasenv, (env, todo, left)::tail) ->
+ | Semicolon, (proof, stack) -> proof, stack
+ | Dot, (proof, (env, todo, left, tag)::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
+ 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
- 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) ->
+ 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 (Printf.sprintf "position %d not found" pos)))
- | None, [] -> raise (Error "no more goals to shift")
+ 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 (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 ))))
+ let t =
+ union t (union (List.map goal_of (List.filter is_open leftopen)) l)
in
- metasenv, (env,todo,left)::tail
- | Merge, (_, [_]) -> raise (Error "can't merge here")
- | Select gl, (metasenv, stack) ->
+ 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 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) ->
+ (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
- | ([], [], [])::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), [], [] ]
+ | ([], [], [], 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
end
projects / helm.git / blobdiff