- Grammar for all obj commands ported to NG (let recs and inductives still need

[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 be6dab1a61085b8b84c0ec9d77d490f779944c95..389e2eb218201d00030b4f1c5fa3dbdc9031055d 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -67,7 +67,7 @@ let add_raw_attribute ~text t = Ast.AttributedTerm (`Raw text, t)
 
 let default_associativity = Gramext.NonA
         
-let mk_rec_corec ind_kind defs loc = 
+let mk_rec_corec ng ind_kind defs loc = 
  (* 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
@@ -93,7 +93,11 @@ let mk_rec_corec ind_kind defs loc =
    else
     `MutualDefinition
   in
-   GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty,
+   if ng then
+    GrafiteAst.NObj (loc, Ast.Theorem(flavour, name, ty,
+     Some (Ast.LetRec (ind_kind, defs, body))))
+   else
+    GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty,
      Some (Ast.LetRec (ind_kind, defs, body))))
 
 type by_continuation =
@@ -515,7 +519,11 @@ EXTEND
       ]
       ];
   ntheorem_flavour: [
-    [ [ IDENT "ntheorem"     ] -> `Theorem
+    [ [ IDENT "ndefinition"  ] -> `Definition
+    | [ IDENT "nfact"        ] -> `Fact
+    | [ IDENT "nlemma"       ] -> `Lemma
+    | [ IDENT "nremark"      ] -> `Remark
+    | [ IDENT "ntheorem"     ] -> `Theorem
     ]
   ];
   theorem_flavour: [
@@ -735,13 +743,22 @@ EXTEND
           Ast.Theorem (flavour, name, Ast.Implicit, Some body))
     | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
         GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
+    | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
+        GrafiteAst.NObj (loc, Ast.Theorem (`Axiom, name, typ, None))
     | LETCOREC ; defs = let_defs -> 
-        mk_rec_corec `CoInductive defs loc
+        mk_rec_corec false `CoInductive defs loc
     | LETREC ; defs = let_defs -> 
-        mk_rec_corec `Inductive defs loc
+        mk_rec_corec false `Inductive defs loc
+    | NLETCOREC ; defs = let_defs -> 
+        mk_rec_corec true `CoInductive defs loc
+    | NLETREC ; defs = let_defs -> 
+        mk_rec_corec true `Inductive defs loc
     | IDENT "inductive"; spec = inductive_spec ->
         let (params, ind_types) = spec in
         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
+    | IDENT "ninductive"; spec = inductive_spec ->
+        let (params, ind_types) = spec in
+        GrafiteAst.NObj (loc, Ast.Inductive (params, ind_types))
     | IDENT "coinductive"; spec = inductive_spec ->
         let (params, ind_types) = spec in
         let ind_types = (* set inductive flags to false (coinductive) *)
@@ -749,6 +766,13 @@ EXTEND
             ind_types
         in
         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
+    | IDENT "ncoinductive"; spec = inductive_spec ->
+        let (params, ind_types) = spec in
+        let ind_types = (* set inductive flags to false (coinductive) *)
+          List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
+            ind_types
+        in
+        GrafiteAst.NObj (loc, Ast.Inductive (params, ind_types))
     | IDENT "coercion" ; 
       t = [ u = URI -> Ast.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
       arity = OPT int ; saturations = OPT int;