Permalink
Browse files

Factoring(continued).

This commit removes the hook.
  • Loading branch information...
1 parent eaa9c14 commit f1a2c15b7a7d7edfd4b4b379ed0bde8b1f5deb7b @aspiwack aspiwack committed Nov 27, 2013
@@ -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))
@@ -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
@@ -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)
@@ -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
;;
View
@@ -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 ->
View
@@ -62,24 +62,22 @@ 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
a constant with its name, kind and possible hook (see [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
@@ -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,36 +237,31 @@ 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;
proof = Proof.start Evd.empty goals;
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;
proof = Proof.dependent_start Evd.empty goals;
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
@@ -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,15 +72,13 @@ 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
initial goals. *)
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
View
@@ -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 =

0 comments on commit f1a2c15

Please sign in to comment.