From a2ea73d84be2fe95eeda42f5f5ac458f0af9968f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 24 Feb 2019 01:57:59 +0100 Subject: [proofs] Store hooks in the proof object. As of now, hooks were stored in the terminators as closures, we place them instead in the proof object and are thus passed back at proof closing time. This helps towards the reification and unification of terminators. --- plugins/derive/derive.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins') diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index aad3967f6d..f8b5f455d1 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -56,9 +56,9 @@ let start_deriving f suchthat name : Lemmas.t = let (opaque,f_def,lemma_def) = match com with | Lemmas.Admitted _ -> CErrors.user_err Pp.(str "Admitted isn't supported in Derive.") - | Lemmas.Proved (_,Some _,_) -> + | Lemmas.Proved (_,Some _,_, _) -> CErrors.user_err Pp.(str "Cannot save a proof of Derive with an explicit name.") - | Lemmas.Proved (opaque, None, obj) -> + | Lemmas.Proved (opaque, None, obj,_) -> match Proof_global.(obj.entries) with | [_;f_def;lemma_def] -> opaque <> Proof_global.Transparent , f_def , lemma_def -- cgit v1.2.3 From 7dc04f0244aeb277b62070f87590cbc2cafd8396 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 24 Feb 2019 20:27:09 +0100 Subject: [proof] drop parameter from terminator type This makes the type of terminator simpler, progressing towards its total reification. --- plugins/derive/derive.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins') diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index f8b5f455d1..0f0bec0129 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -56,9 +56,9 @@ let start_deriving f suchthat name : Lemmas.t = let (opaque,f_def,lemma_def) = match com with | Lemmas.Admitted _ -> CErrors.user_err Pp.(str "Admitted isn't supported in Derive.") - | Lemmas.Proved (_,Some _,_, _) -> + | Lemmas.Proved (_,Some _,_,_,_) -> CErrors.user_err Pp.(str "Cannot save a proof of Derive with an explicit name.") - | Lemmas.Proved (opaque, None, obj,_) -> + | Lemmas.Proved (opaque, None, obj,_,_) -> match Proof_global.(obj.entries) with | [_;f_def;lemma_def] -> opaque <> Proof_global.Transparent , f_def , lemma_def @@ -99,7 +99,7 @@ let start_deriving f suchthat name : Lemmas.t = ignore (Declare.declare_constant name lemma_def) in - let terminator ?hook _ = Lemmas.Internal.make_terminator terminator in + let terminator = Lemmas.Internal.make_terminator terminator in let lemma = Lemmas.start_dependent_lemma name kind goals ~terminator in Lemmas.pf_map (Proof_global.map_proof begin fun p -> Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p -- cgit v1.2.3 From 873281c256fc33941d93044acc3db8eda0a148ee Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 24 Feb 2019 20:38:21 +0100 Subject: [proof] Move declaration hooks to DeclareDef. This way both `Lemmas` and `DeclareObl` can depend on it, removing one more difficulty on the unification of terminators. --- plugins/funind/functional_principles_types.ml | 2 +- plugins/funind/indfun_common.ml | 2 +- plugins/funind/indfun_common.mli | 2 +- plugins/funind/recdef.ml | 4 ++-- plugins/ltac/rewrite.ml | 2 +- 5 files changed, 6 insertions(+), 6 deletions(-) (limited to 'plugins') diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 8af5dc818b..08acb754f7 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -307,7 +307,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin in let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd (EConstr.of_constr new_principle_type) in evd := sigma; - let hook = Lemmas.mk_hook (hook new_principle_type) in + let hook = DeclareDef.Hook.make (hook new_principle_type) in let lemma = Lemmas.start_lemma new_princ_name diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 7683ce1757..732a0d818f 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -137,7 +137,7 @@ let save id const ?hook uctx (locality,_,kind) = let kn = declare_constant id ~local (DefinitionEntry const, k) in ConstRef kn in - Lemmas.call_hook ?hook ~fix_exn uctx [] locality r; + DeclareDef.Hook.call ?hook ~fix_exn uctx [] locality r; definition_message id let with_full_print f a = diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 4078c34331..8dd990775b 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -45,7 +45,7 @@ val jmeq_refl : unit -> EConstr.constr val save : Id.t -> Evd.side_effects Entries.definition_entry - -> ?hook:Lemmas.declaration_hook + -> ?hook:DeclareDef.Hook.t -> UState.t -> Decl_kinds.goal_kind -> unit diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 2b5c0a01db..8169ff459f 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1371,7 +1371,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type let lemma = Lemmas.start_lemma na Decl_kinds.(Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma) - sigma gls_type ~hook:(Lemmas.mk_hook hook) in + sigma gls_type ~hook:(DeclareDef.Hook.make hook) in let lemma = if Indfun_common.is_strict_tcc () then fst @@ Lemmas.by (Proofview.V82.tactic (tclIDTAC)) lemma @@ -1592,5 +1592,5 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type term_id using_lemmas (List.length res_vars) - evd (Lemmas.mk_hook hook)) + evd (DeclareDef.Hook.make hook)) () diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 2da6584aba..2bab55ef74 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -2006,7 +2006,7 @@ let add_morphism_interactive atts m n : Lemmas.t = declare_projection n instance_id (ConstRef cst) | _ -> assert false in - let hook = Lemmas.mk_hook hook in + let hook = DeclareDef.Hook.make hook in Flags.silently (fun () -> let lemma = Lemmas.start_lemma ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in -- cgit v1.2.3 From 9b97d4368aa714aa5f0ae0a91bec7bab7eb1a394 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 24 Feb 2019 20:40:34 +0100 Subject: [proof] Remove terminator type, unifying regular and obligation ones. We radically redesign how proof closing information is stored. Instead of a user-defined closure, we now reify control into a single data structure containing the needed information. In this scheme, the `Lemmas` module can get extra information with obligation info when opening the proof, and will correspondingly call the right closing function based on this. This is the start of what could be a much bigger unification of all the proof save paths. --- plugins/derive/derive.ml | 78 ++++++------------------------------------------ 1 file changed, 9 insertions(+), 69 deletions(-) (limited to 'plugins') diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 0f0bec0129..0447b79dcd 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -8,16 +8,9 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Constr open Context open Context.Named.Declaration -let map_const_entry_body (f:constr->constr) (x: Evd.side_effects Entries.const_entry_body) - : Evd.side_effects Entries.const_entry_body = - Future.chain x begin fun ((b,ctx),fx) -> - (f b , ctx) , fx - end - (** [start_deriving f suchthat lemma] starts a proof of [suchthat] (which can contain references to [f]) in the context extended by [f:=?x]. When the proof ends, [f] is defined as the value of [?x] @@ -36,71 +29,18 @@ let start_deriving f suchthat name : Lemmas.t = (* create the initial goals for the proof: |- Type ; |- ?1 ; f:=?2 |- suchthat *) let goals = let open Proofview in - TCons ( env , sigma , f_type_type , (fun sigma f_type -> + TCons ( env , sigma , f_type_type , (fun sigma f_type -> TCons ( env , sigma , f_type , (fun sigma ef -> - let f_type = EConstr.Unsafe.to_constr f_type in - let ef = EConstr.Unsafe.to_constr ef in - let env' = Environ.push_named (LocalDef (annotR f, ef, f_type)) env in - let sigma, suchthat = Constrintern.interp_type_evars ~program_mode:false env' sigma suchthat in - TCons ( env' , sigma , suchthat , (fun sigma _ -> - TNil sigma)))))) - in - - (* The terminator handles the registering of constants when the proof is closed. *) - let terminator com = - (* Extracts the relevant information from the proof. [Admitted] - and [Save] result in user errors. [opaque] is [true] if the - proof was concluded by [Qed], and [false] if [Defined]. [f_def] - and [lemma_def] correspond to the proof of [f] and of - [suchthat], respectively. *) - let (opaque,f_def,lemma_def) = - match com with - | Lemmas.Admitted _ -> CErrors.user_err Pp.(str "Admitted isn't supported in Derive.") - | Lemmas.Proved (_,Some _,_,_,_) -> - CErrors.user_err Pp.(str "Cannot save a proof of Derive with an explicit name.") - | Lemmas.Proved (opaque, None, obj,_,_) -> - match Proof_global.(obj.entries) with - | [_;f_def;lemma_def] -> - opaque <> Proof_global.Transparent , f_def , lemma_def - | _ -> assert false - in - (* The opacity of [f_def] is adjusted to be [false], as it - must. Then [f] is declared in the global environment. *) - let f_def = { f_def with Entries.const_entry_opaque = false } in - let f_def = Entries.DefinitionEntry f_def , Decl_kinds.(IsDefinition Definition) in - let f_kn = Declare.declare_constant f f_def in - let f_kn_term = mkConst f_kn in - (* In the type and body of the proof of [suchthat] there can be - references to the variable [f]. It needs to be replaced by - references to the constant [f] declared above. This substitution - performs this precise action. *) - let substf c = Vars.replace_vars [f,f_kn_term] c in - (* Extracts the type of the proof of [suchthat]. *) - let lemma_pretype = - match Entries.(lemma_def.const_entry_type) with - | Some t -> t - | None -> assert false (* Proof_global always sets type here. *) - in - (* The references of [f] are subsituted appropriately. *) - let lemma_type = substf lemma_pretype in - (* The same is done in the body of the proof. *) - let lemma_body = - map_const_entry_body substf Entries.(lemma_def.const_entry_body) - in - let lemma_def = let open Entries in { lemma_def with - const_entry_body = lemma_body ; - const_entry_type = Some lemma_type ; - const_entry_opaque = opaque ; } - in - let lemma_def = - Entries.DefinitionEntry lemma_def , - Decl_kinds.(IsProof Proposition) - in - ignore (Declare.declare_constant name lemma_def) + let f_type = EConstr.Unsafe.to_constr f_type in + let ef = EConstr.Unsafe.to_constr ef in + let env' = Environ.push_named (LocalDef (annotR f, ef, f_type)) env in + let sigma, suchthat = Constrintern.interp_type_evars ~program_mode:false env' sigma suchthat in + TCons ( env' , sigma , suchthat , (fun sigma _ -> + TNil sigma)))))) in - let terminator = Lemmas.Internal.make_terminator terminator in - let lemma = Lemmas.start_dependent_lemma name kind goals ~terminator in + let proof_ending = Lemmas.Proof_ending.(End_derive {f; name}) in + let lemma = Lemmas.start_dependent_lemma name kind goals ~proof_ending in Lemmas.pf_map (Proof_global.map_proof begin fun p -> Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p end) lemma -- cgit v1.2.3