From 454816235038540977826f1ab7ba96005639f5e1 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 29 Jan 2019 15:44:33 +0100 Subject: Fix #9432: canonical structure and coercion accept universe binders. (when defining a new constant) --- test-suite/bugs/closed/bug_9432.v | 10 ++++++++++ vernac/g_vernac.mlg | 8 ++++---- 2 files changed, 14 insertions(+), 4 deletions(-) create mode 100644 test-suite/bugs/closed/bug_9432.v diff --git a/test-suite/bugs/closed/bug_9432.v b/test-suite/bugs/closed/bug_9432.v new file mode 100644 index 0000000000..c074f1cfc1 --- /dev/null +++ b/test-suite/bugs/closed/bug_9432.v @@ -0,0 +1,10 @@ + +Record foo := { f : Type }. + +Fail Canonical Structure xx@{} := {| f := Type |}. + +Canonical Structure xx@{i} := {| f := Type@{i} |}. + +Fail Coercion cc@{} := fun x : Type => Build_foo x. + +Coercion cc@{i} := fun x : Type@{i} => Build_foo x. diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 0664e18130..e7d81b8bb0 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -697,14 +697,14 @@ GRAMMAR EXTEND Gram { VernacCanonical CAst.(make ~loc @@ AN qid) } | IDENT "Canonical"; IDENT "Structure"; ntn = by_notation -> { VernacCanonical CAst.(make ~loc @@ ByNotation ntn) } - | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body -> + | IDENT "Canonical"; IDENT "Structure"; qid = global; u = OPT univ_decl; d = def_body -> { let s = coerce_reference_to_id qid in - VernacDefinition ((NoDischarge,CanonicalStructure),((CAst.make (Name s)),None),d) } + VernacDefinition ((NoDischarge,CanonicalStructure),((CAst.make (Name s)),u),d) } (* Coercions *) - | IDENT "Coercion"; qid = global; d = def_body -> + | IDENT "Coercion"; qid = global; u = OPT univ_decl; d = def_body -> { let s = coerce_reference_to_id qid in - VernacDefinition ((NoDischarge,Coercion),((CAst.make (Name s)),None),d) } + VernacDefinition ((NoDischarge,Coercion),((CAst.make (Name s)),u),d) } | IDENT "Identity"; IDENT "Coercion"; f = identref; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> { VernacIdentityCoercion (f, s, t) } -- cgit v1.2.3 From 8549847fc7df04a4896dc2ff4b29eb54a867b4b2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 31 Jan 2019 13:44:38 +0100 Subject: refactor grammar --- vernac/g_vernac.mlg | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index e7d81b8bb0..c36a6fa9c6 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -693,13 +693,15 @@ GRAMMAR EXTEND Gram LIST1 [ v=strategy_level; "["; q=LIST1 smart_global; "]" -> { (v,q) } ] -> { VernacSetStrategy l } (* Canonical structure *) - | IDENT "Canonical"; IDENT "Structure"; qid = global -> - { VernacCanonical CAst.(make ~loc @@ AN qid) } + | IDENT "Canonical"; IDENT "Structure"; qid = global; ud = OPT [ u = OPT univ_decl; d = def_body -> { (u,d) } ] -> + { match ud with + | None -> + VernacCanonical CAst.(make ~loc @@ AN qid) + | Some (u,d) -> + let s = coerce_reference_to_id qid in + VernacDefinition ((NoDischarge,CanonicalStructure),((CAst.make (Name s)),u),d) } | IDENT "Canonical"; IDENT "Structure"; ntn = by_notation -> { VernacCanonical CAst.(make ~loc @@ ByNotation ntn) } - | IDENT "Canonical"; IDENT "Structure"; qid = global; u = OPT univ_decl; d = def_body -> - { let s = coerce_reference_to_id qid in - VernacDefinition ((NoDischarge,CanonicalStructure),((CAst.make (Name s)),u),d) } (* Coercions *) | IDENT "Coercion"; qid = global; u = OPT univ_decl; d = def_body -> -- cgit v1.2.3 From 1123165d3186124bd0b72b382d39383aefe347d8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 13 Feb 2019 13:48:05 +0100 Subject: more tests --- test-suite/bugs/closed/bug_9432.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/test-suite/bugs/closed/bug_9432.v b/test-suite/bugs/closed/bug_9432.v index c074f1cfc1..c85f8129ce 100644 --- a/test-suite/bugs/closed/bug_9432.v +++ b/test-suite/bugs/closed/bug_9432.v @@ -7,4 +7,6 @@ Canonical Structure xx@{i} := {| f := Type@{i} |}. Fail Coercion cc@{} := fun x : Type => Build_foo x. -Coercion cc@{i} := fun x : Type@{i} => Build_foo x. +Polymorphic Coercion cc@{i} := fun x : Type@{i} => Build_foo x. + +Coercion cc1@{i} := (cc@{i}). -- cgit v1.2.3 From 737ae4816a9c84369bc1c0a0b359a9fd4f63dbe6 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 13 Feb 2019 13:53:34 +0100 Subject: [ssr] move shorter Canonical to Coq proper --- doc/sphinx/language/gallina-extensions.rst | 12 ++++++------ plugins/ssr/ssrvernac.mlg | 20 -------------------- vernac/g_vernac.mlg | 4 ++-- 3 files changed, 8 insertions(+), 28 deletions(-) diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 50a56f1d51..ca2d31d7ed 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1924,9 +1924,10 @@ applied to an unknown structure instance (an implicit argument) and a value. The complete documentation of canonical structures can be found in :ref:`canonicalstructures`; here only a simple example is given. -.. cmd:: Canonical Structure @qualid +.. cmd:: Canonical {? Structure } @qualid - This command declares :token:`qualid` as a canonical structure. + This command declares :token:`qualid` as a canonical instance of a + structure (a record). Assume that :token:`qualid` denotes an object ``(Build_struct`` |c_1| … |c_n| ``)`` in the structure :g:`struct` of which the fields are |x_1|, …, |x_n|. @@ -1961,7 +1962,7 @@ in :ref:`canonicalstructures`; here only a simple example is given. Definition nat_setoid : Setoid := Build_Setoid eq_nat_equiv. - Canonical Structure nat_setoid. + Canonical nat_setoid. Thanks to :g:`nat_setoid` declared as canonical, the implicit arguments :g:`A` and :g:`B` can be synthesized in the next statement. @@ -1974,11 +1975,10 @@ in :ref:`canonicalstructures`; here only a simple example is given. If a same field occurs in several canonical structures, then only the structure declared first as canonical is considered. - .. cmdv:: Canonical Structure @ident {? : @type } := @term + .. cmdv:: Canonical {? Structure } @ident {? : @type } := @term This is equivalent to a regular definition of :token:`ident` followed by the - declaration :n:`Canonical Structure @ident`. - + declaration :n:`Canonical @ident`. .. cmd:: Print Canonical Projections diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 191a4e9a20..d083d34b52 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -596,26 +596,6 @@ VERNAC COMMAND EXTEND HintView CLASSIFIED AS SIDEFF Ssrview.AdaptorDb.declare k hints } END -(** Canonical Structure alias *) - -GRAMMAR EXTEND Gram - GLOBAL: gallina_ext; - - gallina_ext: - (* Canonical structure *) - [[ IDENT "Canonical"; qid = Constr.global -> - { Vernacexpr.VernacCanonical (CAst.make @@ AN qid) } - | IDENT "Canonical"; ntn = Prim.by_notation -> - { Vernacexpr.VernacCanonical (CAst.make @@ ByNotation ntn) } - | IDENT "Canonical"; qid = Constr.global; - d = G_vernac.def_body -> - { let s = coerce_reference_to_id qid in - Vernacexpr.VernacDefinition - ((Decl_kinds.NoDischarge,Decl_kinds.CanonicalStructure), - ((CAst.make (Name s)),None), d) } - ]]; -END - (** Keyword compatibility fixes. *) (* Coq v8.1 notation uses "by" and "of" quasi-keywords, i.e., reserved *) diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index c36a6fa9c6..42bee25da3 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -693,14 +693,14 @@ GRAMMAR EXTEND Gram LIST1 [ v=strategy_level; "["; q=LIST1 smart_global; "]" -> { (v,q) } ] -> { VernacSetStrategy l } (* Canonical structure *) - | IDENT "Canonical"; IDENT "Structure"; qid = global; ud = OPT [ u = OPT univ_decl; d = def_body -> { (u,d) } ] -> + | IDENT "Canonical"; OPT [ IDENT "Structure" -> {()} ]; qid = global; ud = OPT [ u = OPT univ_decl; d = def_body -> { (u,d) } ] -> { match ud with | None -> VernacCanonical CAst.(make ~loc @@ AN qid) | Some (u,d) -> let s = coerce_reference_to_id qid in VernacDefinition ((NoDischarge,CanonicalStructure),((CAst.make (Name s)),u),d) } - | IDENT "Canonical"; IDENT "Structure"; ntn = by_notation -> + | IDENT "Canonical"; OPT [ IDENT "Structure" -> {()} ]; ntn = by_notation -> { VernacCanonical CAst.(make ~loc @@ ByNotation ntn) } (* Coercions *) -- cgit v1.2.3