- bugfix in term grammar: lowered precedence level of "let ... in" so

  that "let x = 1 in x + 2" works as expected
- decent grammar for tactics and tacticals: now with precedence levels
  (no more stackoverflows, hopefully)

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 349825bf99b53a33c0bd399a83fb88a890a51489..cd1de44879c723caadc256fd30cbdc8fc72f4e9d 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) =
@@ -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 ];
@@ -203,12 +203,8 @@ EXTEND
       | PAREN "("; t = term; PAREN ")" -> return_term loc t
       ]
     ];
-  tactic_where: [
-    [ where = OPT [ "in"; ident = IDENT -> ident ] -> where ]
-  ];
-  tactic_term: [
-    [ t = term -> t ]
-  ];
+  tactic_where: [ [ where = OPT [ "in"; ident = IDENT -> ident ] -> where ] ];
+  tactic_term: [ [ t = term -> t ] ];
   ident_list0: [
     [ PAREN "["; idents = LIST0 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ]
   ];
@@ -269,26 +265,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 =