LexiconAstPp: fixed syntax for include

[helm.git] / helm / software / components / grafite_parser / grafiteParser.ml

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 586cca004a50f1563bca7e6a3857d160a025082b..64c10b9b47e575db35b37981aa79ffc15c95d3b8 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -218,8 +218,6 @@ 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;
@@ -428,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)
@@ -576,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),_,_) :: _ ->
@@ -590,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))
@@ -665,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
     ]