# HG changeset patch # User haftmann # Date 1259925463 -3600 # Node ID 9c7fa7f76950260f547b33a4840898c0c6a2f8f3 # Parent 74db95c74f8924f372cd4da39e66d63cf1c1c72d modernized structure Datatype_Aux diff -r 74db95c74f89 -r 9c7fa7f76950 src/HOL/Tools/Datatype/datatype_aux.ML --- 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); diff -r 74db95c74f89 -r 9c7fa7f76950 src/HOLCF/Tools/Domain/domain_axioms.ML --- 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); diff -r 74db95c74f89 -r 9c7fa7f76950 src/HOLCF/Tools/Domain/domain_extender.ML --- 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; diff -r 74db95c74f89 -r 9c7fa7f76950 src/HOLCF/Tools/Domain/domain_isomorphism.ML --- 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; diff -r 74db95c74f89 -r 9c7fa7f76950 src/HOLCF/Tools/Domain/domain_library.ML --- 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; diff -r 74db95c74f89 -r 9c7fa7f76950 src/HOLCF/Tools/Domain/domain_theorems.ML --- 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);