From 809291d5ef7371bfe8841b95126c0332da55578f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 15 Mar 2020 17:52:16 -0400 Subject: [obligations] Pre-functionalize Program state In our quest to unify all the declaration paths, an important step is to account for the state pertaining to `Program` declarations. Whereas regular proofs keep are kept in a stack-like structure; obligations for constants defined by `Program` are stored in a global map which is manipulated by almost regular open/close proof primitives. This PR is in preparation for the switch to a purely functional state in #11836 ; the full switch requires deeper changes so it is helpful to have this PR preparing most of the structure. Most of the PR is routine; only remarkable change is that the hook for admitted obligations is now called explicitly in `finish_admitted` as it had to learn about the different types of proof_endings. Before, obligations set it in `start_lemma` but only used in the `Admitted` path. --- stm/stm.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index b296f8f08f..aa5a14c7dd 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -202,7 +202,7 @@ let mkTransCmd cast cids ceff cqueue = (* Parts of the system state that are morally part of the proof state *) let summary_pstate = Evarutil.meta_counter_summary_tag, Evd.evar_counter_summary_tag, - DeclareObl.program_tcc_summary_tag + DeclareObl.State.prg_tag type cached_state = | EmptyState @@ -878,7 +878,7 @@ end = struct (* {{{ *) Vernacstate.LemmaStack.t option * int * (* Evarutil.meta_counter_summary_tag *) int * (* Evd.evar_counter_summary_tag *) - DeclareObl.ProgramDecl.t CEphemeron.key Names.Id.Map.t (* Obligations.program_tcc_summary_tag *) + DeclareObl.State.t type partial_state = [ `Full of Vernacstate.t -- cgit v1.2.3 From c8b54d74bc7cf29cc04d0a3cedbf4a106f6e744c Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 4 May 2020 11:18:34 +0200 Subject: [declare] Merge `DeclareObl` into `Declare` This is needed as a first step to refactor and unify the obligation save path and state; in particular `Equations` is a heavy user of Hooks to modify obligations state, thus in order to make the hook aware of this we need to place the obligation state before the hook. As a good side-effect, `inline_private_constants` and `Hook.call` are not exported from `Declare` anymore. --- stm/stm.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index aa5a14c7dd..177a76e64b 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -202,7 +202,7 @@ let mkTransCmd cast cids ceff cqueue = (* Parts of the system state that are morally part of the proof state *) let summary_pstate = Evarutil.meta_counter_summary_tag, Evd.evar_counter_summary_tag, - DeclareObl.State.prg_tag + Declare.Obls.State.prg_tag type cached_state = | EmptyState @@ -878,7 +878,7 @@ end = struct (* {{{ *) Vernacstate.LemmaStack.t option * int * (* Evarutil.meta_counter_summary_tag *) int * (* Evd.evar_counter_summary_tag *) - DeclareObl.State.t + Declare.Obls.State.t type partial_state = [ `Full of Vernacstate.t @@ -3308,7 +3308,7 @@ let unreachable_state_hook = Hooks.unreachable_state_hook let document_add_hook = Hooks.document_add_hook let document_edit_hook = Hooks.document_edit_hook let sentence_exec_hook = Hooks.sentence_exec_hook -let () = Hook.set DeclareObl.stm_get_fix_exn (fun () -> !State.fix_exn_ref) +let () = Declare.Obls.stm_get_fix_exn := (fun () -> !State.fix_exn_ref) type document = VCS.vcs let backup () = VCS.backup () -- cgit v1.2.3 From 5ae026cebc6c468373459af950533bee0c02501a Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 11 May 2020 04:09:31 +0200 Subject: [declare] Grand unification of the proof save path. We complete some arduous refactoring in order to bring all the internals and code of constant / proof saving into the same module. In particular, this PR moves the remaining parts of proof saving from `Lemmas` to `Declare`. The reduction in exposed internals is considerable; in particular, we remove the export of the internals of `proof_entry` and `proof_object` [used in delayed proofs], which will allow us to start to address many issues with the current setup, such as #10363 . There are still some TODOs, that will be addressed in subsequent PRs: - Remove `declare_constant` in favor of higher-level APIs - Then, remove access to `proof_entry` entirely - Refactor current very verbose handling of proof info. - Remove compat modules / API. - Rework handling of delayed proofs [this may be hard due to state and the STM] - Reify Hook API for the case where it acts as a continuation [that is to say, declaring constants from the Hook] List of remaining offenders for `proof_entry` / `declare_constant` in the codebase: - File "vernac/comHints.ml" - File "vernac/indschemes.ml" - File "vernac/comProgramFixpoint.ml" - File "vernac/comAssumption.ml" - File "vernac/record.ml" - File "plugins/ltac/leminv.ml" - File "plugins/setoid_ring/newring.ml" - File "plugins/funind/recdef.ml" - File "plugins/funind/gen_principle.ml" --- stm/stm.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 177a76e64b..04f08e488b 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1684,7 +1684,9 @@ end = struct (* {{{ *) (* STATE We use the state resulting from reaching start. *) let st = Vernacstate.freeze_interp_state ~marshallable:false in ignore(stm_qed_delay_proof ~id:stop ~st ~proof ~info ~loc ~control:[] (Proved (opaque,None))); - `OK proof + (* Is this name the same than the one in scope? *) + let name = Declare.get_po_name proof in + `OK name end with e -> let (e, info) = Exninfo.capture e in @@ -1723,7 +1725,7 @@ end = struct (* {{{ *) | `ERROR -> exit 1 | `ERROR_ADMITTED -> cst, false | `OK_ADMITTED -> cst, false - | `OK { Declare.name } -> + | `OK name -> let con = Nametab.locate_constant (Libnames.qualid_of_ident name) in let c = Global.lookup_constant con in let o = match c.Declarations.const_body with -- cgit v1.2.3