New content level representations for LetRec, Inductive and CoInductive.

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

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index af185a63eb93eccf67b2f447cc6c1115729d915d..9b9a5da22ed93d8534681ce02a4ef18042b9338e 100644 (file)
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -61,12 +61,6 @@ type by_continuation =
 
 EXTEND
   GLOBAL: term statement;
-  arg: [
-   [ LPAREN; names = LIST1 IDENT SEP SYMBOL ",";
-      SYMBOL ":"; ty = term; RPAREN -> names,ty
-   | name = IDENT -> [name],Ast.Implicit
-   ]
-  ];
   constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
   tactic_term: [ [ t = term LEVEL "90N" -> t ] ];
   ident_list0: [ [ LPAREN; idents = LIST0 IDENT; RPAREN -> idents ] ];
@@ -360,7 +354,7 @@ EXTEND
     ]
   ];
   inductive_spec: [ [
-    fst_name = IDENT; params = LIST0 [ arg=arg -> arg ];
+    fst_name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars;
     SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
     fst_constructors = LIST0 constructor SEP SYMBOL "|";
     tl = OPT [ "with";
@@ -382,7 +376,7 @@ EXTEND
   ] ];
   
   record_spec: [ [
-    name = IDENT; params = LIST0 [ arg = arg -> arg ] ;
+    name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars ;
      SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ; 
      fields = LIST0 [ 
        name = IDENT ; 
@@ -551,8 +545,14 @@ EXTEND
         defs = CicNotationParser.let_defs -> 
           let name,ty = 
             match defs with
-            | ((Ast.Ident (name, None), Some ty),_,_) :: _ -> name,ty
-            | ((Ast.Ident (name, None), None),_,_) :: _ ->
+            | (params,(Ast.Ident (name, None), Some ty),_,_) :: _ ->
+                let ty =
+                 List.fold_right
+                  (fun var ty -> Ast.Binder (`Pi,var,ty)
+                  ) params ty
+                in
+                 name,ty
+            | (_,(Ast.Ident (name, None), None),_,_) :: _ ->
                 name, Ast.Implicit
             | _ -> assert false 
           in