- removed mandatory parens for application

- "in" and "and" are now keywords
- changed binder syntax, now more coqish
- alone symbols no longer permitted (e.g. "+" alone is no longer a term)

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index c64fcd42cb96faad16d4efb759b3fcb52324ffe1..a539fef6c238783365912191b037985ec8a75a3d 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -73,6 +73,10 @@ let name_of_string = function
   | "_" -> Cic.Anonymous
   | s -> Cic.Name s
 
+let int_opt = function
+  | None -> None
+  | Some lexeme -> Some (int_of_string lexeme)
+
 EXTEND
   GLOBAL: term term0 tactic tactical tactical0 command;
   int: [
@@ -108,7 +112,7 @@ EXTEND
     ]
   ];
   substituted_name: [ (* a subs.name is an explicit substitution subject *)
-    [ s = [ IDENT | SYMBOL ];
+    [ s = IDENT;
       subst = OPT [
         SYMBOL "\\subst";  (* to avoid catching frequent "a [1]" cases *)
         PAREN "[";
@@ -133,12 +137,9 @@ EXTEND
   term0: [ [ t = term; EOI -> return_term loc t ] ];
   term:
     [ "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 ->
+        t1 = term; "in"; t2 = term ->
           return_term loc (CicAst.LetIn (var, t1, t2))
       | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
           defs = LIST1 [
@@ -149,20 +150,20 @@ EXTEND
             SYMBOL "="; (* SYMBOL <:unicode<def>> (* ≝ *); *)
             t1 = term ->
               (var, t1, (match index with None -> 0 | Some i -> i))
-          ] SEP (IDENT "and");
-          IDENT "in"; body = term ->
+          ] SEP "and";
+          "in"; body = term ->
             return_term loc (CicAst.LetRec (ind_kind, defs, body))
       ]
     | "binder" RIGHTA
       [
         b = binder;
         (vars, typ) =
-          [ vars = LIST1 IDENT SEP SYMBOL ",";
+          [ vars = LIST1 IDENT;
             typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ)
-          | PAREN "("; vars = LIST1 IDENT SEP SYMBOL ",";
+          | PAREN "("; vars = LIST1 IDENT;
             typ = OPT [ SYMBOL ":"; t = term -> t ]; PAREN ")" -> (vars, typ)
           ];
-        SYMBOL "."; body = term ->
+        SYMBOL ","; body = term ->
           let binder =
             List.fold_right
               (fun var body ->
@@ -186,11 +187,17 @@ EXTEND
     | "mult" LEFTA    [ (* nothing here by default *) ]
     | "power" LEFTA   [ (* nothing here by default *) ]
     | "inv" NONA      [ (* nothing here by default *) ]
+    | "apply" LEFTA
+      [ t1 = term; t2 = term ->
+        let rec aux = function
+          | CicAst.Appl (hd :: tl) -> aux hd @ tl
+          | term -> [term]
+        in
+        CicAst.Appl (aux t1 @ [t2])
+      ]
     | "simple" NONA
       [ 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))
       | i = NUM -> return_term loc (CicAst.Num (i, (fresh_num_instance ())))
       | IMPLICIT -> return_term loc CicAst.Implicit
       | m = META;
@@ -223,7 +230,7 @@ EXTEND
       ]
     ];
   tactic_where: [
-    [ where = OPT [ IDENT "in"; ident = IDENT -> ident ] -> where ]
+    [ where = OPT [ "in"; ident = IDENT -> ident ] -> where ]
   ];
   tactic_term: [ [ t = term -> t ] ];
   ident_list0: [
@@ -281,9 +288,11 @@ EXTEND
       idents = OPT ident_list0 ->
         let idents = match idents with None -> [] | Some idents -> idents in
         return_tactic loc (TacticAst.Intros (num, idents))
+    | [ IDENT "intro" | IDENT "Intro" ] ->
+        return_tactic loc (TacticAst.Intros (Some 1, []))
     | [ IDENT "left" | IDENT "Left" ] -> return_tactic loc TacticAst.Left
     | [ "let" | "Let" ];
-      t = tactic_term; IDENT "in"; where = IDENT ->
+      t = tactic_term; "in"; where = IDENT ->
         return_tactic loc (TacticAst.LetIn (t, where))
     (* TODO Reduce *)
     | [ IDENT "reflexivity" | IDENT "Reflexivity" ] ->
@@ -356,6 +365,10 @@ EXTEND
     | [ IDENT "goal" | IDENT "Goal" ]; typ = term;
       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
         return_command loc (TacticAst.Theorem (`Goal, None, typ, body))
+    | [ IDENT "undo"   | IDENT "Undo" ]; steps = OPT NUM ->
+        return_command loc (TacticAst.Undo (int_opt steps))
+    | [ IDENT "redo"   | IDENT "Redo" ]; steps = OPT NUM ->
+        return_command loc (TacticAst.Redo (int_opt steps))
     ]
   ];
 END