X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=64c10b9b47e575db35b37981aa79ffc15c95d3b8;hb=64d7a7dfa840d7279f9af64240ee1f8a69181801;hp=054bff6215e1f64ec1b6d90813a3f7a316b88089;hpb=d669da59d27e2418e65a275dc5d405237db2b93a;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 054bff621..64c10b9b4 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -220,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
@@ -228,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" ->
@@ -424,11 +426,11 @@ EXTEND
     [ [ IDENT "check"   ]; t = term ->
         GrafiteAst.Check (loc, t)
     | [ IDENT "inline"]; 
-        style = OPT [ IDENT "procedural" ];
+        style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
 	suri = QSTRING; prefix = OPT QSTRING ->
          let style = match style with 
-	    | None   -> GrafiteAst.Declarative
-	    | Some _ -> GrafiteAst.Procedural
+	    | 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)
@@ -572,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),_,_) :: _ ->
@@ -586,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))
@@ -661,7 +674,7 @@ EXTEND
             (loc,GrafiteAst.Include (iloc,buri))))
     | scom = lexicon_command ; SYMBOL "." ->
        fun ~include_paths status ->
-        let status = LexiconEngine.eval_command status scom in
+	let status = LexiconEngine.eval_command status scom in
          status,LNone loc
     | EOI -> raise End_of_file
     ]