New v8.0 URIs.

[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 349825bf99b53a33c0bd399a83fb88a890a51489..7c0dfc1c6ab31c04a36d7f6ed8189d3cc09fbfa6 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -119,7 +119,28 @@ EXTEND
   ];
   term0: [ [ t = term; EOI -> return_term loc t ] ];
   term:
-    [ "binder" RIGHTA
+    [ "letin" NONA
+        (* actually "in" and "and" are _not_ keywords. Parsing works anyway
+         * since applications are required to be bound by parens *)
+      [ "let"; var = typed_name;
+        SYMBOL "="; (* SYMBOL <:unicode<def>> (* ≝ *); *)
+        t1 = term;
+        IDENT "in"; t2 = term ->
+          return_term loc (CicAst.LetIn (var, t1, t2))
+      | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
+          defs = LIST1 [
+            var = typed_name;
+            index = OPT [ PAREN "("; index = NUM; PAREN ")" ->
+              int_of_string index
+            ];
+            SYMBOL "="; (* SYMBOL <:unicode<def>> (* ≝ *); *)
+            t1 = term ->
+              (var, t1, (match index with None -> 0 | Some i -> i))
+          ] SEP (IDENT "and");
+          IDENT "in"; body = term ->
+            return_term loc (CicAst.LetRec (ind_kind, defs, body))
+      ]
+    | "binder" RIGHTA
       [
         b = binder;
         (vars, typ) =
@@ -141,7 +162,7 @@ EXTEND
             return_term loc
               (CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2))
       ]
-    | "eq" LEFTA
+    | "relop" LEFTA
       [ t1 = term; SYMBOL "="; t2 = term ->
         return_term loc (CicAst.Appl [CicAst.Symbol ("eq", 0); t1; t2])
       ]
@@ -167,27 +188,6 @@ EXTEND
                 fail loc ("Invalid meta variable number: " ^ m)
             in
             return_term loc (CicAst.Meta (index, substs))
-        (* actually "in" and "and" are _not_ keywords. Parsing works anyway
-         * since applications are required to be bound by parens *)
-      | "let"; var = typed_name;
-(*         SYMBOL <:unicode<def>> (* ≝ *); *)
-        SYMBOL "=";
-        t1 = term;
-        IDENT "in"; t2 = term ->
-          return_term loc (CicAst.LetIn (var, t1, t2))
-      | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
-          defs = LIST1 [
-            var = typed_name;
-            index = OPT [ PAREN "("; index = NUM; PAREN ")" ->
-              int_of_string index
-            ];
-(*             SYMBOL <:unicode<def>> (* ≝ *); *)
-            SYMBOL "=";
-            t1 = term ->
-              (var, t1, (match index with None -> 0 | Some i -> i))
-          ] SEP (IDENT "and");
-          IDENT "in"; body = term ->
-            return_term loc (CicAst.LetRec (ind_kind, defs, body))
       | outtyp = OPT [ PAREN "["; typ = term; PAREN "]" -> typ ];
         "match"; t = term;
         indty_ident = OPT [ SYMBOL ":"; id = IDENT -> id ];
@@ -204,11 +204,9 @@ EXTEND
       ]
     ];
   tactic_where: [
-    [ where = OPT [ "in"; ident = IDENT -> ident ] -> where ]
-  ];
-  tactic_term: [
-    [ t = term -> t ]
+    [ where = OPT [ IDENT "in"; ident = IDENT -> ident ] -> where ]
   ];
+  tactic_term: [ [ t = term -> t ] ];
   ident_list0: [
     [ PAREN "["; idents = LIST0 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ]
   ];
@@ -237,7 +235,7 @@ EXTEND
     | IDENT "elim"; IDENT "type"; t = tactic_term ->
         return_tactic loc (TacticAst.ElimType t)
     | IDENT "elim"; t1 = tactic_term;
-      using = OPT [ IDENT "using"; using = tactic_term -> using ] ->
+      using = OPT [ "using"; using = tactic_term -> using ] ->
         return_tactic loc (TacticAst.Elim (t1, using))
     | IDENT "exact"; t = tactic_term -> return_tactic loc (TacticAst.Exact t)
     | IDENT "exists" -> return_tactic loc TacticAst.Exists
@@ -269,26 +267,33 @@ EXTEND
     ]
   ];
   tactical0 : [ [ t = tactical; SYMBOL "." -> t ] ];
-  tactical: [
-    [ IDENT "fail" -> return_tactical loc TacticAst.Fail
-    | IDENT "do"; count = int; tac = tactical ->
-        return_tactical loc (TacticAst.Do (count, tac))
-    | IDENT "id" -> return_tactical loc TacticAst.IdTac
-    | IDENT "repeat"; tac = tactical ->
-        return_tactical loc (TacticAst.Repeat tac)
-    | tactics = LIST0 tactical SEP SYMBOL ";" ->
-        return_tactical loc (TacticAst.Seq tactics)
-    | tac = tactical;
-      PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" ->
-        return_tactical loc (TacticAst.Then (tac, tacs))
-    | IDENT "tries";
-      PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" ->
-        return_tactical loc (TacticAst.Tries tacs)
-    | IDENT "try"; tac = tactical -> return_tactical loc (TacticAst.Try tac)
-    | tac = tactic -> return_tactical loc (TacticAst.Tactic tac)
-    | PAREN "("; tac = tactical; PAREN ")" -> return_tactical loc tac
-    ]
-  ];
+  tactical:
+    [ "sequence" LEFTA
+      [ tactics = LIST1 NEXT SEP SYMBOL ";" ->
+          return_tactical loc (TacticAst.Seq tactics)
+      ]
+    | "then" NONA
+      [ tac = tactical;
+        PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" ->
+          return_tactical loc (TacticAst.Then (tac, tacs))
+      ]
+    | "loops" RIGHTA
+      [ IDENT "do"; count = int; tac = tactical ->
+          return_tactical loc (TacticAst.Do (count, tac))
+      | IDENT "repeat"; tac = tactical ->
+          return_tactical loc (TacticAst.Repeat tac)
+      ]
+    | "simple" NONA
+      [ IDENT "tries";
+        PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" ->
+          return_tactical loc (TacticAst.Tries tacs)
+      | IDENT "try"; tac = NEXT -> return_tactical loc (TacticAst.Try tac)
+      | IDENT "fail" -> return_tactical loc TacticAst.Fail
+      | IDENT "id" -> return_tactical loc TacticAst.IdTac
+      | PAREN "("; tac = tactical; PAREN ")" -> return_tactical loc tac
+      | tac = tactic -> return_tactical loc (TacticAst.Tactic tac)
+      ]
+    ];
 END
 
 let parse_term stream =