lapply and fwd improved

[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 9f6476d281981b3a2970f7e7fe1b417da49aa742..728ff94a085157d37933e1d14e782f108c2866d6 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -318,6 +318,9 @@ EXTEND
   ident_list0: [
     [ PAREN "["; idents = LIST0 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ]
   ];
+  tactic_term_list1: [
+    [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
+  ];
   reduction_kind: [
     [ [ IDENT "reduce" ] -> `Reduce
     | [ IDENT "simplify" ] -> `Simpl
@@ -363,7 +366,7 @@ EXTEND
         TacticAst.Assumption loc
     | IDENT "auto";
       depth = OPT [ IDENT "depth"; SYMBOL "="; i = NUM -> int_of_string i ];
-      width = OPT [ IDENT "depth"; SYMBOL "="; i = NUM -> int_of_string i ] -> 
+      width = OPT [ IDENT "width"; SYMBOL "="; i = NUM -> int_of_string i ] -> 
           TacticAst.Auto (loc,depth,width)
     | IDENT "clear"; id = IDENT ->
         TacticAst.Clear (loc,id)
@@ -381,7 +384,7 @@ EXTEND
         TacticAst.Cut (loc, ident, t)
     | IDENT "decide"; IDENT "equality" ->
         TacticAst.DecideEquality loc
-    | IDENT "decompose"; where = term ->
+    | IDENT "decompose"; where = tactic_term ->
         TacticAst.Decompose (loc, where)
     | IDENT "discriminate"; t = tactic_term ->
         TacticAst.Discriminate (loc, t)
@@ -399,25 +402,29 @@ EXTEND
         TacticAst.Fold (loc, kind, p)
     | IDENT "fourier" ->
         TacticAst.Fourier loc
-    | IDENT "fwd"; t = term ->
-        TacticAst.FwdSimpl (loc, t)
+    | IDENT "fwd"; hyp = IDENT; idents = OPT ident_list0 ->
+        let idents = match idents with None -> [] | Some idents -> idents in
+        TacticAst.FwdSimpl (loc, hyp, idents)
     | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
        TacticAst.Generalize (loc,p,id)
     | IDENT "goal"; n = NUM ->
         TacticAst.Goal (loc, int_of_string n)
     | IDENT "id" -> TacticAst.IdTac loc
-    | IDENT "injection"; t = term ->
+    | IDENT "injection"; t = tactic_term ->
         TacticAst.Injection (loc, t)
-    | IDENT "intros"; num = OPT [num = int -> num]; idents = OPT ident_list0 ->
-        let idents = match idents with None -> [] | Some idents -> idents in
-        TacticAst.Intros (loc, num, idents)
     | IDENT "intro"; ident = OPT IDENT ->
         let idents = match ident with None -> [] | Some id -> [id] in
         TacticAst.Intros (loc, Some 1, idents)
-    | IDENT "lapply"; what = tactic_term; 
-      to_what = OPT [ "to" ; t = tactic_term -> t ];
-      ident = OPT [ "using" ; id = IDENT -> id ] ->
-        TacticAst.LApply (loc, to_what, what, ident)
+    | IDENT "intros"; num = OPT [num = int -> num]; idents = OPT ident_list0 ->
+        let idents = match idents with None -> [] | Some idents -> idents in
+        TacticAst.Intros (loc, num, idents)
+    | IDENT "lapply"; 
+      depth = OPT [ IDENT "depth"; SYMBOL "="; i = NUM -> int_of_string i ];
+      what = tactic_term; 
+      to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
+      ident = OPT [ "using" ; ident = IDENT -> ident ] ->
+        let to_what = match to_what with None -> [] | Some to_what -> to_what in
+        TacticAst.LApply (loc, depth, to_what, what, ident)
     | IDENT "left" -> TacticAst.Left loc
     | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
         TacticAst.LetIn (loc, t, where)
@@ -427,7 +434,7 @@ EXTEND
         TacticAst.Reflexivity loc
     | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
         TacticAst.Replace (loc, p, t)
-    | IDENT "rewrite" ; d = direction; t = term ; p = pattern_spec ->
+    | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec ->
        let (pt,_,_) = p in
         if pt <> None then
          raise
@@ -454,7 +461,7 @@ EXTEND
       ]
     | "then" NONA
       [ tac = tactical;
-        PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" ->
+        PAREN "["; tacs = LIST0 tactical SEP SYMBOL "|"; PAREN "]" ->
           (TacticAst.Then (loc, tac, tacs))
       ]
     | "loops" RIGHTA