From 56ffe818ab7706a82d79b538fdf3af8b23d95f40 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 14 Mar 2020 03:07:42 -0400 Subject: [declare] [obligations] Refactor preparation of obligation entry Preparation of obligation/program entries requires low-level manipulation that does break the abstraction over `proof_entry`; we thus introduce `prepare_obligation`, and move the code that prepares the obligation entry to its own module. This seems to improve separation of concerns, and helps clarify the two of three current models in which Coq operates w.r.t. definitions: - single, ground entries with possibly mutual definitions [regular lemmas] - single, non-ground entries with possibly mutual definitions [obligations] - multiple entries [equations] --- vernac/classes.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'vernac/classes.ml') diff --git a/vernac/classes.ml b/vernac/classes.ml index dafd1cc5e4..e0bf9e777c 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -315,7 +315,7 @@ let instance_hook info global imps ?hook cst = let declare_instance_constant info global imps ?hook name udecl poly sigma term termtype = let kind = Decls.(IsDefinition Instance) in let sigma, entry = DeclareDef.prepare_definition - ~allow_evars:false ~poly sigma ~udecl ~types:(Some termtype) ~body:term in + ~poly sigma ~udecl ~types:(Some termtype) ~body:term in let kn = Declare.declare_constant ~name ~kind (Declare.DefinitionEntry entry) in Declare.definition_message name; DeclareUniv.declare_univ_binders (GlobRef.ConstRef kn) (Evd.universe_binders sigma); @@ -343,7 +343,7 @@ let declare_instance_program env sigma ~global ~poly name pri imps udecl term te let sigma = Evd.from_env env in declare_instance env sigma (Some pri) (not global) (GlobRef.ConstRef cst) in - let obls, _, term, typ = Obligations.eterm_obligations env name sigma 0 term termtype in + let obls, _, term, typ = RetrieveObl.retrieve_obligations env name sigma 0 term termtype in let hook = DeclareDef.Hook.make hook in let uctx = Evd.evar_universe_context sigma in let scope, kind = DeclareDef.Global Declare.ImportDefaultBehavior, Decls.Instance in -- cgit v1.2.3 From d507679b5b6dfac944e038b6a3ebd9fb8e6998ff Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 14 Mar 2020 03:19:15 -0400 Subject: [declareDef] Cleanup of allow_evars and check_evars We don't the parameter anymore as the paths are too different now. Note that this removes a duplicate `check_evars` that has been in `master` quite some time [double check in `ComDefinition` and in `DeclareDef.prepare_definition`] --- vernac/classes.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/classes.ml') diff --git a/vernac/classes.ml b/vernac/classes.ml index e0bf9e777c..65d20a13a1 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -328,7 +328,7 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst in let (_, ty_constr) = instance_constructor (k,u) subst in let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in - let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma ~udecl ~types:termtype in + let sigma, entry = DeclareDef.prepare_parameter ~poly sigma ~udecl ~types:termtype in let cst = Declare.declare_constant ~name ~kind:Decls.(IsAssumption Logical) (Declare.ParameterEntry entry) in DeclareUniv.declare_univ_binders (GlobRef.ConstRef cst) (Evd.universe_binders sigma); -- cgit v1.2.3 From 8ac27a8261f5f3fb5d4bf2a207a144df07477910 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 14 Mar 2020 03:42:57 -0400 Subject: [declare] Make the type of closed entries opaque. This is a step in forcing all entry creation go thru the preparation functions. We still need to handle plain `Declare.` calls, but this will be next step. We need to leave a backdoor for interactive proofs until we unify proof preparation happening in `Proof_global` with the one happening in `DeclareDef`, but we are getting there. TODO: see how to avoid the normalization problems in DeclareObl --- vernac/classes.ml | 23 ++++++++++++----------- 1 file changed, 12 insertions(+), 11 deletions(-) (limited to 'vernac/classes.ml') diff --git a/vernac/classes.ml b/vernac/classes.ml index 65d20a13a1..88b6ab34ff 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -304,22 +304,21 @@ let id_of_class cl = mip.(0).Declarations.mind_typename | _ -> assert false -let instance_hook info global imps ?hook cst = - Impargs.maybe_declare_manual_implicits false cst imps; +let instance_hook info global ?hook cst = let info = intern_info info in let env = Global.env () in let sigma = Evd.from_env env in declare_instance env sigma (Some info) (not global) cst; (match hook with Some h -> h cst | None -> ()) -let declare_instance_constant info global imps ?hook name udecl poly sigma term termtype = +let declare_instance_constant info global impargs ?hook name udecl poly sigma term termtype = let kind = Decls.(IsDefinition Instance) in let sigma, entry = DeclareDef.prepare_definition ~poly sigma ~udecl ~types:(Some termtype) ~body:term in - let kn = Declare.declare_constant ~name ~kind (Declare.DefinitionEntry entry) in - Declare.definition_message name; - DeclareUniv.declare_univ_binders (GlobRef.ConstRef kn) (Evd.universe_binders sigma); - instance_hook info global imps ?hook (GlobRef.ConstRef kn) + let ubind = Evd.universe_binders sigma in + let scope = DeclareDef.Global Declare.ImportDefaultBehavior in + let kn = DeclareDef.declare_definition ~name ~kind ~scope ~ubind ~impargs entry in + instance_hook info global ?hook kn let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst name = let subst = List.fold_left2 @@ -332,7 +331,9 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst let cst = Declare.declare_constant ~name ~kind:Decls.(IsAssumption Logical) (Declare.ParameterEntry entry) in DeclareUniv.declare_univ_binders (GlobRef.ConstRef cst) (Evd.universe_binders sigma); - instance_hook pri global impargs (GlobRef.ConstRef cst) + let cst = (GlobRef.ConstRef cst) in + Impargs.maybe_declare_manual_implicits false cst impargs; + instance_hook pri global cst let declare_instance_program env sigma ~global ~poly name pri imps udecl term termtype = let hook { DeclareDef.Hook.S.scope; dref; _ } = @@ -351,7 +352,7 @@ let declare_instance_program env sigma ~global ~poly name pri imps udecl term te Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook typ ~uctx obls in () -let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids term termtype = +let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl ids term termtype = (* spiwack: it is hard to reorder the actions to do the pretyping after the proof has opened. As a consequence, we use the low-level primitives to code @@ -359,12 +360,12 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids t let gls = List.rev (Evd.future_goals sigma) in let sigma = Evd.reset_future_goals sigma in let kind = Decls.(IsDefinition Instance) in - let hook = DeclareDef.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global imps ?hook dref)) in + let hook = DeclareDef.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global ?hook dref)) in let info = Lemmas.Info.make ~hook ~kind () in (* XXX: We need to normalize the type, otherwise Admitted / Qed will fails! This is due to a bug in proof_global :( *) let termtype = Evarutil.nf_evar sigma termtype in - let lemma = Lemmas.start_lemma ~name:id ~poly ~udecl ~info sigma termtype in + let lemma = Lemmas.start_lemma ~name:id ~poly ~udecl ~info ~impargs sigma termtype in (* spiwack: I don't know what to do with the status here. *) let lemma = match term with -- cgit v1.2.3 From 8fbc927ac40cc707b1a940d8339a2a289755d533 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 14 Mar 2020 16:34:30 -0400 Subject: [declareDef] More consistent handling of universe binders The only reasons that `prepare_definition` returned a sigma were: - to obtain the universe binders to be passed to declare - to obtain the UState.t to be passed to the equations hook We handle this automatically now; it seems like a reasonably good API improvement. However, it is not clear what we do now is right for all cases; must check. --- vernac/classes.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'vernac/classes.ml') diff --git a/vernac/classes.ml b/vernac/classes.ml index 88b6ab34ff..a882f6db0a 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -313,11 +313,10 @@ let instance_hook info global ?hook cst = let declare_instance_constant info global impargs ?hook name udecl poly sigma term termtype = let kind = Decls.(IsDefinition Instance) in - let sigma, entry = DeclareDef.prepare_definition + let entry = DeclareDef.prepare_definition ~poly sigma ~udecl ~types:(Some termtype) ~body:term in - let ubind = Evd.universe_binders sigma in let scope = DeclareDef.Global Declare.ImportDefaultBehavior in - let kn = DeclareDef.declare_definition ~name ~kind ~scope ~ubind ~impargs entry in + let kn = DeclareDef.declare_definition ~name ~kind ~scope ~impargs entry in instance_hook info global ?hook kn let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst name = -- cgit v1.2.3 From 7b2e166eae2d9f83bf0e14f68075b0be0a8bd668 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 14 Mar 2020 23:14:12 -0400 Subject: [classes] Declare obligation implicits using standard API. --- vernac/classes.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'vernac/classes.ml') diff --git a/vernac/classes.ml b/vernac/classes.ml index a882f6db0a..40c1a5d97d 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -334,10 +334,9 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst Impargs.maybe_declare_manual_implicits false cst impargs; instance_hook pri global cst -let declare_instance_program env sigma ~global ~poly name pri imps udecl term termtype = +let declare_instance_program env sigma ~global ~poly name pri impargs udecl term termtype = let hook { DeclareDef.Hook.S.scope; dref; _ } = let cst = match dref with GlobRef.ConstRef kn -> kn | _ -> assert false in - Impargs.declare_manual_implicits false dref imps; let pri = intern_info pri in let env = Global.env () in let sigma = Evd.from_env env in @@ -348,7 +347,7 @@ let declare_instance_program env sigma ~global ~poly name pri imps udecl term te let uctx = Evd.evar_universe_context sigma in let scope, kind = DeclareDef.Global Declare.ImportDefaultBehavior, Decls.Instance in let _ : DeclareObl.progress = - Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook typ ~uctx obls + Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook ~impargs ~uctx typ obls in () let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl ids term termtype = -- cgit v1.2.3 From 7d46a32dc928af64e3e111d6d62caa00f93c427c Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 18 Mar 2020 05:35:41 -0400 Subject: [declare] Fuse prepare and declare for the non-interactive path. This will allow to share the definition metadata for example with obligations; a bit more work is needed to finally move the preparation of interactive proofs from Proof_global to `prepare_entry`. --- vernac/classes.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'vernac/classes.ml') diff --git a/vernac/classes.ml b/vernac/classes.ml index 40c1a5d97d..6e929de581 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -313,10 +313,9 @@ let instance_hook info global ?hook cst = let declare_instance_constant info global impargs ?hook name udecl poly sigma term termtype = let kind = Decls.(IsDefinition Instance) in - let entry = DeclareDef.prepare_definition - ~poly sigma ~udecl ~types:(Some termtype) ~body:term in let scope = DeclareDef.Global Declare.ImportDefaultBehavior in - let kn = DeclareDef.declare_definition ~name ~kind ~scope ~impargs entry in + let kn = DeclareDef.declare_definition ~name ~kind ~scope ~impargs + ~opaque:false ~poly sigma ~udecl ~types:(Some termtype) ~body:term in instance_hook info global ?hook kn let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst name = -- cgit v1.2.3