From 3337e1349c79b52dcadb2b072539ca0c881d70c9 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 10 Oct 2005 08:07:19 +0000 Subject: [PATCH] - added stack frame tagging - unified "End" for Branch and Select --- helm/ocaml/tactics/continuationals.ml | 115 ++++++++++++++++++------- helm/ocaml/tactics/continuationals.mli | 38 +++++--- 2 files changed, 107 insertions(+), 46 deletions(-) diff --git a/helm/ocaml/tactics/continuationals.ml b/helm/ocaml/tactics/continuationals.ml index 5f72547c2..5b1bbce3d 100644 --- a/helm/ocaml/tactics/continuationals.ml +++ b/helm/ocaml/tactics/continuationals.ml @@ -55,15 +55,63 @@ let list_assoc_extract 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.proof * ((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 = @@ -71,11 +119,9 @@ struct | 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 @@ -93,7 +139,7 @@ struct | 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) + 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 @@ -117,7 +163,7 @@ struct let eval continuational status = match continuational, status with | _, (_, []) -> assert false - | Tactical t, (proof, (env, todo, left)::tail) -> + | Tactical t, (proof, (env, todo, left,tag)::tail) -> assert (List.length env > 1); let proof, opened, closed = List.fold_left @@ -138,23 +184,24 @@ struct proof, (open_all stack_opened, complementary closed todo, - complementary opened left) + complementary opened left, tag) :: map_stack (close closed) (complementary closed) (complementary opened) tail | Semicolon, (proof, stack) -> proof, stack - | Dot, (proof, (env, todo, left)::tail) -> + | Dot, (proof, (env, todo, left, tag)::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) -> + proof, (env, todo, left, tag)::tail + | Branch, (proof, (g1::tl, todo, left, tag)::tail) -> assert (List.length tl >= 1); - proof, ([g1], [], [])::(tl, todo, left)::tail + proof, ([g1], [], [], BranchTag)::(tl, todo, left, tag)::tail | Branch, (_, _) -> fail "can't branch on a singleton context" - | Shift opt_pos, (proof, (leftopen, t, l)::(goals, todo, left)::tail) -> + | 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 @@ -167,32 +214,34 @@ struct 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 + proof, ([next_goal], t, [], BranchTag)::(rem_goals, todo,left,tag)::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 + if 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) -> + (proof, (open_all (map_dummy_pos gl),[],[],SelectTag)::stack) + | End, (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" + | ([], [], [], 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 + | _ -> fail "can't end here") let init proof = proof, - [ map_open_pos (E.goals_of_proof proof), [], [] ] + [ map_open_pos (E.goals_of_proof proof), [], [], NoTag ] + + let is_completed = + function + | (_, [[],[],[],NoTag]) -> true + | _ -> false end diff --git a/helm/ocaml/tactics/continuationals.mli b/helm/ocaml/tactics/continuationals.mli index 65a579b67..e89e2e51d 100644 --- a/helm/ocaml/tactics/continuationals.mli +++ b/helm/ocaml/tactics/continuationals.mli @@ -39,15 +39,16 @@ sig proof * goal list * goal list (** new proof, opened goals, closed goals *) end -module Make (E:Engine) : +module type C = sig - 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 + type goal + type proof + type tactic + + type status type tactical = - | Tactic of E.tactic + | Tactic of tactic | Skip type t = @@ -56,16 +57,27 @@ sig | Branch | Shift of int option - | Merge - - | Select of E.goal list - | End_select + | Select of goal list + | End | Tactical of tactical - | Qed - val eval: t -> status -> status - val init: E.proof -> status + val init: proof -> status + + (** {2 Status accessors} *) + + 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) : C + with type goal = E.goal + and type proof = E.proof + and type tactic = E.tactic + -- 2.39.2