X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_parser%2FgrafiteParser.ml;h=586cca004a50f1563bca7e6a3857d160a025082b;hb=e00d05ab58597620345c2fd49b84a23efa8db34c;hp=a78ca811332486a2fced5260c7651f6aee9ae116;hpb=06e2976ca4ef6bdfe14beba14ba538a2479c51a8;p=helm.git

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index a78ca8113..586cca004 100644
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -35,7 +35,8 @@ type 'a localized_option =
 
 type ast_statement =
   (CicNotationPt.term, CicNotationPt.term,
-   CicNotationPt.term GrafiteAst.reduction, CicNotationPt.obj, string)
+   CicNotationPt.term GrafiteAst.reduction, 
+   CicNotationPt.term CicNotationPt.obj, string)
     GrafiteAst.statement
 
 type statement =
@@ -115,9 +116,15 @@ EXTEND
     | SYMBOL "<" -> `RightToLeft ]
   ];
   int: [ [ num = NUMBER -> int_of_string num ] ];
+  intros_names: [
+   [ idents = OPT ident_list0 ->
+      match idents with None -> [] | Some idents -> idents
+   ]
+  ];
   intros_spec: [
-    [ num = OPT [ num = int -> num ]; idents = OPT ident_list0 ->
-        let idents = match idents with None -> [] | Some idents -> idents in
+    [ OPT [ IDENT "names" ]; 
+      num = OPT [ num = int -> num ]; 
+      idents = intros_names ->
         num, idents
     ]
   ];
@@ -135,6 +142,9 @@ EXTEND
         GrafiteAst.Assumption loc
     | IDENT "auto"; params = auto_params ->
         GrafiteAst.Auto (loc,params)
+    | IDENT "cases"; what = tactic_term;
+      (num, idents) = intros_spec ->
+	GrafiteAst.Cases (loc, what, idents)
     | IDENT "clear"; ids = LIST1 IDENT ->
         GrafiteAst.Clear (loc, ids)
     | IDENT "clearbody"; id = IDENT ->
@@ -208,9 +218,12 @@ EXTEND
         GrafiteAst.Reduce (loc, kind, p)
     | IDENT "reflexivity" ->
         GrafiteAst.Reflexivity loc
+    | IDENT "rename"; froms = ident_list0; "as"; tos = ident_list0 ->
+	GrafiteAst.Rename (loc, froms, tos)
     | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
         GrafiteAst.Replace (loc, p, t)
-    | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec ->
+    | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
+       xnames = OPT [ "as"; n = ident_list0 -> n ] ->
        let (pt,_,_) = p in
         if pt <> None then
          raise
@@ -218,7 +231,8 @@ EXTEND
            (CicNotationParser.Parse_error
             "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
         else
-         GrafiteAst.Rewrite (loc, d, t, p)
+	 let n = match xnames with None -> [] | Some names -> names in 
+         GrafiteAst.Rewrite (loc, d, t, p, n)
     | IDENT "right" ->
         GrafiteAst.Right loc
     | IDENT "ring" ->
@@ -259,6 +273,8 @@ EXTEND
               | LSome t -> GrafiteAst.AndElim (loc, t, id1, t1, id2, t2)))
     | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; id = OPT [ LPAREN ; id = IDENT ; RPAREN -> id ] ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term -> t']->
         GrafiteAst.We_need_to_prove (loc, t, id, t1)
+    | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->  
+        GrafiteAst.We_proceed_by_cases_on (loc, t, t1)
     | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->  
         GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
     | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->