1. new syntax for patterns:

[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 352c925fbba057947ede41bab2f91fec9f6aa929..fc46cc725e8626ee62f5b0bf0bd949ee4386cc7a 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -325,15 +325,30 @@ EXTEND
     | [ IDENT "normalize" ] -> `Normalize ]
   ];
   pattern_spec: [
-    [ "in";
-      hyp_paths =
-       LIST0
-        [ id = IDENT ;
-          path = OPT [SYMBOL ":" ; path = term -> path ] ->
-          (id,match path with Some p -> p | None -> CicAst.UserInput) ]
-        SEP SYMBOL ";";
-      goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = term -> term ] ->
-        (hyp_paths, goal_path) ]
+    [ wanted = OPT term;
+      hyp_paths_and_goal_path =
+       OPT [
+        "in";
+        hyp_paths =
+         LIST0
+          [ id = IDENT ;
+            path = OPT [SYMBOL ":" ; path = term -> path ] ->
+            (id,match path with Some p -> p | None -> CicAst.UserInput) ]
+          SEP SYMBOL ";";
+        goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = term -> term ] ->
+         let goal_path =
+          match goal_path with
+             None -> CicAst.UserInput
+           | Some goal_path -> goal_path
+         in
+          hyp_paths,goal_path
+       ] ->
+         let hyp_paths,goal_path =
+          match hyp_paths_and_goal_path with
+             None -> [], CicAst.UserInput
+           | Some (hyp_paths,goal_path) -> hyp_paths,goal_path
+         in
+          wanted, hyp_paths, goal_path ]
   ];
   direction: [
     [ IDENT "left" -> `Left
@@ -356,9 +371,8 @@ EXTEND
         TacticAst.Clear (loc,id)
     | IDENT "clearbody"; id = IDENT ->
         TacticAst.ClearBody (loc,id)
-    | IDENT "change"; t1 = tactic_term; "with"; t2 = tactic_term; "in";
-      where = pattern_spec ->
-        TacticAst.Change (loc, t1, t2, where)
+    | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
+        TacticAst.Change (loc, what, t)
     | IDENT "compare"; t = tactic_term ->
         TacticAst.Compare (loc,t)
     | IDENT "constructor"; n = NUM ->
@@ -383,19 +397,14 @@ EXTEND
     | IDENT "exists" ->
         TacticAst.Exists loc
     | IDENT "fail" -> TacticAst.Fail loc
-    | IDENT "fold"; kind = reduction_kind; t = tactic_term;
-      p = OPT [ pattern_spec ] ->
-        let p = match p with None -> [], None | Some p -> p in
-        TacticAst.Fold (loc, kind, t, p)
+    | IDENT "fold"; kind = reduction_kind; p = pattern_spec ->
+        TacticAst.Fold (loc, kind, p)
     | IDENT "fourier" ->
         TacticAst.Fourier loc
     | IDENT "fwd"; t = term ->
         TacticAst.FwdSimpl (loc, t)
-    | IDENT "generalize"; t = tactic_term;
-       id = OPT [ "as" ; id = IDENT -> id ];
-       p = OPT [ pattern_spec ] ->
-       let p = match p with None -> [], None | Some p -> p in
-       TacticAst.Generalize (loc,t,id,p)
+    | 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
@@ -414,17 +423,20 @@ EXTEND
     | IDENT "left" -> TacticAst.Left loc
     | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
         TacticAst.LetIn (loc, t, where)
-    | kind = reduction_kind; p = OPT [ pattern_spec ] ->
-        let p = match p with None -> [], None | Some p -> p in
+    | kind = reduction_kind; p = pattern_spec ->
         TacticAst.Reduce (loc, kind, p)
     | IDENT "reflexivity" ->
         TacticAst.Reflexivity loc
-    | IDENT "replace"; p = OPT [ pattern_spec ]; "with"; t = tactic_term ->
-        let p = match p with None -> [], None | Some p -> p in
+    | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
         TacticAst.Replace (loc, p, t)
-    | IDENT "rewrite" ; d = direction; t = term ; p = OPT [ pattern_spec ] ->
-        let p = match p with None -> [], None | Some p -> p in
-        TacticAst.Rewrite (loc, d, t, p)
+    | IDENT "rewrite" ; d = direction; t = term ; p = pattern_spec ->
+       let (pt,_,_) = p in
+        if pt <> None then
+         raise
+          (Parse_error
+            (loc,"the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion"))
+        else
+         TacticAst.Rewrite (loc, d, t, p)
     | IDENT "right" ->
         TacticAst.Right loc
     | IDENT "ring" ->