export ID, oo; add more dtyp operations

--- a/src/HOLCF/Tools/domain/domain_library.ML	Fri May 22 10:34:22 2009 -0700
+++ b/src/HOLCF/Tools/domain/domain_library.ML	Fri May 22 10:36:38 2009 -0700
@@ -78,6 +78,8 @@
   val UU : term;
   val TT : term;
   val FF : term;
+  val ID : term;
+  val oo : term * term -> term;
   val mk_up : term -> term;
   val mk_sinl : term -> term;
   val mk_sinr : term -> term;
@@ -131,6 +133,7 @@
   val mk_arg : (bool * DatatypeAux.dtyp) * string option * string -> arg;
   val is_lazy : arg -> bool;
   val rec_of : arg -> int;
+  val dtyp_of : arg -> DatatypeAux.dtyp;
   val sel_of : arg -> string option;
   val vname : arg -> string;
   val upd_vname : (string -> string) -> arg -> arg;
@@ -146,6 +149,7 @@
   val idx_name : 'a list -> string -> int -> string;
   val app_rec_arg : (int -> term) -> arg -> term;
   val con_app : string -> arg list -> term;
+  val dtyp_of_eq : eq -> DatatypeAux.dtyp;
 
 
   (* Name mangling *)
@@ -223,6 +227,7 @@
 (* FIXME: what about indirect recursion? *)
 
 fun is_lazy arg = fst (first arg);
+fun dtyp_of arg = snd (first arg);
 val sel_of    =       second;
 val     vname =       third;
 val upd_vname =   upd_third;
@@ -231,6 +236,25 @@
 fun nonlazy     args   = map vname (filter_out is_lazy    args);
 fun nonlazy_rec args   = map vname (List.filter is_nonlazy_rec args);
 
+
+(* ----- combinators for making dtyps ----- *)
+
+fun mk_uD T = DatatypeAux.DtType(@{type_name "u"}, [T]);
+fun mk_sprodD (T, U) = DatatypeAux.DtType(@{type_name "**"}, [T, U]);
+fun mk_ssumD (T, U) = DatatypeAux.DtType(@{type_name "++"}, [T, U]);
+fun mk_liftD T = DatatypeAux.DtType(@{type_name "lift"}, [T]);
+val unitD = DatatypeAux.DtType(@{type_name "unit"}, []);
+val boolD = DatatypeAux.DtType(@{type_name "bool"}, []);
+val oneD = mk_liftD unitD;
+val trD = mk_liftD boolD;
+fun big_sprodD ds = case ds of [] => oneD | _ => foldr1 mk_sprodD ds;
+fun big_ssumD ds = case ds of [] => unitD | _ => foldr1 mk_ssumD ds;
+
+fun dtyp_of_arg ((lazy, D), _, _) = if lazy then mk_uD D else D;
+fun dtyp_of_cons (_, args) = big_sprodD (map dtyp_of_arg args);
+fun dtyp_of_eq (_, cons) = big_ssumD (map dtyp_of_cons cons);
+
+
 (* ----- support for type and mixfix expressions ----- *)
 
 fun mk_uT T = Type(@{type_name "u"}, [T]);