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(-)

(limited to 'parsing')

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