diff options
author | Arnaud Spiwack <arnaud@spiwack.net> | 2013-11-27 18:41:09 +0100 |
---|---|---|
committer | Arnaud Spiwack <arnaud@spiwack.net> | 2013-12-04 14:14:33 +0100 |
commit | f1a2c15b7a7d7edfd4b4b379ed0bde8b1f5deb7b (patch) | |
tree | 7f29564ddfa4d1bf2d4a06b6dd212cc3ef3beaff | |
parent | eaa9c147f1801c363635a5be4e0258e0de1ab02e (diff) |
Factoring(continued).
This commit removes the hook.
-rw-r--r-- | plugins/funind/functional_principles_types.ml | 11 | ||||
-rw-r--r-- | plugins/funind/indfun_common.ml | 4 | ||||
-rw-r--r-- | plugins/funind/indfun_common.mli | 3 | ||||
-rw-r--r-- | plugins/xml/xmlcommand.ml | 2 | ||||
-rw-r--r-- | proofs/pfedit.ml | 20 | ||||
-rw-r--r-- | proofs/pfedit.mli | 14 | ||||
-rw-r--r-- | proofs/proof_global.ml | 72 | ||||
-rw-r--r-- | proofs/proof_global.mli | 5 | ||||
-rw-r--r-- | toplevel/lemmas.ml | 17 |
9 files changed, 68 insertions, 80 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 3d577b440..2661a78a5 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -289,12 +289,13 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro let new_princ_name = next_ident_away_in_goal (Id.of_string "___________princ_________") [] in + let hook = hook new_principle_type in begin Lemmas.start_proof new_princ_name (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem)) new_principle_type - (hook new_principle_type) + hook ; (* let _tim1 = System.get_time () in *) ignore (Pfedit.by (Proofview.V82.tactic (proof_tac (Array.map mkConst funs) mutr_nparams))); @@ -303,7 +304,7 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro (* let dur1 = System.time_difference tim1 tim2 in *) (* Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *) (* end; *) - get_proof_clean true + get_proof_clean true,Ephemeron.create hook end @@ -359,7 +360,7 @@ let generate_functional_principle register_with_sort InProp; register_with_sort InSet in - let (id,(entry,g_kind,hook)) = + let ((id,(entry,g_kind)),hook) = build_functional_principle interactive_proof old_princ_type new_sorts funs i proof_tac hook in @@ -511,7 +512,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis s::l_schemes -> s,l_schemes | _ -> anomaly (Pp.str "") in - let (_,(const,_,_)) = + let ((_,(const,_)),_) = try build_functional_principle false first_type @@ -585,7 +586,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis (* If we reach this point, the two principle are not mutually recursive We fall back to the previous method *) - let (_,(const,_,_)) = + let ((_,(const,_)),_) = build_functional_principle false (List.nth other_princ_types (!i - 1)) diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 604d7d853..5c37dcec3 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -166,8 +166,8 @@ let save with_clean id const (locality,kind) hook = let cook_proof _ = - let (id,(entry,strength,hook)) = Pfedit.cook_proof (fun _ -> ()) in - (id,(entry,strength,hook)) + let (id,(entry,strength)) = Pfedit.cook_proof () in + (id,(entry,strength)) let get_proof_clean do_reduce = let result = cook_proof do_reduce in diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index cea5ffe25..0e8b22deb 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -54,8 +54,7 @@ val save : bool -> Id.t -> Entries.definition_entry -> Decl_kinds.goal_kind -> *) val get_proof_clean : bool -> Names.Id.t * - (Entries.definition_entry * Decl_kinds.goal_kind * - unit Tacexpr.declaration_hook Ephemeron.key) + (Entries.definition_entry * Decl_kinds.goal_kind) diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index 83a4d425b..5f26e2bac 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -412,7 +412,7 @@ let show_pftreestate internal fn (kind,pftst) id = let show fn = let pftst = Pfedit.get_pftreestate () in - let (id,kind,_,_) = Pfedit.current_proof_statement () in + let (id,kind,_) = Pfedit.current_proof_statement () in show_pftreestate false fn (kind,pftst) id ;; diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 83eb47bb9..7d225a470 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -29,23 +29,23 @@ 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 hook terminator = +let start_proof (id : Id.t) str hyps c ?init_tac terminator = let goals = [ (Global.env_of_context hyps , c) ] in - Proof_global.start_proof id str goals hook terminator; + Proof_global.start_proof id str goals terminator; let env = Global.env () in ignore (Proof_global.with_current_proof (fun _ p -> match init_tac with | None -> p,true | Some tac -> Proof.run_tactic env tac p)) -let cook_this_proof hook p = +let cook_this_proof p = match p with - | { Proof_global.id;entries=[constr];persistence;hook } -> - (id,(constr,persistence,hook)) + | { Proof_global.id;entries=[constr];persistence } -> + (id,(constr,persistence)) | _ -> Errors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.") -let cook_proof hook = - cook_this_proof hook (fst (Proof_global.close_proof (fun x -> x))) +let cook_proof () = + cook_this_proof (fst (Proof_global.close_proof (fun x -> x))) let get_pftreestate () = Proof_global.give_me_the_proof () @@ -88,7 +88,7 @@ let get_current_goal_context () = let current_proof_statement () = match Proof_global.V82.get_current_initial_conclusions () with - | (id,([concl],strength,hook)) -> id,strength,concl,hook + | (id,([concl],strength)) -> id,strength,concl | _ -> Errors.anomaly ~label:"Pfedit.current_proof_statement" (Pp.str "more than one statement") let solve ?with_end_tac gi tac pr = @@ -123,10 +123,10 @@ 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 _ _ -> ()) (fun _ -> ()); + start_proof id goal_kind sign typ (fun _ -> ()); try let status = by tac in - let _,(const,_,_) = cook_proof (fun _ -> ()) in + let _,(const,_) = cook_proof () in delete_current_proof (); const, status with reraise -> diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 9762d415f..c3d0c9053 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 -> - unit declaration_hook -> Proof_global.proof_terminator -> unit + Proof_global.proof_terminator -> unit (** {6 ... } *) (** [cook_proof opacity] turns the current proof (assumed completed) into @@ -70,16 +70,14 @@ val start_proof : it fails if there is no current proof of if it is not completed; it also tells if the guardness condition has to be inferred. *) -val cook_this_proof : (Proof.proof -> unit) -> +val cook_this_proof : Proof_global.proof_object -> (Id.t * - (Entries.definition_entry * goal_kind * - unit declaration_hook Ephemeron.key)) + (Entries.definition_entry * goal_kind)) -val cook_proof : (Proof.proof -> unit) -> +val cook_proof : unit -> (Id.t * - (Entries.definition_entry * goal_kind * - unit declaration_hook Ephemeron.key)) + (Entries.definition_entry * goal_kind)) (** {6 ... } *) (** [get_pftreestate ()] returns the current focused pending proof. @@ -100,7 +98,7 @@ val get_current_goal_context : unit -> Evd.evar_map * env (** [current_proof_statement] *) val current_proof_statement : - unit -> Id.t * goal_kind * types * unit declaration_hook Ephemeron.key + unit -> Id.t * goal_kind * types (** {6 ... } *) (** [get_current_proof_name ()] return the name of the current focused diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 2534a1ec7..2f002e941 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -69,7 +69,6 @@ type proof_object = { id : Names.Id.t; entries : Entries.definition_entry list; persistence : Decl_kinds.goal_kind; - hook : unit Tacexpr.declaration_hook Ephemeron.key } type proof_ending = Vernacexpr.proof_end * proof_object @@ -84,7 +83,6 @@ type pstate = { section_vars : Context.section_context option; proof : Proof.proof; strength : Decl_kinds.goal_kind; - pr_hook : unit Tacexpr.declaration_hook Ephemeron.key; mode : proof_mode Ephemeron.key; } @@ -239,16 +237,13 @@ let _ = Errors.register_handler begin function | _ -> raise Errors.Unhandled end -(* [start_proof s str env t hook tac] 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); init_tac is possibly a tactic to - systematically apply at initialization time (e.g. to start the - proof of mutually dependent theorems). - It raises exception [ProofInProgress] if there is a proof being - currently edited. *) +(* [start_proof id str goals terminator] starts a proof of name [id] + with goals [goals] (a list of pairs of environment and + conclusion); at the end of the proof [terminator] is called to + close the proof. It raises exception [ProofInProgress] if there + is a proof being currently edited. *) -let start_proof id str goals hook terminator = +let start_proof id str goals terminator = let initial_state = { pid = id; terminator = Ephemeron.create terminator; @@ -256,11 +251,10 @@ let start_proof id str goals hook terminator = endline_tactic = None; section_vars = None; strength = str; - pr_hook = Ephemeron.create hook; mode = find_proof_mode "No" } in push initial_state pstates -let start_dependent_proof id str goals hook terminator = +let start_dependent_proof id str goals terminator = let initial_state = { pid = id; terminator = Ephemeron.create terminator; @@ -268,7 +262,6 @@ let start_dependent_proof id str goals hook terminator = endline_tactic = None; section_vars = None; strength = str; - pr_hook = Ephemeron.create hook; mode = find_proof_mode "No" } in push initial_state pstates @@ -288,46 +281,45 @@ let set_used_variables l = let get_open_goals () = let gl, gll, shelf , _ , _ = Proof.proof (cur_pstate ()).proof in List.length gl + - List.fold_left (+) 0 + List.fold_left (+) 0 (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) + - List.length shelf + List.length shelf let close_proof ~now fpl = - let { pid;section_vars;strength;pr_hook;proof;terminator } = + let { pid;section_vars;strength;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; - const_entry_secctx = section_vars; - const_entry_type = Some t; - const_entry_inline_code = false; - const_entry_opaque = true }) fpl initial_goals in + const_entry_body = p; + const_entry_secctx = section_vars; + const_entry_type = Some t; + const_entry_inline_code = false; + const_entry_opaque = true }) fpl initial_goals in if now then List.iter (fun x -> ignore(Future.join x.Entries.const_entry_body)) entries; { id = pid ; entries = entries ; - persistence = strength ; - hook = pr_hook } , terminator + persistence = strength } , terminator let return_proof () = let { proof } = cur_pstate () in let initial_goals = Proof.initial_goals proof in let evd = - try Proof.return proof with - | Proof.UnfinishedProof -> - raise (Errors.UserError("last tactic before Qed", - str"Attempt to save an incomplete proof")) - | Proof.HasShelvedGoals -> - raise (Errors.UserError("last tactic before Qed", - str"Attempt to save a proof with shelved goals")) - | Proof.HasGivenUpGoals -> - raise (Errors.UserError("last tactic before Qed", - str"Attempt to save a proof with given up goals")) - | Proof.HasUnresolvedEvar -> - raise (Errors.UserError("last tactic before Qed", - str"Attempt to save a proof with existential " ++ - str"variables still non-instantiated")) + try Proof.return proof with + | Proof.UnfinishedProof -> + raise (Errors.UserError("last tactic before Qed", + str"Attempt to save an incomplete proof")) + | Proof.HasShelvedGoals -> + raise (Errors.UserError("last tactic before Qed", + str"Attempt to save a proof with shelved goals")) + | Proof.HasGivenUpGoals -> + raise (Errors.UserError("last tactic before Qed", + str"Attempt to save a proof with given up goals")) + | Proof.HasUnresolvedEvar -> + raise (Errors.UserError("last tactic before Qed", + str"Attempt to save a proof with existential " ++ + str"variables still non-instantiated")) in let eff = Evd.eval_side_effects evd in (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate @@ -483,8 +475,8 @@ let _ = module V82 = struct let get_current_initial_conclusions () = - let { pid; strength; pr_hook; proof } = cur_pstate () in - pid, (List.map snd (Proof.initial_goals proof), strength, pr_hook) + let { pid; strength; proof } = cur_pstate () in + pid, (List.map snd (Proof.initial_goals proof), strength) end type state = pstate list diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 71d03438b..ed7668d57 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -57,7 +57,6 @@ type proof_object = { id : Names.Id.t; entries : Entries.definition_entry list; persistence : Decl_kinds.goal_kind; - hook : unit Tacexpr.declaration_hook Ephemeron.key } type proof_ending = Vernacexpr.proof_end * proof_object @@ -73,7 +72,6 @@ type closed_proof = proof_object*proof_terminator Ephemeron.key val start_proof : Names.Id.t -> Decl_kinds.goal_kind -> (Environ.env * Term.types) list -> - unit Tacexpr.declaration_hook -> proof_terminator -> unit (** Like [start_proof] except that there may be dependencies between @@ -81,7 +79,6 @@ val start_proof : Names.Id.t -> val start_dependent_proof : Names.Id.t -> Decl_kinds.goal_kind -> Proofview.telescope -> - unit Tacexpr.declaration_hook -> proof_terminator -> unit @@ -177,7 +174,7 @@ val get_default_goal_selector : unit -> Vernacexpr.goal_selector module V82 : sig val get_current_initial_conclusions : unit -> Names.Id.t *(Term.types list * - Decl_kinds.goal_kind * unit Tacexpr.declaration_hook Ephemeron.key) + Decl_kinds.goal_kind) end type state diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index 9d7a58ff0..b0c04556f 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -280,8 +280,8 @@ let save_anonymous_with_strength proof kind save_ident = (* Admitted *) -let admit () = - let (id,k,typ,hook) = Pfedit.current_proof_statement () in +let admit hook () = + let (id,k,typ) = Pfedit.current_proof_statement () in let e = Pfedit.get_used_variables(), typ, None in let kn = declare_constant id (ParameterEntry e,IsAssumption Conjectural) in let () = match fst k with @@ -299,19 +299,20 @@ let start_hook = ref ignore let set_start_hook = (:=) start_hook -let get_proof proof do_guard opacity = - let (id,(const,persistence,hook)) = - Pfedit.cook_this_proof !save_hook proof +let get_proof proof do_guard hook opacity = + let (id,(const,persistence)) = + Pfedit.cook_this_proof proof in id,{const with const_entry_opaque = opacity},do_guard,persistence,hook let start_proof id kind ?sign c ?init_tac ?(compute_guard=[]) hook = + let hook = Ephemeron.create hook in let terminator = let open Vernacexpr in function | Admitted,_ -> - admit (); + admit hook (); Pp.feedback Interface.AddedAxiom | Proved (is_opaque,idopt),proof -> - let proof = get_proof proof compute_guard is_opaque in + let proof = get_proof proof compute_guard hook is_opaque in begin match idopt with | None -> save_named proof | Some ((_,id),None) -> save_anonymous proof id @@ -325,7 +326,7 @@ let start_proof id kind ?sign c ?init_tac ?(compute_guard=[]) hook = | None -> initialize_named_context_for_proof () in !start_hook c; - Pfedit.start_proof id kind sign c ?init_tac hook terminator + Pfedit.start_proof id kind sign c ?init_tac terminator let rec_tac_initializer finite guard thms snl = |