From: Stefano Zacchiroli Date: Thu, 6 Oct 2005 17:59:24 +0000 (+0000) Subject: changed functor interface, now based on proofs instead of metasenvs (this one is... X-Git-Tag: V_0_7_2_3~232 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8508b9dd5fa37b169b36e8143df8bf5e9206b127;p=helm.git changed functor interface, now based on proofs instead of metasenvs (this one is implementable on top of ProofEngineTypes ...) --- diff --git a/helm/ocaml/tactics/continuationals.ml b/helm/ocaml/tactics/continuationals.ml index 0dc1b7523..5f72547c2 100644 --- a/helm/ocaml/tactics/continuationals.ml +++ b/helm/ocaml/tactics/continuationals.ml @@ -23,23 +23,24 @@ * 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, @@ -59,7 +60,7 @@ struct 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 @@ -78,18 +79,21 @@ struct 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 @@ -103,89 +107,92 @@ struct 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 diff --git a/helm/ocaml/tactics/continuationals.mli b/helm/ocaml/tactics/continuationals.mli index bebea7045..65a579b67 100644 --- a/helm/ocaml/tactics/continuationals.mli +++ b/helm/ocaml/tactics/continuationals.mli @@ -28,16 +28,15 @@ exception Error of string 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 (** new proof, opened goals, closed goals *) end module Make (E:Engine) : @@ -45,7 +44,7 @@ sig 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 @@ -67,6 +66,6 @@ sig | Qed val eval: t -> status -> status - val init: E.metasenv -> status + val init: E.proof -> status end