X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualParser2.ml;h=a7d43bb45f75461cda893201a49459bc458f0dda;hb=2eb1644f907fc2319957fad1511ad98dccc89209;hp=6e368d79bdbb13fd0ab4fbf7171fa765c96a057c;hpb=aeec9dd128be72caf5a39bac3a0ef34b564ecd8b;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 6e368d79b..a7d43bb45 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -171,14 +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, ty)
-        ];
+        args = LIST1 [arg = arg -> arg];
         index_name = OPT [ IDENT "on"; idx = IDENT -> idx ];
         ty = OPT [ SYMBOL ":" ; t = term -> t ];
         SYMBOL <:unicode<def>> (* ≝ *);
@@ -294,7 +296,7 @@ EXTEND
             return_term loc (CicAst.Meta (index, substs))
       | outtyp = OPT [ PAREN "["; typ = term; PAREN "]" -> typ ];
         "match"; t = term;
-        indty_ident = OPT [ SYMBOL ":"; id = IDENT -> id ];
+        indty_ident = OPT ["in" ; id = IDENT -> id ];
         "with";
         PAREN "[";
         patterns = LIST0 [
@@ -377,8 +379,8 @@ EXTEND
     | [ IDENT "intro" ] ->
         TacticAst.Intros (loc, Some 1, [])
     | [ IDENT "left" ] -> TacticAst.Left loc
-    | [ "let" | "Let" ];
-      t = tactic_term; "in"; where = IDENT ->
+    | [ IDENT "letin" ];
+       where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
         TacticAst.LetIn (loc, t, where)
     | kind = reduction_kind;
       pat = OPT [
@@ -450,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";
@@ -472,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 *)
@@ -541,13 +556,15 @@ EXTEND
     | flavour = theorem_flavour; name = OPT IDENT; SYMBOL ":"; typ = term;
       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
         TacticAst.Theorem (loc, flavour, name, typ, body)
+    | flavour = theorem_flavour; name = OPT IDENT;
+      body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+        TacticAst.Theorem (loc, flavour, name, CicAst.Implicit, body)
     | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
         defs = let_defs -> 
           let name,ty = 
             match defs with
             | ((Cic.Name name,Some ty),_,_) :: _ -> name,ty
-            | ((Cic.Name name,None),_,_) :: _ -> 
-                fail loc ("No type given for " ^ name)
+            | ((Cic.Name name,None),_,_) :: _ -> name,CicAst.Implicit
             | _ -> assert false 
           in
           let body = CicAst.Ident (name,None) in
@@ -570,6 +587,8 @@ EXTEND
         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.Record (loc, params,name,ty,fields)
   ]];
 
   executable: [