* http://helm.cs.unibo.it/
*)
+open Printf
+
exception Error of string
-module L = List
+let fail msg = raise (Error msg)
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,
type goal_switch = Open of E.goal | Closed of E.goal
type 'a stack = 'a list
type status =
- E.metasenv * ((int * goal_switch) list * E.goal list * E.goal list) stack
+ E.proof * ((int * goal_switch) list * E.goal list * E.goal list) stack
type tactical =
| Tactic of E.tactic
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) -> f a, g b, h c)
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 _ -> 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, (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)::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
+ :: 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)::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
+ | [], [] -> 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
- 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)::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 ->
- raise (Error (Printf.sprintf "position %d not found" pos)))
- | None, [] -> raise (Error "no more goals to shift")
+ 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
- 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) ->
+ 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 (L.filter is_open leftopen ))))
+ (union not_processed (List.filter is_open leftopen))))
in
- metasenv, (env,todo,left)::tail
- | Merge, (_, [_]) -> raise (Error "can't merge here")
- | Select gl, (metasenv, stack) ->
+ proof, (env,todo,left)::tail
+ | Merge, (_, [_]) -> fail "can't merge here"
+ | 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 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 -> 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), [], [] ]
+ | ([], [], [])::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), [], [] ]
end
projects / helm.git / commitdiff