X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=9a0cc9f438ae90941aa7f41ddf169bf626777224;hb=8402a4a856b031916b1e2b1354b863933763fa58;hp=4c1ddffb20c07617f96b4da6fbb3340aa8b2ceb4;hpb=403b7486e9f2cb5583a2c8035cf419bbac982fb1;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 4c1ddffb2..9a0cc9f43 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/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 ->
@@ -210,7 +220,8 @@ EXTEND
         GrafiteAst.Reflexivity loc
     | 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 +229,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 +271,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 ->
@@ -268,9 +282,9 @@ EXTEND
     | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
         SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
 	 GrafiteAst.Case(loc,id,params)
-    | IDENT "obtain" ; termine=tactic_term ; SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> `Term t | SYMBOL "_" ; params = auto_params -> `Auto params  ] ; cont=rewriting_step_continuation ->
-     GrafiteAst.RewritingStep(loc, Some termine, t1, t2, cont)
-    | SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> `Term t | SYMBOL "_" ; params = auto_params -> `Auto params ] ;
+    | start=[IDENT "conclude" -> None | IDENT "obtain" ; name = IDENT -> Some name] ; termine=tactic_term ; SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> `Term t | SYMBOL "_" ; params = auto_params' -> `Auto params  ] ; cont=rewriting_step_continuation ->
+     GrafiteAst.RewritingStep(loc, Some (start,termine), t1, t2, cont)
+    | SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> `Term t | SYMBOL "_" ; params = auto_params' -> `Auto params ] ;
       cont=rewriting_step_continuation  ->
      GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
   ]
@@ -281,6 +295,11 @@ EXTEND
        string_of_int v | v = IDENT -> v ] -> i,v ] ->
       params
    ]
+];
+  auto_params': [
+   [ LPAREN; params = auto_params; RPAREN -> params
+   | -> []
+   ]
 ];
   by_continuation: [
     [ IDENT "we" ; IDENT "proved" ; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] -> BYC_weproved (ty,Some id,t1)
@@ -294,9 +313,8 @@ EXTEND
     ]
 ];
   rewriting_step_continuation : [
-    [ IDENT "done" -> None
-    | IDENT "we" ; IDENT "proved" ; id=IDENT -> Some (Cic.Name id)
-    | -> Some Cic.Anonymous
+    [ IDENT "done" -> true
+    | -> false
     ]
 ];
   atomic_tactical:
@@ -407,9 +425,15 @@ EXTEND
   macro: [
     [ [ IDENT "check"   ]; t = term ->
         GrafiteAst.Check (loc, t)
-    | [ IDENT "inline"]; suri = QSTRING; prefix = OPT QSTRING ->
-         let prefix = match prefix with None -> "" | Some prefix -> prefix in
-	 GrafiteAst.Inline (loc,suri,prefix)
+    | [ IDENT "inline"]; 
+        style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
+	suri = QSTRING; prefix = OPT QSTRING ->
+         let style = match style with 
+	    | None       -> GrafiteAst.Declarative
+	    | Some depth -> GrafiteAst.Procedural depth
+	 in
+	 let prefix = match prefix with None -> "" | Some prefix -> prefix in
+	 GrafiteAst.Inline (loc,style,suri,prefix)
     | [ IDENT "hint" ] -> GrafiteAst.Hint loc
     | [ IDENT "whelp"; "match" ] ; t = term -> 
         GrafiteAst.WMatch (loc,t)
@@ -550,6 +574,11 @@ EXTEND
         GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
     | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
         defs = CicNotationParser.let_defs -> 
+         (* In case of mutual definitions here we produce just
+            the syntax tree for the first one. The others will be
+            generated from the completely specified term just before
+            insertion in the environment. We use the flavour
+            `MutualDefinition to rememer this. *)
           let name,ty = 
             match defs with
             | (params,(Ast.Ident (name, None), Some ty),_,_) :: _ ->
@@ -564,8 +593,14 @@ EXTEND
             | _ -> assert false 
           in
           let body = Ast.Ident (name,None) in
-          GrafiteAst.Obj (loc, Ast.Theorem(`Definition, name, ty,
-            Some (Ast.LetRec (ind_kind, defs, body))))
+          let flavour =
+           if List.length defs = 1 then
+            `Definition
+           else
+            `MutualDefinition
+          in
+           GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty,
+             Some (Ast.LetRec (ind_kind, defs, body))))
     | IDENT "inductive"; spec = inductive_spec ->
         let (params, ind_types) = spec in
         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))