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. --- doc/plugin_tutorial/tuto1/src/g_tuto1.mlg | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'doc') diff --git a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg index 75251d8e33..147b0df567 100644 --- a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg +++ b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg @@ -146,11 +146,12 @@ END VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY | ![ proof ] [ "Cmd9" ] -> - { fun ~pstate -> - Option.iter (fun (pstate : Proof_global.t) -> + { fun ~pstate:ontop -> + Option.iter (fun ontop -> + let pstate = Proof_global.get_current_pstate ontop in let sigma, env = Pfedit.get_current_context pstate in let pprf = Proof.partial_proof Proof_global.(give_me_the_proof pstate) in Feedback.msg_notice - (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf)) pstate; - pstate } + (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf)) ontop; + 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. --- doc/plugin_tutorial/tuto1/src/g_tuto1.mlg | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) (limited to 'doc') diff --git a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg index 147b0df567..300d62285a 100644 --- a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg +++ b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg @@ -145,13 +145,11 @@ END it gives an error message that is basically impossible to understand. *) VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY -| ![ proof ] [ "Cmd9" ] -> - { fun ~pstate:ontop -> - Option.iter (fun ontop -> - let pstate = Proof_global.get_current_pstate ontop in - let sigma, env = Pfedit.get_current_context pstate in - let pprf = Proof.partial_proof Proof_global.(give_me_the_proof pstate) in - Feedback.msg_notice - (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf)) ontop; - ontop } +| ![ proof_query ] [ "Cmd9" ] -> + { fun ~pstate -> + let sigma, env = Pfedit.get_current_context pstate in + let pprf = Proof.partial_proof Proof_global.(give_me_the_proof pstate) in + Feedback.msg_notice + (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf) + } END -- cgit v1.2.3 From 0f1814bcbaafbd93d7c7587eef8826a80b65477f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 22 May 2019 17:52:19 +0200 Subject: [function] always open a proof when used with `wf` or `measure` --- .../02-specification-language/10215-rm-maybe-open-proof.rst | 5 +++++ doc/sphinx/language/gallina-extensions.rst | 2 +- 2 files changed, 6 insertions(+), 1 deletion(-) create mode 100644 doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst (limited to 'doc') diff --git a/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst b/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst new file mode 100644 index 0000000000..53828db951 --- /dev/null +++ b/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst @@ -0,0 +1,5 @@ +- Function always opens a proof when used with a ``measure`` or ``wf`` + annotation, see Description of the changes, with possible link to + :ref:`advanced-recursive-functions` of the updated documentation + (`#10215 `_, + by Enrico Tassi). diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 8c5ad785e4..c93984661e 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -737,7 +737,7 @@ used by ``Function``. A more precise description is given below. decreases at each recursive call of :token:`term`. The order must be well-founded. Parameters of the function are bound in :token:`term`. - Depending on the annotation, the user is left with some proof + If the annotation is ``measure`` or ``fw``, the user is left with some proof obligations that will be used to define the function. These proofs are: proofs that each recursive call is actually decreasing with respect to the given criteria, and (if the criteria is `wf`) a proof -- cgit v1.2.3 From 2ebd73901edb94030aa804572cbe86d486ca6732 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 22 May 2019 17:50:44 +0200 Subject: [rewrite] Add Morphism syntax made different for module type parameters --- .../02-specification-language/10215-rm-maybe-open-proof.rst | 7 +++++++ doc/sphinx/addendum/generalized-rewriting.rst | 7 +++++++ 2 files changed, 14 insertions(+) (limited to 'doc') diff --git a/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst b/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst index 53828db951..12d458a72c 100644 --- a/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst +++ b/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst @@ -3,3 +3,10 @@ :ref:`advanced-recursive-functions` of the updated documentation (`#10215 `_, by Enrico Tassi). + +- The legacy command Add Morphism always opens a proof and cannot be used + inside a module type. In order to declare a module type parameter that + happens to be a morphism, use ``Parameter Morphism``. See + :ref:`deprecated_syntax_for_generalized_rewriting` for the updated + documentation (`#10215 `_, + by Enrico Tassi). diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index e58049b8d0..2ea0861e47 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -563,6 +563,7 @@ Printing relations and morphisms of morphisms, the :cmd:`Print Instances` command can be useful to understand what additional morphisms should be registered. +.. _deprecated_syntax_for_generalized_rewriting: Deprecated syntax and backward incompatibilities ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -589,6 +590,12 @@ Deprecated syntax and backward incompatibilities bi-implication in place of a simple implication. In practice, porting an old development to the new semantics is usually quite simple. +.. cmd:: Declare Morphism @ident : @ident + :name: Declare Morphism + + This commands is to be used in a module type to declare a parameter that + is a morphism. + Notice that several limitations of the old implementation have been lifted. In particular, it is now possible to declare several relations with the same carrier and several signatures for the same morphism. -- cgit v1.2.3 From 4131b14ac8ea93b54583c0c6fc0dff310a9c5172 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 28 May 2019 22:20:03 +0200 Subject: Fix typo in changelog --- .../02-specification-language/10215-rm-maybe-open-proof.rst | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'doc') diff --git a/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst b/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst index 12d458a72c..21ec7f8e5b 100644 --- a/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst +++ b/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst @@ -1,7 +1,6 @@ - Function always opens a proof when used with a ``measure`` or ``wf`` - annotation, see Description of the changes, with possible link to - :ref:`advanced-recursive-functions` of the updated documentation - (`#10215 `_, + annotation, see :ref:`advanced-recursive-functions` for the updated + documentation (`#10215 `_, by Enrico Tassi). - The legacy command Add Morphism always opens a proof and cannot be used -- cgit v1.2.3