removed ocaml-pxp

[helm.git] / helm / ocaml / cic_disambiguation / cicTextualParser2.ml

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index fda6d14e636eac74aefc6da73e0b6a22d7dda114..a7d43bb45f75461cda893201a49459bc458f0dda 100644 (file)
--- 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 ",";
-          ty = OPT [ SYMBOL ":"; ty = term -> ty ] ; 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>> (* ≝ *);
@@ -195,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 
@@ -456,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";
@@ -478,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 *)
@@ -547,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
@@ -576,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: [