From 797b256a0e91614b8ef8e0061fa0d624189a93db Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 4 Oct 2004 09:39:20 +0000
Subject: [PATCH] - 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)

---
 .../cic_disambiguation/cicTextualParser2.ml   | 41 ++++++++++++-------
 1 file changed, 27 insertions(+), 14 deletions(-)

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index c64fcd42c..a539fef6c 100644
--- 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
-- 
2.39.2