- Configuration file moved to /projects/helm/etc.

[helm.git] / helm / ocaml / cic_disambiguation / cicTextualParser2.ml

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 397d038678839f00941803ffa830c7c6af27d645..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,17 +105,17 @@ 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 = LIST1 IDENT SEP SYMBOL ",";
-        typ = OPT [ SYMBOL ":"; t = term -> t ];
+        b = binder;
+        (vars, typ) =
+          [ vars = LIST1 IDENT SEP SYMBOL ",";
+            typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ)
+          | PAREN "("; vars = LIST1 IDENT SEP SYMBOL ",";
+            typ = OPT [ SYMBOL ":"; t = term -> t ]; PAREN ")" -> (vars, typ)
+          ];
         SYMBOL "."; body = term ->
           let binder =
             List.fold_right
@@ -120,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 ->
@@ -129,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))
@@ -174,7 +178,7 @@ EXTEND
             return_term loc (CicAst.LetRec (ind_kind, defs, body))
       | outtyp = OPT [ PAREN "["; typ = term; PAREN "]" -> typ ];
         "match"; t = term;
-        SYMBOL ":"; indty = IDENT;
+        indty_ident = OPT [ SYMBOL ":"; id = IDENT -> id ];
         "with";
         PAREN "[";
         patterns = LIST0 [
@@ -183,7 +187,7 @@ EXTEND
         ] SEP SYMBOL "|";
         PAREN "]" ->
           return_term loc
-            (CicAst.Case (t, indty, outtyp, patterns))
+            (CicAst.Case (t, indty_ident, outtyp, patterns))
       | PAREN "("; t = term; PAREN ")" -> return_term loc t
       ]
     ];