From b755869a7fdb34dcf7dacc9d5fd93c768d71d751 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 26 Mar 2020 02:26:43 -0400 Subject: [proof] Split delayed and regular proof closing functions, part II We make the types of the delayed / non-delayed declaration path different, as the latter is just creating futures that are forced right away. TTBOMK the new code should behave identically w.r.t. old one, modulo the equation `Future.(force (from_val x)) = x`. There are some questions as what the code is doing, but in this PR I've opted to keep the code 100% faithful to the original one, unless I did a mistake. --- vernac/lemmas.ml | 2 +- vernac/vernacstate.ml | 4 ++-- vernac/vernacstate.mli | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) (limited to 'vernac') diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index feedf4d71d..7f7340bb34 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -403,7 +403,7 @@ let process_idopt_for_save ~idopt info = let save_lemma_proved ~lemma ~opaque ~idopt = (* Env and sigma are just used for error printing in save_remaining_recthms *) - let proof_obj = Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) lemma.proof in + let proof_obj = Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false lemma.proof in let proof_info = process_idopt_for_save ~idopt lemma.info in finalize_proof proof_obj proof_info diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index 6846826bfa..7c191a1f86 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -170,8 +170,8 @@ module Proof_global = struct cc_lemma (fun pt -> pf_fold (fun st -> close_future_proof ~opaque ~feedback_id st pf) pt, Internal.get_info pt) - let close_proof ~opaque ~keep_body_ucst_separate f = - cc_lemma (fun pt -> pf_fold ((close_proof ~opaque ~keep_body_ucst_separate f)) pt, + let close_proof ~opaque ~keep_body_ucst_separate = + cc_lemma (fun pt -> pf_fold ((close_proof ~opaque ~keep_body_ucst_separate)) pt, Internal.get_info pt) let discard_all () = s_lemmas := None diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli index 7607f8373a..2c9c7ecc6f 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -74,7 +74,7 @@ module Proof_global : sig feedback_id:Stateid.t -> Proof_global.closed_proof_output Future.computation -> closed_proof - val close_proof : opaque:Proof_global.opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof + val close_proof : opaque:Proof_global.opacity_flag -> keep_body_ucst_separate:bool -> closed_proof val discard_all : unit -> unit val update_global_env : unit -> unit -- cgit v1.2.3 From e9c05828bba7ceb696a5c17457b8e0826bbd94f1 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 26 Mar 2020 02:45:47 -0400 Subject: [proof] Split return_proof in partial and regular versions. This is a small refactoring as these two functions behave very differently and the invariants are quite different, in fact regular `return_proof` should not be exported but be part of close proof, but there is small use in the STM still. --- vernac/vernacstate.ml | 3 ++- vernac/vernacstate.mli | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) (limited to 'vernac') diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index 7c191a1f86..b722acd1ad 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -164,7 +164,8 @@ module Proof_global = struct type closed_proof = Proof_global.proof_object * Lemmas.Info.t - let return_proof ?allow_partial () = cc (return_proof ?allow_partial) + let return_proof () = cc return_proof + let return_partial_proof () = cc return_partial_proof let close_future_proof ~opaque ~feedback_id pf = cc_lemma (fun pt -> pf_fold (fun st -> close_future_proof ~opaque ~feedback_id st pf) pt, diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli index 2c9c7ecc6f..b6b24c9275 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -65,7 +65,8 @@ module Proof_global : sig val with_current_proof : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> 'a - val return_proof : ?allow_partial:bool -> unit -> Proof_global.closed_proof_output + val return_proof : unit -> Proof_global.closed_proof_output + val return_partial_proof : unit -> Proof_global.closed_proof_output type closed_proof = Proof_global.proof_object * Lemmas.Info.t -- cgit v1.2.3 From 0eadf776ba78dcfdcab842f38f5de871ed337376 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 26 Mar 2020 17:04:16 -0400 Subject: [proof] [stm] Force `opaque` in `close_future_proof` Following an observation by Enrico Tassi, we remove the `opaque` parameter from `close_future_proof`, it should never be called with transparent constants. We will enforce this thru typing at the proof layer soon. --- vernac/vernacstate.ml | 4 ++-- vernac/vernacstate.mli | 1 - 2 files changed, 2 insertions(+), 3 deletions(-) (limited to 'vernac') diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index b722acd1ad..a4e9c8e1ab 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -167,8 +167,8 @@ module Proof_global = struct let return_proof () = cc return_proof let return_partial_proof () = cc return_partial_proof - let close_future_proof ~opaque ~feedback_id pf = - cc_lemma (fun pt -> pf_fold (fun st -> close_future_proof ~opaque ~feedback_id st pf) pt, + let close_future_proof ~feedback_id pf = + cc_lemma (fun pt -> pf_fold (fun st -> close_future_proof ~feedback_id st pf) pt, Internal.get_info pt) let close_proof ~opaque ~keep_body_ucst_separate = diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli index b6b24c9275..9c4de7720c 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -71,7 +71,6 @@ module Proof_global : sig type closed_proof = Proof_global.proof_object * Lemmas.Info.t val close_future_proof : - opaque:Proof_global.opacity_flag -> feedback_id:Stateid.t -> Proof_global.closed_proof_output Future.computation -> closed_proof -- cgit v1.2.3