X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualParser2.ml;h=feb161d7fe84aaa022271e5d7338b839a0f9e17b;hb=358cefe50cccd4cb7d8e2a9cecb7efcb5780b8a3;hp=9f65555a4e80c8dc999fad607b484d55df5ef9cb;hpb=e42e345f711e051c903072d8cd994ab7b2154b25;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 9f65555a4..feb161d7f 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -171,15 +171,16 @@ EXTEND
         (head, vars)
     ]
   ];
+  arg: [
+   [ PAREN "(" ; names = LIST1 IDENT SEP SYMBOL ",";
+      SYMBOL ":"; ty = term; PAREN ")" -> names,ty
+   | name = IDENT -> [name],CicAst.Implicit
+   ]
+  ];
   let_defs:[
     [ defs = LIST1 [
         name = IDENT;
-        args = LIST1 [
-            PAREN "(" ; names = LIST1 IDENT SEP SYMBOL ",";
-            SYMBOL ":"; ty = term; PAREN ")" ->
-              (names, Some ty)
-          | name = IDENT -> [name],None
-        ];
+        args = LIST1 [arg = arg -> arg];
         index_name = OPT [ IDENT "on"; idx = IDENT -> idx ];
         ty = OPT [ SYMBOL ":" ; t = term -> t ];
         SYMBOL <:unicode<def>> (* ≝ *);
@@ -196,12 +197,6 @@ EXTEND
                 list_of_binder binder ty 
                   (binder_of_arg_list binder final_term tl) l
           in
-          let args = 
-           List.map
-            (function
-                names,Some ty -> names,ty
-              | names,None -> names,CicAst.Implicit
-            ) args in
           let t1' = binder_of_arg_list `Lambda t1 args in
           let ty' = 
             match ty with 
@@ -457,9 +452,7 @@ EXTEND
     ]
   ];
   inductive_spec: [ [
-    fst_name = IDENT; params = LIST0 [
-      PAREN "("; names = LIST1 IDENT SEP SYMBOL ","; SYMBOL ":";
-      typ = term; PAREN ")" -> (names, typ) ];
+    fst_name = IDENT; params = LIST0 [ arg=arg -> arg ];
     SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
     fst_constructors = LIST0 constructor SEP SYMBOL "|";
     tl = OPT [ "with";
@@ -479,7 +472,22 @@ EXTEND
       let ind_types = fst_ind_type :: tl_ind_types in
       (params, ind_types)
   ] ];
-
+  
+  record_spec: [ [
+    name = IDENT; params = LIST0 [ arg = arg -> arg ] ;
+     SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; PAREN "{" ; 
+     fields = LIST0 [ 
+       name = IDENT ; SYMBOL ":" ; ty = term -> (name,ty) 
+     ] SEP SYMBOL ";"; PAREN "}" -> 
+      let params =
+        List.fold_right
+          (fun (names, typ) acc ->
+            (List.map (fun name -> (name, typ)) names) @ acc)
+          params []
+      in
+      (params,name,typ,fields)
+  ] ];
+  
   macro: [
     [ [ IDENT "quit"  ] -> TacticAst.Quit loc
 (*     | [ IDENT "abort" ] -> TacticAst.Abort loc *)
@@ -545,9 +553,12 @@ EXTEND
       [ IDENT "set"    ]; n = QSTRING; v = QSTRING ->
         TacticAst.Set (loc, n, v)
     | [ IDENT "qed"   ] -> TacticAst.Qed loc
-    | flavour = theorem_flavour; name = OPT IDENT; SYMBOL ":"; typ = term;
+    | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
+      body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+        TacticAst.Obj (loc,TacticAst.Theorem (flavour, name, typ, body))
+    | flavour = theorem_flavour; name = IDENT;
       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
-        TacticAst.Theorem (loc, flavour, name, typ, body)
+        TacticAst.Obj (loc,TacticAst.Theorem (flavour, name, CicAst.Implicit, body))
     | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
         defs = let_defs -> 
           let name,ty = 
@@ -557,25 +568,27 @@ EXTEND
             | _ -> assert false 
           in
           let body = CicAst.Ident (name,None) in
-          TacticAst.Theorem(loc, `Definition, Some name, ty,
-            Some (CicAst.LetRec (ind_kind, defs, body)))
+          TacticAst.Obj (loc,TacticAst.Theorem(`Definition, name, ty,
+            Some (CicAst.LetRec (ind_kind, defs, body))))
           
     | [ IDENT "inductive" ]; spec = inductive_spec ->
         let (params, ind_types) = spec in
-        TacticAst.Inductive (loc, params, ind_types)
+        TacticAst.Obj (loc,TacticAst.Inductive (params, ind_types))
     | [ IDENT "coinductive" ]; 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
-        TacticAst.Inductive (loc, params, ind_types)
+        TacticAst.Obj (loc,TacticAst.Inductive (params, ind_types))
     | [ IDENT "coercion" ] ; name = IDENT -> 
         TacticAst.Coercion (loc, CicAst.Ident (name,Some []))
     | [ IDENT "coercion" ] ; name = URI -> 
         TacticAst.Coercion (loc, CicAst.Uri (name,Some []))
     | [ IDENT "alias"   ]; spec = alias_spec ->
         TacticAst.Alias (loc, spec)
+    | [ IDENT "record" ]; (params,name,ty,fields) = record_spec ->
+        TacticAst.Obj (loc,TacticAst.Record (params,name,ty,fields))
   ]];
 
   executable: [