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. --- stm/stm.ml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index d77e37c910..a0247e0d8f 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1532,14 +1532,15 @@ end = struct (* {{{ *) (* Unfortunately close_future_proof and friends are not pure so we need to set the state manually here *) State.unfreeze st; - let pobject, _ = + let pobject, _terminator, _hook = PG_compat.close_future_proof ~opaque ~feedback_id:stop (Future.from_val ~fix_exn p) in + let terminator = (* The one sent by master is an InvalidKey *) Lemmas.(standard_proof_terminator []) in let st = Vernacstate.freeze_interp_state ~marshallable:false in stm_vernac_interp stop - ~proof:(pobject, terminator) st + ~proof:(pobject, terminator, None) st { verbose = false; indentation = 0; strlen = 0; expr = CAst.make ?loc @@ VernacExpr ([], VernacEndProof (Proved (opaque,None))) }) in ignore(Future.join checked_proof); @@ -1676,10 +1677,10 @@ end = struct (* {{{ *) let opaque = Proof_global.Opaque in (* The original terminator, a hook, has not been saved in the .vio*) - let pterm, _invalid_terminator = + let pterm, _invalid_terminator, _hook = PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in - let proof = pterm , Lemmas.standard_proof_terminator [] in + let proof = pterm , Lemmas.standard_proof_terminator [], None in (* We jump at the beginning since the kernel handles side effects by also * looking at the ones that happen to be present in the current env *) @@ -1734,7 +1735,7 @@ end = struct (* {{{ *) | `ERROR -> exit 1 | `ERROR_ADMITTED -> cst, false | `OK_ADMITTED -> cst, false - | `OK (po,_) -> + | `OK (po,_,_) -> let con = Nametab.locate_constant (Libnames.qualid_of_ident po.Proof_global.id) in -- cgit v1.2.3 From a296e879112f2e88b2fdfbf2fe90f1807f90b890 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 24 Feb 2019 02:24:47 +0100 Subject: [proof] Unify obligation proof save path: Part I, declareObl We move obligation declaration-specific functions to their own file. This way, `Lemmas` can access them, and in the next part we can factorize common parts in the save proof. --- 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 a0247e0d8f..4f435f1fa5 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -208,7 +208,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, - Obligations.program_tcc_summary_tag + DeclareObl.program_tcc_summary_tag type cached_state = | EmptyState @@ -884,7 +884,7 @@ end = struct (* {{{ *) Lemmas.Stack.t option * int * (* Evarutil.meta_counter_summary_tag *) int * (* Evd.evar_counter_summary_tag *) - Obligations.program_info Names.Id.Map.t (* Obligations.program_tcc_summary_tag *) + DeclareObl.program_info CEphemeron.key Names.Id.Map.t (* Obligations.program_tcc_summary_tag *) type partial_state = [ `Full of Vernacstate.t @@ -3238,7 +3238,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 Obligations.stm_get_fix_exn (fun () -> !State.fix_exn_ref) +let () = Hook.set DeclareObl.stm_get_fix_exn (fun () -> !State.fix_exn_ref) type document = VCS.vcs let backup () = VCS.backup () -- 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. --- stm/stm.ml | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 4f435f1fa5..13996aca0f 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1532,15 +1532,12 @@ end = struct (* {{{ *) (* Unfortunately close_future_proof and friends are not pure so we need to set the state manually here *) State.unfreeze st; - let pobject, _terminator, _hook = + let pobject, _info = PG_compat.close_future_proof ~opaque ~feedback_id:stop (Future.from_val ~fix_exn p) in - let terminator = (* The one sent by master is an InvalidKey *) - Lemmas.(standard_proof_terminator []) in - let st = Vernacstate.freeze_interp_state ~marshallable:false in stm_vernac_interp stop - ~proof:(pobject, terminator, None) st + ~proof:(pobject, Lemmas.default_info) st { verbose = false; indentation = 0; strlen = 0; expr = CAst.make ?loc @@ VernacExpr ([], VernacEndProof (Proved (opaque,None))) }) in ignore(Future.join checked_proof); @@ -1677,10 +1674,10 @@ end = struct (* {{{ *) let opaque = Proof_global.Opaque in (* The original terminator, a hook, has not been saved in the .vio*) - let pterm, _invalid_terminator, _hook = + let pterm, _info = PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in - let proof = pterm , Lemmas.standard_proof_terminator [], None in + let proof = pterm, Lemmas.default_info in (* We jump at the beginning since the kernel handles side effects by also * looking at the ones that happen to be present in the current env *) @@ -1735,7 +1732,7 @@ end = struct (* {{{ *) | `ERROR -> exit 1 | `ERROR_ADMITTED -> cst, false | `OK_ADMITTED -> cst, false - | `OK (po,_,_) -> + | `OK (po,_) -> let con = Nametab.locate_constant (Libnames.qualid_of_ident po.Proof_global.id) in -- cgit v1.2.3