Big commit and major code clean-up:

[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 3d7699ecde14207b2d3e7ad4410321d927f1076a..feb161d7fe84aaa022271e5d7338b839a0f9e17b 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 ","; 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>> (* ≝ *);
@@ -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 *)
@@ -538,38 +553,42 @@ 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 = 
             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
-          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: [