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/derive/derive.ml | 4 ++-- plugins/derive/derive.mli | 2 +- plugins/derive/g_derive.mlg | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) (limited to 'plugins/derive') diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 4769c2dc53..9c1882dc9a 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -101,8 +101,8 @@ let start_deriving f suchthat lemma = in let terminator = Proof_global.make_terminator terminator in - let pstate = Proof_global.start_dependent_proof ~ontop:None lemma kind goals terminator in - Proof_global.simple_with_current_proof begin fun _ p -> + let pstate = Proof_global.start_dependent_proof lemma kind goals terminator in + Proof_global.modify_proof begin fun p -> let p,_,() = Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p in p end pstate diff --git a/plugins/derive/derive.mli b/plugins/derive/derive.mli index 6bb923118e..6e4bffa0b6 100644 --- a/plugins/derive/derive.mli +++ b/plugins/derive/derive.mli @@ -12,4 +12,4 @@ (which can contain references to [f]) in the context extended by [f:=?x]. When the proof ends, [f] is defined as the value of [?x] and [lemma] as the proof. *) -val start_deriving : Names.Id.t -> Constrexpr.constr_expr -> Names.Id.t -> Proof_global.t +val start_deriving : Names.Id.t -> Constrexpr.constr_expr -> Names.Id.t -> Proof_global.pstate diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg index 214a9d8bb5..ee076f5ae3 100644 --- a/plugins/derive/g_derive.mlg +++ b/plugins/derive/g_derive.mlg @@ -24,5 +24,5 @@ let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpac VERNAC COMMAND EXTEND Derive CLASSIFIED BY { classify_derive_command } | ![ proof ] [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] -> - { fun ~pstate -> Some Derive.(start_deriving f suchthat lemma) } + { fun ~pstate -> Some (Proof_global.push ~ontop:pstate Derive.(start_deriving f suchthat lemma)) } 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/derive/g_derive.mlg | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/derive') diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg index ee076f5ae3..d25b8fd01c 100644 --- a/plugins/derive/g_derive.mlg +++ b/plugins/derive/g_derive.mlg @@ -23,6 +23,6 @@ let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpac } VERNAC COMMAND EXTEND Derive CLASSIFIED BY { classify_derive_command } -| ![ proof ] [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] -> - { fun ~pstate -> Some (Proof_global.push ~ontop:pstate Derive.(start_deriving f suchthat lemma)) } +| ![ open_proof ] [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] -> + { Derive.(start_deriving f suchthat lemma) } 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/derive/g_derive.mlg | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/derive') diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg index d25b8fd01c..526989fdf3 100644 --- a/plugins/derive/g_derive.mlg +++ b/plugins/derive/g_derive.mlg @@ -22,7 +22,7 @@ let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpac } -VERNAC COMMAND EXTEND Derive CLASSIFIED BY { classify_derive_command } -| ![ open_proof ] [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] -> +VERNAC COMMAND EXTEND Derive CLASSIFIED BY { classify_derive_command } STATE open_proof +| [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] -> { Derive.(start_deriving f suchthat lemma) } 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/derive/derive.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/derive') diff --git a/plugins/derive/derive.mli b/plugins/derive/derive.mli index 6e4bffa0b6..6bb923118e 100644 --- a/plugins/derive/derive.mli +++ b/plugins/derive/derive.mli @@ -12,4 +12,4 @@ (which can contain references to [f]) in the context extended by [f:=?x]. When the proof ends, [f] is defined as the value of [?x] and [lemma] as the proof. *) -val start_deriving : Names.Id.t -> Constrexpr.constr_expr -> Names.Id.t -> Proof_global.pstate +val start_deriving : Names.Id.t -> Constrexpr.constr_expr -> Names.Id.t -> Proof_global.t -- cgit v1.2.3