From: Stefano Zacchiroli Date: Thu, 6 Oct 2005 11:37:40 +0000 (+0000) Subject: - better naming X-Git-Tag: V_0_7_2_3~238 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=99db482ebae3e3e4dcc6c4df12027a81bb7a7f76;p=helm.git - better naming - uniform handling of empty stack assertion failure - added Qed and init --- diff --git a/helm/ocaml/tactics/continuationals.ml b/helm/ocaml/tactics/continuationals.ml index f5a747720..0dc1b7523 100644 --- a/helm/ocaml/tactics/continuationals.ml +++ b/helm/ocaml/tactics/continuationals.ml @@ -35,7 +35,7 @@ sig type tactic val goal_of_conjecture: conjecture -> goal - val is_goal_in_metasenv: metasenv -> goal -> bool + val goal_mem: goal -> metasenv -> bool val apply_tactic: tactic -> metasenv -> goal -> @@ -74,6 +74,7 @@ struct | Select of E.goal list | End_select | Tactical of tactical + | Qed let goal_of = function _, Open g -> g | _, Closed g -> g let is_open = function _, Open _ -> true | _, Closed _ -> false @@ -94,6 +95,14 @@ struct let add_dummy_pos g = dummy_pos, g let map_dummy_pos = List.map add_dummy_pos + let map_open_pos = + let rec aux pos = + function + | [] -> [] + | g :: tl -> (pos, Open g) :: aux (pos + 1) tl + in + aux 1 + let eval_tactical tactical metasenv switch = match tactical, switch with | Tactic tac, Open n -> E.apply_tactic tac metasenv n @@ -101,8 +110,9 @@ struct | Tactic _, Closed _ -> raise (Error "can't apply tactic to a closed goal") | Skip, Open _ -> raise (Error "can't skip an open goal") - let eval continuational (status: status) = + 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 = @@ -127,7 +137,6 @@ struct complementary opened left) :: stack_map (close closed) (complementary closed) (complementary opened) tail - | Tactical _, (_, []) -> assert false | Semicolon, (metasenv, stack) -> metasenv, stack | Dot, (metasenv, (env, todo, left)::tail) -> let env, left = @@ -137,7 +146,6 @@ struct | [], g::left -> [dummy_pos, Open g], left in metasenv, (env, todo, left)::tail - | Dot, (_, []) -> assert false | Branch, (metasenv, (g1::tl, todo, left)::tail) -> assert (L.length tl >= 1); metasenv, ([g1], [], [])::(tl, todo, left)::tail @@ -163,16 +171,21 @@ struct (union not_processed (L.filter is_open leftopen )))) in metasenv, (env,todo,left)::tail - | Merge, (_, []) | Merge, (_, [_]) -> raise (Error "can't merge here") | Select gl, (metasenv, stack) -> List.iter - (fun g -> if not (E.is_goal_in_metasenv metasenv g) then + (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) -> (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), [], [] ] end diff --git a/helm/ocaml/tactics/continuationals.mli b/helm/ocaml/tactics/continuationals.mli index 4b2632e56..bebea7045 100644 --- a/helm/ocaml/tactics/continuationals.mli +++ b/helm/ocaml/tactics/continuationals.mli @@ -33,7 +33,7 @@ sig type tactic val goal_of_conjecture: conjecture -> goal - val is_goal_in_metasenv: metasenv -> goal -> bool + val goal_mem: goal -> metasenv -> bool val apply_tactic: tactic -> metasenv -> goal -> @@ -54,13 +54,19 @@ sig type t = | Dot | Semicolon + | Branch | Shift of int option | Merge + | Select of E.goal list | End_select + | Tactical of tactical + | Qed + val eval: t -> status -> status + val init: E.metasenv -> status end