\lambda x.x y ----> \lambda x.(x y)

[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 34b3d01e0cc18a72dde5f36c0953930b46989681..add74d03e856cde6162bf7064d66f3ec6da489c9 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -250,6 +250,9 @@ EXTEND
         b = binder_low; (vars, typ) = binder_vars; SYMBOL "."; body = term ->
           let binder = mk_binder_ast b typ vars body in
           return_term loc binder
+      | b = binder_high; (vars, typ) = binder_vars; SYMBOL "."; body = term ->
+          let binder = mk_binder_ast b typ 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))
       ]
@@ -272,12 +275,6 @@ EXTEND
         in
         CicAst.Appl (aux t1 @ [t2])
       ]
-    | "binder" RIGHTA
-      [
-        b = binder_high; (vars, typ) = binder_vars; SYMBOL "."; body = term ->
-          let binder = mk_binder_ast b typ vars body in
-          return_term loc binder
-      ]
     | "simple" NONA
       [ sort = sort -> CicAst.Sort sort
       | n = substituted_name -> return_term loc n
@@ -391,14 +388,17 @@ EXTEND
         (match (pat, terms) with
         | None, [] -> TacticAst.Reduce (loc, kind, None)
         | None, terms -> TacticAst.Reduce (loc, kind, Some (terms, `Goal))
-        | Some pat, [] -> TacticAst.Reduce (loc, kind, Some ([], pat))
+        | Some pat, [] -> fail loc "Missing term [list]"
         | Some pat, terms -> TacticAst.Reduce (loc, kind, Some (terms, pat)))
     | [ IDENT "reflexivity" ] ->
         TacticAst.Reflexivity loc
     | [ IDENT "replace" ];
       t1 = tactic_term; "with"; t2 = tactic_term ->
         TacticAst.Replace (loc, t1, t2)
-    (* TODO Rewrite *)
+    | [ IDENT "rewrite" ; IDENT "left" ] ; t = term ->
+        TacticAst.Rewrite (loc,`Left, t, None)
+    | [ IDENT "rewrite" ; IDENT "right" ] ; t = term ->
+        TacticAst.Rewrite (loc,`Right, t, None)
     (* TODO Replace_pattern *)
     | [ IDENT "right" ] -> TacticAst.Right loc
     | [ IDENT "ring" ] -> TacticAst.Ring loc
@@ -481,7 +481,16 @@ EXTEND
     | [ IDENT "check"   ]; t = term ->
         TacticAst.Check (loc, t)
     | [ IDENT "hint" ] -> TacticAst.Hint loc
-    | [ IDENT "pmatch" ] ; t = term -> TacticAst.Match (loc,t)
+    | [ IDENT "whelp"; "match" ] ; t = term -> 
+        TacticAst.WMatch (loc,t)
+    | [ IDENT "whelp"; IDENT "instance" ] ; t = term -> 
+        TacticAst.WInstance (loc,t)
+    | [ IDENT "whelp"; IDENT "locate" ] ; id = IDENT -> 
+        TacticAst.WLocate (loc,id)
+    | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
+        TacticAst.WElim (loc, t)
+    | [ IDENT "whelp"; IDENT "hint" ] ; t = term -> 
+        TacticAst.WHint (loc,t)
     | [ IDENT "print" ]; name = QSTRING -> TacticAst.Print (loc, name)
   ]];
 
@@ -559,12 +568,26 @@ EXTEND
         TacticAst.Alias (loc, spec)
   ]];
 
-  statement: [
+  executable: [
     [ cmd = command; SYMBOL "." -> TacticAst.Command (loc, cmd)
     | tac = tactical; SYMBOL "." -> TacticAst.Tactical (loc, tac)
     | mac = macro; SYMBOL "." -> TacticAst.Macro (loc, mac)
     ]
   ];
+  
+  comment: [
+    [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT -> 
+       TacticAst.Code (loc, ex)
+    | str = NOTE -> 
+       TacticAst.Note (loc, str)
+    ]
+  ];
+  
+  statement: [
+    [ ex = executable -> TacticAst.Executable (loc,ex)
+    | com = comment -> TacticAst.Comment (loc, com)
+    ]
+  ];
 END
 
 let exc_located_wrapper f =