(first) complete implementation of (mutual) (co)inductive types syntax

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index a1f431b60ef1e6f137e1b040b5eb080e637b7613..3a5f76b673cbfe3d9ccdd20ddd9b00f092fa36ca 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -364,6 +364,29 @@ EXTEND
     | [ IDENT "theorem"     | IDENT "Theorem"     ] -> `Theorem
     ]
   ];
+  inductive_spec: [ [
+    fst_name = IDENT; params = LIST0 [
+      PAREN "("; names = LIST1 IDENT SEP SYMBOL ","; SYMBOL ":";
+      typ = term; PAREN ")" -> (names, typ) ];
+    SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
+    fst_constructors = LIST0 constructor SEP SYMBOL "|";
+    tl = OPT [ "with";
+      types = LIST1 [
+        name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
+        OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
+          (name, true, typ, constructors) ] SEP "with" -> types
+    ] ->
+      let params =
+        List.fold_right
+          (fun (names, typ) acc ->
+            (List.map (fun name -> (name, typ)) names) @ acc)
+          params []
+      in
+      let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
+      let tl_ind_types = match tl with None -> [] | Some types -> types in
+      let ind_types = fst_ind_type :: tl_ind_types in
+      (params, ind_types)
+  ] ];
   command: [
     [ [ IDENT "abort" | IDENT "Abort" ] -> return_command loc TacticAst.Abort
     | [ IDENT "proof" | IDENT "Proof" ] -> return_command loc TacticAst.Proof
@@ -375,20 +398,15 @@ EXTEND
     | flavour = theorem_flavour; name = OPT IDENT; SYMBOL ":"; typ = term;
       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
         return_command loc (TacticAst.Theorem (flavour, name, typ, body))
-    | [ IDENT "inductive" | IDENT "Inductive" ]; fst_name = IDENT;
-      params = LIST0 [
-        PAREN "("; names = LIST1 IDENT SEP SYMBOL ","; SYMBOL ":";
-        typ = term; PAREN ")" -> (names, typ) ];
-      SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
-      fst_constructors = LIST0 constructor SEP SYMBOL "|" ->
-        let params =
-          List.fold_right
-            (fun (names, typ) acc ->
-              (List.map (fun name -> (name, typ)) names) @ acc)
-            params []
+    | [ IDENT "inductive" | IDENT "Inductive" ]; spec = inductive_spec ->
+        let (params, ind_types) = spec in
+        return_command loc (TacticAst.Inductive (params, ind_types))
+    | [ IDENT "coinductive" | 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
-        let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
-        let ind_types = [fst_ind_type] in
         return_command loc (TacticAst.Inductive (params, ind_types))
     | [ IDENT "goal" | IDENT "Goal" ]; typ = term;
       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->