From 5f937b2f8532b2ccf36c62557934cc2c9150005b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 9 Mar 2020 06:32:00 -0400 Subject: [proof] Miscellaneous cleanup on proof info handling After the refactorings proof information is organized in a slightly different way thus the lower layers don't need to pass info back anymore. --- plugins/funind/gen_principle.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins') diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 446026c4c8..28cf5c7d98 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -199,7 +199,7 @@ let build_functional_principle ?(opaque=Proof_global.Transparent) (evd:Evd.evar_ (* end; *) let open Proof_global in - let { name; entries } = Lemmas.pf_fold (close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x)) lemma in + let { entries } = Lemmas.pf_fold (close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x)) lemma in match entries with | [entry] -> entry, hook -- cgit v1.2.3 From 9be8376b9c8b1b3fc9b37d1617b26ef54b172ca6 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 14 Mar 2020 02:27:54 -0400 Subject: [ComDefinition] Split program from regular declarations Proof "preparation" [as in `DeclareDef.prepare_definition`] is fairly more complicated in the Program case; in particular, it includes checking the existential variables, and elaborating a list of entries from the holes. Indeed, in the `Program` case we cannot use `DeclareDef.prepare_definition` while keeping a good level of abstraction, so we should introduce a `prepare_obligation` function. This PR is in preparation for that. --- plugins/funind/gen_principle.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'plugins') diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 28cf5c7d98..4242da2802 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -375,7 +375,6 @@ let register_struct is_rec fixpoint_exprl = | None -> CErrors.user_err ~hdr:"Function" Pp.(str "Body of Function must be given") in ComDefinition.do_definition - ~program_mode:false ~name:fname.CAst.v ~poly:false ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) -- 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 --- plugins/funind/gen_principle.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'plugins') diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 4242da2802..47e56b81aa 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -291,6 +291,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) *) let uctx = Evd.evar_universe_context sigma in let hook_data = hook, uctx, [] in + let entry = DeclareDef.ClosedDef.of_proof_entry entry in let _ : Names.GlobRef.t = DeclareDef.declare_definition ~name:new_princ_name ~hook_data ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) -- 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. --- plugins/funind/gen_principle.ml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'plugins') diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 47e56b81aa..ebd280ecf6 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -290,13 +290,11 @@ let generate_functional_principle (evd: Evd.evar_map ref) Don't forget to close the goal if an error is raised !!!! *) let uctx = Evd.evar_universe_context sigma in - let hook_data = hook, uctx, [] in - let entry = DeclareDef.ClosedDef.of_proof_entry entry in + let entry = DeclareDef.ClosedDef.of_proof_entry ~uctx entry in let _ : Names.GlobRef.t = DeclareDef.declare_definition - ~name:new_princ_name ~hook_data + ~name:new_princ_name ~hook ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~kind:Decls.(IsProof Theorem) - ~ubind:UnivNames.empty_binders ~impargs:[] entry in () -- 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`. --- plugins/funind/gen_principle.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'plugins') diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index ebd280ecf6..45c46c56f4 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -290,13 +290,12 @@ let generate_functional_principle (evd: Evd.evar_map ref) Don't forget to close the goal if an error is raised !!!! *) let uctx = Evd.evar_universe_context sigma in - let entry = DeclareDef.ClosedDef.of_proof_entry ~uctx entry in - let _ : Names.GlobRef.t = DeclareDef.declare_definition + let _ : Names.GlobRef.t = DeclareDef.declare_entry ~name:new_princ_name ~hook ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~kind:Decls.(IsProof Theorem) ~impargs:[] - entry in + ~uctx entry in () with e when CErrors.noncritical e -> raise (Defining_principle e) -- cgit v1.2.3