src/HOLCF/Tools/domain/domain_library.ML

   val `% : term * string -> term;
   val /\ : string -> term -> term;
   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;
   val mk_stuple : term list -> term;
   val mk_ctuple : term list -> term;

   type cons = string * arg list;
   type eq = (string * typ list) * cons list;
   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;
   val is_rec : arg -> bool;
   val is_nonlazy_rec : arg -> bool;

   val when_funs : 'a list -> string list;
   val bound_arg : ''a list -> ''a -> term; (* ''a = arg or string *)
   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 *)
   val strip_esc : string -> string;
   val extern_name : string -> string;

 fun rec_of ((_,dtyp),_,_) =
   case dtyp of DatatypeAux.DtRec i => i | _ => ~1;
 (* 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;
 fun is_rec         arg = rec_of arg >=0;
 fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg);
 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]);
 fun mk_cfunT (T, U) = Type(@{type_name "->"}, [T, U]);