diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/pfedit.ml | 21 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 16 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 45 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 31 |
4 files changed, 67 insertions, 46 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 8a52244df2..e4cdf49896 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -29,9 +29,9 @@ let delete_all_proofs = Proof_global.discard_all let set_undo _ = () let get_undo _ = None -let start_proof (id : Id.t) str hyps c ?init_tac ?compute_guard hook = +let start_proof (id : Id.t) str hyps c ?init_tac ?compute_guard hook terminator = let goals = [ (Global.env_of_context hyps , c) ] in - Proof_global.start_proof id str goals ?compute_guard hook; + Proof_global.start_proof id str goals ?compute_guard hook terminator; let env = Global.env () in ignore (Proof_global.with_current_proof (fun _ p -> match init_tac with @@ -40,11 +40,12 @@ let start_proof (id : Id.t) str hyps c ?init_tac ?compute_guard hook = let cook_this_proof hook p = match p with - | (i,([e],cg,str,h)) -> (i,(e,cg,str,h)) + | { Proof_global.id;entries=[constr];do_guard;persistence;hook } -> + (id,(constr,do_guard,persistence,hook)) | _ -> Errors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.") let cook_proof hook = - cook_this_proof hook (Proof_global.close_proof (fun x -> x)) + cook_this_proof hook (fst (Proof_global.close_proof (fun x -> x))) let get_pftreestate () = Proof_global.give_me_the_proof () @@ -122,7 +123,7 @@ open Decl_kinds let next = let n = ref 0 in fun () -> incr n; !n let build_constant_by_tactic id sign ?(goal_kind = Global,Proof Theorem) typ tac = - start_proof id goal_kind sign typ (fun _ _ -> ()); + start_proof id goal_kind sign typ (fun _ _ -> ()) (fun _ -> ()); try let status = by tac in let _,(const,_,_,_) = cook_proof (fun _ -> ()) in @@ -166,13 +167,3 @@ let solve_by_implicit_tactic env sigma evk = (try fst (build_by_tactic env evi.evar_concl (Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (Errors.UserError ("",Pp.str"Proof is not complete."))) []))) with e when Logic.catchable_exception e -> raise Exit) | _ -> raise Exit - - - - - - - - - - diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 6dad738afb..110df23470 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -62,7 +62,7 @@ type lemma_possible_guards = Proof_global.lemma_possible_guards val start_proof : Id.t -> goal_kind -> named_context_val -> constr -> ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> - unit declaration_hook -> unit + unit declaration_hook -> Proof_global.proof_terminator -> unit (** {6 ... } *) (** [cook_proof opacity] turns the current proof (assumed completed) into @@ -71,19 +71,15 @@ val start_proof : it also tells if the guardness condition has to be inferred. *) val cook_this_proof : (Proof.proof -> unit) -> - Id.t * - (Entries.definition_entry list * - lemma_possible_guards * - Decl_kinds.goal_kind * - unit Tacexpr.declaration_hook Ephemeron.key) -> - Id.t * + Proof_global.proof_object -> + (Id.t * (Entries.definition_entry * lemma_possible_guards * goal_kind * - unit declaration_hook Ephemeron.key) + unit declaration_hook Ephemeron.key)) val cook_proof : (Proof.proof -> unit) -> - Id.t * + (Id.t * (Entries.definition_entry * lemma_possible_guards * goal_kind * - unit declaration_hook Ephemeron.key) + unit declaration_hook Ephemeron.key)) (** {6 ... } *) (** [get_pftreestate ()] returns the current focused pending proof. diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index b7a32a9801..b2282a6831 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -65,14 +65,28 @@ let _ = (* Extra info on proofs. *) type lemma_possible_guards = int list list +type proof_object = { + id : Names.Id.t; + entries : Entries.definition_entry list; + do_guard : lemma_possible_guards; + persistence : Decl_kinds.goal_kind; + hook : unit Tacexpr.declaration_hook Ephemeron.key +} + +type proof_ending = Vernacexpr.proof_end * proof_object +type proof_terminator = + proof_ending -> unit +type closed_proof = proof_object*proof_terminator Ephemeron.key + type pstate = { pid : Id.t; + terminator : proof_terminator Ephemeron.key; endline_tactic : Tacexpr.raw_tactic_expr option; section_vars : Context.section_context option; proof : Proof.proof; strength : Decl_kinds.goal_kind; compute_guard : lemma_possible_guards; - hook : unit Tacexpr.declaration_hook Ephemeron.key; + pr_hook : unit Tacexpr.declaration_hook Ephemeron.key; mode : proof_mode Ephemeron.key; } @@ -236,27 +250,29 @@ end It raises exception [ProofInProgress] if there is a proof being currently edited. *) -let start_proof id str goals ?(compute_guard=[]) hook = +let start_proof id str goals ?(compute_guard=[]) hook terminator = let initial_state = { pid = id; + terminator = Ephemeron.create terminator; proof = Proof.start Evd.empty goals; endline_tactic = None; section_vars = None; strength = str; compute_guard = compute_guard; - hook = Ephemeron.create hook; + pr_hook = Ephemeron.create hook; mode = find_proof_mode "No" } in push initial_state pstates -let start_dependent_proof id str goals ?(compute_guard=[]) hook = +let start_dependent_proof id str goals ?(compute_guard=[]) hook terminator = let initial_state = { pid = id; + terminator = Ephemeron.create terminator; proof = Proof.dependent_start Evd.empty goals; endline_tactic = None; section_vars = None; strength = str; compute_guard = compute_guard; - hook = Ephemeron.create hook; + pr_hook = Ephemeron.create hook; mode = find_proof_mode "No" } in push initial_state pstates @@ -280,13 +296,10 @@ let get_open_goals () = (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) + List.length shelf -type closed_proof = - Names.Id.t * - (Entries.definition_entry list * lemma_possible_guards * - Decl_kinds.goal_kind * unit Tacexpr.declaration_hook Ephemeron.key) - let close_proof ~now fpl = - let { pid;section_vars;compute_guard;strength;hook;proof } = cur_pstate () in + let { pid;section_vars;compute_guard;strength;pr_hook;proof;terminator } = + cur_pstate () + in let initial_goals = Proof.initial_goals proof in let entries = Future.map2 (fun p (c, t) -> { Entries. const_entry_body = p; @@ -296,7 +309,11 @@ let close_proof ~now fpl = const_entry_opaque = true }) fpl initial_goals in if now then List.iter (fun x -> ignore(Future.join x.Entries.const_entry_body)) entries; - (pid, (entries, compute_guard, strength, hook)) + { id = pid ; + entries = entries ; + do_guard = compute_guard ; + persistence = strength ; + hook = pr_hook } , terminator let return_proof () = let { proof } = cur_pstate () in @@ -471,8 +488,8 @@ let _ = module V82 = struct let get_current_initial_conclusions () = - let { pid; strength; hook; proof } = cur_pstate () in - pid, (List.map snd (Proof.initial_goals proof), strength, hook) + let { pid; strength; pr_hook; proof } = cur_pstate () in + pid, (List.map snd (Proof.initial_goals proof), strength, pr_hook) end type state = pstate list diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index e88c2f3942..eb7d0ecb17 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -46,17 +46,37 @@ exception NoCurrentProof val give_me_the_proof : unit -> Proof.proof (** @raise NoCurrentProof when outside proof mode. *) +(** When a proof is closed, it is reified into a [proof_object], where + [id] is the name of the proof, [entries] the list of the proof terms + (in a form suitable for definitions). Together with the [terminator] + function which takes a [proof_object] together with a [proof_end] + (i.e. an proof ending command) and registers the appropriate + values. *) +type lemma_possible_guards = int list list +type proof_object = { + id : Names.Id.t; + entries : Entries.definition_entry list; + do_guard : lemma_possible_guards; + persistence : Decl_kinds.goal_kind; + hook : unit Tacexpr.declaration_hook Ephemeron.key +} + +type proof_ending = Vernacexpr.proof_end * proof_object +type proof_terminator = + proof_ending -> unit +type closed_proof = proof_object*proof_terminator Ephemeron.key + (** [start_proof s str goals ~init_tac ~compute_guard hook] starts a proof of name [s] and conclusion [t]; [hook] is optionally a function to be applied at proof end (e.g. to declare the built constructions as a coercion or a setoid morphism). *) -type lemma_possible_guards = int list list val start_proof : Names.Id.t -> Decl_kinds.goal_kind -> (Environ.env * Term.types) list -> - ?compute_guard:lemma_possible_guards -> - unit Tacexpr.declaration_hook -> + ?compute_guard:lemma_possible_guards -> + unit Tacexpr.declaration_hook -> + proof_terminator -> unit (** Like [start_proof] except that there may be dependencies between initial goals. *) @@ -65,12 +85,9 @@ val start_dependent_proof : Names.Id.t -> Proofview.telescope -> ?compute_guard:lemma_possible_guards -> unit Tacexpr.declaration_hook -> + proof_terminator -> unit -type closed_proof = - Names.Id.t * - (Entries.definition_entry list * lemma_possible_guards * - Decl_kinds.goal_kind * unit Tacexpr.declaration_hook Ephemeron.key) (* Takes a function to add to the exceptions data relative to the state in which the proof was built *) |