--- a/src/HOL/Tools/Datatype/datatype_aux.ML Wed Dec 02 11:29:49 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML Fri Dec 04 12:17:43 2009 +0100
@@ -374,7 +374,7 @@
then NONE
else Option.map (Integer.add 1 o snd) (find_nonempty descr (i::is) i)
| arg_nonempty _ = SOME 0;
- fun max_inf (SOME i) (SOME j) = Integer.max i j
+ fun max_inf (SOME i) (SOME j) = SOME (Integer.max i j)
| max_inf _ _ = NONE;
fun max xs = fold max_inf xs (SOME 0);
val (_, _, constrs) = the (AList.lookup (op =) descr i);
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML Wed Dec 02 11:29:49 2009 +0100
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Fri Dec 04 12:17:43 2009 +0100
@@ -38,10 +38,10 @@
(@{type_name "u"}, @{const_name "u_map"})];
fun copy_of_dtyp tab r dt =
- if DatatypeAux.is_rec_type dt then copy tab r dt else ID
-and copy tab r (DatatypeAux.DtRec i) = r i
- | copy tab r (DatatypeAux.DtTFree a) = ID
- | copy tab r (DatatypeAux.DtType (c, ds)) =
+ if Datatype_Aux.is_rec_type dt then copy tab r dt else ID
+and copy tab r (Datatype_Aux.DtRec i) = r i
+ | copy tab r (Datatype_Aux.DtTFree a) = ID
+ | copy tab r (Datatype_Aux.DtType (c, ds)) =
case Symtab.lookup tab c of
SOME f => list_ccomb (%%:f, map (copy_of_dtyp tab r) ds)
| NONE => (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID);
--- a/src/HOLCF/Tools/Domain/domain_extender.ML Wed Dec 02 11:29:49 2009 +0100
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML Fri Dec 04 12:17:43 2009 +0100
@@ -162,7 +162,7 @@
fun one_con (con,args,mx) =
((Syntax.const_name mx (Binding.name_of con)),
ListPair.map (fn ((lazy,sel,tp),vn) =>
- mk_arg ((lazy, DatatypeAux.dtyp_of_typ new_dts tp),
+ mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp),
Option.map Binding.name_of sel,vn))
(args,(mk_var_names(map (typid o third) args)))
) : cons;
@@ -237,7 +237,7 @@
fun one_con (con,args,mx) =
((Syntax.const_name mx (Binding.name_of con)),
ListPair.map (fn ((lazy,sel,tp),vn) =>
- mk_arg ((lazy, DatatypeAux.dtyp_of_typ new_dts tp),
+ mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp),
Option.map Binding.name_of sel,vn))
(args,(mk_var_names(map (typid o third) args)))
) : cons;
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Wed Dec 02 11:29:49 2009 +0100
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Dec 04 12:17:43 2009 +0100
@@ -581,12 +581,12 @@
mk_fst t :: mk_copy_args xs (mk_snd t);
in mk_copy_args doms copy_arg end;
fun copy_of_dtyp (T, dt) =
- if DatatypeAux.is_rec_type dt
+ if Datatype_Aux.is_rec_type dt
then copy_of_dtyp' (T, dt)
else ID_const T
- and copy_of_dtyp' (T, DatatypeAux.DtRec i) = nth copy_args i
- | copy_of_dtyp' (T, DatatypeAux.DtTFree a) = ID_const T
- | copy_of_dtyp' (T as Type (_, Ts), DatatypeAux.DtType (c, ds)) =
+ and copy_of_dtyp' (T, Datatype_Aux.DtRec i) = nth copy_args i
+ | copy_of_dtyp' (T, Datatype_Aux.DtTFree a) = ID_const T
+ | copy_of_dtyp' (T as Type (_, Ts), Datatype_Aux.DtType (c, ds)) =
case Symtab.lookup map_tab' c of
SOME f =>
Library.foldl mk_capply
@@ -599,7 +599,7 @@
val copy_bind = Binding.suffix_name "_copy" tbind;
val (copy_const, thy) = thy |>
Sign.declare_const ((copy_bind, copy_type), NoSyn);
- val dtyp = DatatypeAux.dtyp_of_typ new_dts rhsT;
+ val dtyp = Datatype_Aux.dtyp_of_typ new_dts rhsT;
val body = copy_of_dtyp (rhsT, dtyp);
val comp = mk_cfcomp (abs_const, mk_cfcomp (body, rep_const));
val rhs = big_lambda copy_arg comp;
--- a/src/HOLCF/Tools/Domain/domain_library.ML Wed Dec 02 11:29:49 2009 +0100
+++ b/src/HOLCF/Tools/Domain/domain_library.ML Fri Dec 04 12:17:43 2009 +0100
@@ -230,7 +230,7 @@
val mk_arg = I;
fun rec_of ((_,dtyp),_,_) =
- case dtyp of DatatypeAux.DtRec i => i | _ => ~1;
+ case dtyp of Datatype_Aux.DtRec i => i | _ => ~1;
(* FIXME: what about indirect recursion? *)
fun is_lazy arg = fst (first arg);
@@ -246,12 +246,12 @@
(* ----- 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"}, []);
+fun mk_uD T = Datatype_Aux.DtType(@{type_name "u"}, [T]);
+fun mk_sprodD (T, U) = Datatype_Aux.DtType(@{type_name "**"}, [T, U]);
+fun mk_ssumD (T, U) = Datatype_Aux.DtType(@{type_name "++"}, [T, U]);
+fun mk_liftD T = Datatype_Aux.DtType(@{type_name "lift"}, [T]);
+val unitD = Datatype_Aux.DtType(@{type_name "unit"}, []);
+val boolD = Datatype_Aux.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;
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Wed Dec 02 11:29:49 2009 +0100
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Fri Dec 04 12:17:43 2009 +0100
@@ -600,7 +600,7 @@
let
val lhs = dc_copy`%"f"`(con_app con args);
fun one_rhs arg =
- if DatatypeAux.is_rec_type (dtyp_of arg)
+ if Datatype_Aux.is_rec_type (dtyp_of arg)
then Domain_Axioms.copy_of_dtyp map_tab
(proj (%:"f") eqs) (dtyp_of arg) ` (%# arg)
else (%# arg);
@@ -730,7 +730,7 @@
let
fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n";
fun one_rhs arg =
- if DatatypeAux.is_rec_type (dtyp_of arg)
+ if Datatype_Aux.is_rec_type (dtyp_of arg)
then Domain_Axioms.copy_of_dtyp map_tab
mk_take (dtyp_of arg) ` (%# arg)
else (%# arg);