From 8abacf00c6c39ec98085d531737d18edc9c19b2a Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 2 May 2019 19:46:02 +0200 Subject: Proof_global: pass only 1 pstate when we don't want the proof stack Typically instead of [start_proof : ontop:Proof_global.t option -> bla -> Proof_global.t] we have [start_proof : bla -> Proof_global.pstate] and the pstate is pushed on the stack by a caller around the vernacentries/mlg level. Naming can be a bit awkward, hopefully it can be improved (maybe in a followup PR). We can see some patterns appear waiting for nicer combinators, eg in mlg we often only want to work with the current proof, not the stack. Behaviour should be similar modulo bugs, let's see what CI says. --- plugins/extraction/extract_env.ml | 4 ---- plugins/extraction/extract_env.mli | 2 +- plugins/extraction/g_extraction.mlg | 8 +++++++- 3 files changed, 8 insertions(+), 6 deletions(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 8f17f7b2dd..c5439ffaf6 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -751,10 +751,6 @@ let extract_and_compile l = (* Show the extraction of the current ongoing proof *) let show_extraction ~pstate = - let pstate = match pstate with - | None -> CErrors.user_err Pp.(str "No ongoing proof") - | Some pstate -> pstate - in init ~inner:true false false; let prf = Proof_global.give_me_the_proof pstate in let sigma, env = Pfedit.get_current_context pstate in diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index 7ba7e05019..efd5b5575f 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -40,4 +40,4 @@ val structure_for_compute : (* Show the extraction of the current ongoing proof *) -val show_extraction : pstate:Proof_global.t option -> unit +val show_extraction : pstate:Proof_global.pstate -> unit diff --git a/plugins/extraction/g_extraction.mlg b/plugins/extraction/g_extraction.mlg index db1a389fe7..d43d90af60 100644 --- a/plugins/extraction/g_extraction.mlg +++ b/plugins/extraction/g_extraction.mlg @@ -179,5 +179,11 @@ END VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY | ![ proof ] [ "Show" "Extraction" ] - -> { fun ~pstate -> let () = show_extraction ~pstate in pstate } + -> { fun ~pstate:ontop -> + let pstate = Option.map Proof_global.get_current_pstate ontop in + let pstate = match pstate with + | None -> CErrors.user_err Pp.(str "No ongoing proof") + | Some pstate -> pstate + in + let () = show_extraction ~pstate in ontop } END -- cgit v1.2.3 From b8842c3c8d6e6d9d4c19a75453fca9f94de6fa49 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 3 May 2019 14:14:40 +0200 Subject: coqpp: add new ![] specifiers for structured proof interaction ![proof_stack] is equivalent to the old meaning of ![proof]: the body has type `pstate:Proof_global.t option -> Proof_global.t option` The other specifiers are for the following body types: ~~~ ![open_proof] `is_ontop:bool -> pstate` ![maybe_open_proof] `is_ontop:bool -> pstate option` ![proof] `pstate:pstate -> pstate` ![proof_opt_query] `pstate:pstate option -> unit` ![proof_query] `pstate:pstate -> unit` ~~~ The `is_ontop` is only used for the warning message when declaring a section variable inside a proof, we could also just stop warning. The specifiers look closely related to stm classifiers, but currently they're unconnected. Notably this means that a ![proof_query] doesn't have to be classified QUERY. ![proof_stack] is only used by g_rewrite/rewrite whose behaviour I don't fully understand, maybe we can drop it in the future. For compat we may want to consider keeping ![proof] with its old meaning and using some new name for the new meaning. OTOH fixing plugins to be stricter is easier if we change it as the errors tell us where it's used. --- plugins/extraction/g_extraction.mlg | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/g_extraction.mlg b/plugins/extraction/g_extraction.mlg index d43d90af60..487accbc9b 100644 --- a/plugins/extraction/g_extraction.mlg +++ b/plugins/extraction/g_extraction.mlg @@ -178,12 +178,6 @@ END (* Show the extraction of the current proof *) VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY -| ![ proof ] [ "Show" "Extraction" ] - -> { fun ~pstate:ontop -> - let pstate = Option.map Proof_global.get_current_pstate ontop in - let pstate = match pstate with - | None -> CErrors.user_err Pp.(str "No ongoing proof") - | Some pstate -> pstate - in - let () = show_extraction ~pstate in ontop } +| ![ proof_query ] [ "Show" "Extraction" ] + -> { show_extraction } END -- cgit v1.2.3 From 02fda88fc065577f3f9604477db2e03eb4d5a9b4 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 7 May 2019 14:34:06 +0200 Subject: Alternate syntax for ![]: VERNAC EXTEND Foo STATE proof eg ![proof] becomes STATE proof This commits still supports the old ![] so there is redundancy: ~~~ VERNAC EXTEND Foo STATE proof | ... VERNAC EXTEND Foo | ![proof] ... ~~~ with the ![] form being local to the rule and the STATE form applying to the whole EXTEND except for the rules with a ![]. --- plugins/extraction/g_extraction.mlg | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/g_extraction.mlg b/plugins/extraction/g_extraction.mlg index 487accbc9b..9ea3fbeaf4 100644 --- a/plugins/extraction/g_extraction.mlg +++ b/plugins/extraction/g_extraction.mlg @@ -177,7 +177,7 @@ VERNAC COMMAND EXTEND ExtractionInductive CLASSIFIED AS SIDEFF END (* Show the extraction of the current proof *) -VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY -| ![ proof_query ] [ "Show" "Extraction" ] +VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY STATE proof_query +| [ "Show" "Extraction" ] -> { show_extraction } END -- cgit v1.2.3 From 99154fcb97653c606d2e62e0a0521c4afddff44c Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 20 May 2019 17:11:00 +0200 Subject: Rename Proof_global.{pstate -> t} --- plugins/extraction/extract_env.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index efd5b5575f..7d04fee7c1 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -40,4 +40,4 @@ val structure_for_compute : (* Show the extraction of the current ongoing proof *) -val show_extraction : pstate:Proof_global.pstate -> unit +val show_extraction : pstate:Proof_global.t -> unit -- cgit v1.2.3