src/ZF/Datatype.ML
changeset 6053 8a1059aa01f0
parent 1461 6bcb44e4d6e5
child 6112 5e4871c5136b
--- a/src/ZF/Datatype.ML	Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/Datatype.ML	Mon Dec 28 16:59:28 1998 +0100
@@ -7,63 +7,41 @@
 *)
 
 
-(*For most datatypes involving univ*)
-val datatype_intrs = 
-    [SigmaI, InlI, InrI,
-     Pair_in_univ, Inl_in_univ, Inr_in_univ, 
-     zero_in_univ, A_into_univ, nat_into_univ, UnCI];
-
-(*Needed for mutual recursion*)
-val datatype_elims = [make_elim InlD, make_elim InrD];
+(*Typechecking rules for most datatypes involving univ*)
+structure Data_Arg =
+  struct
+  val intrs = 
+      [SigmaI, InlI, InrI,
+       Pair_in_univ, Inl_in_univ, Inr_in_univ, 
+       zero_in_univ, A_into_univ, nat_into_univ, UnCI];
 
-(*For most codatatypes involving quniv*)
-val codatatype_intrs = 
-    [QSigmaI, QInlI, QInrI,
-     QPair_in_quniv, QInl_in_quniv, QInr_in_quniv, 
-     zero_in_quniv, A_into_quniv, nat_into_quniv, UnCI];
-
-val codatatype_elims = [make_elim QInlD, make_elim QInrD];
-
-signature INDUCTIVE_THMS =
-  sig
-  val monos      : thm list             (*monotonicity of each M operator*)
-  val type_intrs : thm list             (*type-checking intro rules*)
-  val type_elims : thm list             (*type-checking elim rules*)
+  (*Needed for mutual recursion*)
+  val elims = [make_elim InlD, make_elim InrD];
   end;
 
-functor Data_section_Fun
- (Arg: sig include CONSTRUCTOR_ARG INDUCTIVE_I INDUCTIVE_THMS end)  
-    : sig include CONSTRUCTOR_RESULT INTR_ELIM INDRULE end =
-struct
 
-structure Con = Constructor_Fun 
-        (structure Const = Arg and Pr=Standard_Prod and Su=Standard_Sum);
-
-structure Inductive = Ind_section_Fun
-   (open Arg; 
-    val con_defs = Con.con_defs
-    val type_intrs = Arg.type_intrs @ datatype_intrs
-    val type_elims = Arg.type_elims @ datatype_elims);
-
-open Inductive Con
-end;
+structure Data_Package = 
+    Add_datatype_def_Fun
+      (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
+       and Su=Standard_Sum
+       and Ind_Package = Ind_Package
+       and Datatype_Arg = Data_Arg);
 
 
-functor CoData_section_Fun
- (Arg: sig include CONSTRUCTOR_ARG INDUCTIVE_I INDUCTIVE_THMS end)  
-    : sig include CONSTRUCTOR_RESULT INTR_ELIM COINDRULE end =
-struct
-
-structure Con = Constructor_Fun 
-        (structure Const = Arg and Pr=Quine_Prod and Su=Quine_Sum);
+(*Typechecking rules for most codatatypes involving quniv*)
+structure CoData_Arg =
+  struct
+  val intrs = 
+      [QSigmaI, QInlI, QInrI,
+       QPair_in_quniv, QInl_in_quniv, QInr_in_quniv, 
+       zero_in_quniv, A_into_quniv, nat_into_quniv, UnCI];
 
-structure CoInductive = CoInd_section_Fun
-   (open Arg; 
-    val con_defs = Con.con_defs
-    val type_intrs = Arg.type_intrs @ codatatype_intrs
-    val type_elims = Arg.type_elims @ codatatype_elims);
+  val elims = [make_elim QInlD, make_elim QInrD];
+  end;
 
-open CoInductive Con
-end;
+structure CoData_Package = 
+    Add_datatype_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
+                          and Su=Quine_Sum
+			  and Ind_Package = CoInd_Package
+			  and Datatype_Arg = CoData_Arg);
 
-