From a8c6c554a0fa282a1e66203bc0c7f76a41054166 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Fri, 25 Oct 2019 14:45:50 +0200 Subject: Possible simplification of parsing rules. Noticed by Jim while working on automatic grammar documentation. --- parsing/g_constr.mlg | 16 ++++------------ 1 file changed, 4 insertions(+), 12 deletions(-) diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index ea44e748c9..87b9a8eea3 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -196,17 +196,11 @@ GRAMMAR EXTEND Gram [ "200" RIGHTA [ c = binder_constr -> { c } ] | "100" RIGHTA - [ c1 = operconstr; "<:"; c2 = binder_constr -> + [ c1 = operconstr; "<:"; c2 = operconstr LEVEL "200" -> { CAst.make ~loc @@ CCast(c1, CastVM c2) } - | c1 = operconstr; "<:"; c2 = SELF -> - { CAst.make ~loc @@ CCast(c1, CastVM c2) } - | c1 = operconstr; "<<:"; c2 = binder_constr -> - { CAst.make ~loc @@ CCast(c1, CastNative c2) } - | c1 = operconstr; "<<:"; c2 = SELF -> + | c1 = operconstr; "<<:"; c2 = operconstr LEVEL "200" -> { CAst.make ~loc @@ CCast(c1, CastNative c2) } - | c1 = operconstr; ":";c2 = binder_constr -> - { CAst.make ~loc @@ CCast(c1, CastConv c2) } - | c1 = operconstr; ":"; c2 = SELF -> + | c1 = operconstr; ":"; c2 = operconstr LEVEL "200" -> { CAst.make ~loc @@ CCast(c1, CastConv c2) } | c1 = operconstr; ":>" -> { CAst.make ~loc @@ CCast(c1, CastCoerce) } ] @@ -407,9 +401,7 @@ GRAMMAR EXTEND Gram pattern: [ "200" RIGHTA [ ] | "100" RIGHTA - [ p = pattern; ":"; ty = binder_constr -> - {CAst.make ~loc @@ CPatCast (p, ty) } - | p = pattern; ":"; ty = operconstr LEVEL "100" -> + [ p = pattern; ":"; ty = operconstr LEVEL "200" -> {CAst.make ~loc @@ CPatCast (p, ty) } ] | "99" RIGHTA [ ] | "90" RIGHTA [ ] -- cgit v1.2.3 From 342db66cc94a6010a6f301071d251aa458e21547 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 28 Oct 2019 10:47:42 +0100 Subject: Add changelog for #10963. --- doc/changelog/03-notations/10963-simplify-parser.rst | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 doc/changelog/03-notations/10963-simplify-parser.rst diff --git a/doc/changelog/03-notations/10963-simplify-parser.rst b/doc/changelog/03-notations/10963-simplify-parser.rst new file mode 100644 index 0000000000..8b501aac82 --- /dev/null +++ b/doc/changelog/03-notations/10963-simplify-parser.rst @@ -0,0 +1,6 @@ +- A simplification of parsing rules could cause a slight change of + parsing precedences for the very rare users who defined notations + with `constr` at level stritcly between 100 and 200 and use these + notations on the right-hand side of a cast operator (`:`, `:>`, + `:>>`) (`#10963 `_, by Théo + Zimmermann, simplification initially noticed by Jim Fehrle). -- cgit v1.2.3 From 74c6d69a08b50b77c001ca758d25f1a969bf2c73 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 28 Oct 2019 16:44:45 +0100 Subject: Fix typos. Co-Authored-By: Clément Pit-Claudel --- doc/changelog/03-notations/10963-simplify-parser.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/changelog/03-notations/10963-simplify-parser.rst b/doc/changelog/03-notations/10963-simplify-parser.rst index 8b501aac82..327a39bdb6 100644 --- a/doc/changelog/03-notations/10963-simplify-parser.rst +++ b/doc/changelog/03-notations/10963-simplify-parser.rst @@ -1,6 +1,6 @@ - A simplification of parsing rules could cause a slight change of parsing precedences for the very rare users who defined notations - with `constr` at level stritcly between 100 and 200 and use these + with `constr` at level strictly between 100 and 200 and used these notations on the right-hand side of a cast operator (`:`, `:>`, `:>>`) (`#10963 `_, by Théo Zimmermann, simplification initially noticed by Jim Fehrle). -- cgit v1.2.3