solved a precedence issue between binders and arrows

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 0ac43a11e4d0771a6182e22579ac0ab6e2772043..793d95e025fe89cdf8fcae17c8b65e30596576ec 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -64,10 +64,15 @@ EXTEND
   ];
   binder: [
     [ SYMBOL <:unicode<lambda>> (* λ *) -> `Lambda
-    | SYMBOL <:unicode<pi>> (* π *) -> `Pi
+    | SYMBOL <:unicode<Pi>>     (* Π *) -> `Pi
     | SYMBOL <:unicode<exists>> (* ∃ *) -> `Exists
-    | SYMBOL <:unicode<forall>> (* ∀ *) -> `Forall
-    ]
+    | SYMBOL <:unicode<forall>> (* ∀ *) -> `Forall ]
+  ];
+  sort: [
+    [ "Prop" -> `Prop
+    | "Set" -> `Set
+    | "Type" -> `Type
+    | "CProp" -> `CProp ]
   ];
   typed_name: [
     [ PAREN "("; i = IDENT; SYMBOL ":"; typ = term; PAREN ")" ->
@@ -100,14 +105,9 @@ EXTEND
         (head, vars)
     ]
   ];
-  term0: [ [ t = term -> return_term loc t ] ];
+  term0: [ [ t = term; EOI -> return_term loc t ] ];
   term:
-    [ "arrow" RIGHTA
-      [ t1 = term; SYMBOL <:unicode<to>>; t2 = term ->
-          return_term loc
-            (CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2))
-      ]
-    | "binder" RIGHTA
+    [ "binder" RIGHTA
       [
         b = binder;
         (vars, typ) =
@@ -125,6 +125,9 @@ EXTEND
               vars body
           in
           return_term loc binder
+      | t1 = term; SYMBOL <:unicode<to>> (* → *); t2 = term ->
+            return_term loc
+              (CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2))
       ]
     | "eq" LEFTA
       [ t1 = term; SYMBOL "="; t2 = term ->
@@ -134,11 +137,7 @@ EXTEND
     | "mult" LEFTA    [ (* nothing here by default *) ]
     | "inv" NONA      [ (* nothing here by default *) ]
     | "simple" NONA
-      [
-        sort_kind = [
-          "Prop" -> `Prop | "Set" -> `Set | "Type" -> `Type | "CProp" -> `CProp
-        ] ->
-          CicAst.Sort sort_kind
+      [ sort = sort -> CicAst.Sort sort
       | n = substituted_name -> return_term loc n
       | PAREN "("; head = term; args = LIST1 term; PAREN ")" ->
           return_term loc (CicAst.Appl (head :: args))

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli
index aec7c8f1d7580a7f62fada503f06d7b88bf39251..7e0625cc361567c3c7bf7f9d0226b749bc776702 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli
@@ -31,8 +31,8 @@ val parse_term: char Stream.t -> CicAst.term
 
 (** {2 Grammar extensions} *)
 
-val term: CicAst.term Grammar.Entry.e (** recursive rule *)
-val term0: CicAst.term Grammar.Entry.e (** top level rule *)
+val term: CicAst.term Grammar.Entry.e   (** recursive rule *)
+val term0: CicAst.term Grammar.Entry.e  (** top level rule *)
 
 val return_term: CicAst.location -> CicAst.term -> CicAst.term