modernized structure Datatype_Aux
authorhaftmann
Fri Dec 04 12:17:43 2009 +0100 (2009-12-04 ago)
changeset 339719c7fa7f76950
parent 33970 74db95c74f89
child 33972 daf65be6bfe5
child 33974 01dcd9b926bf
modernized structure Datatype_Aux
src/HOL/Tools/Datatype/datatype_aux.ML
src/HOL/Tools/Datatype/datatype_data.ML
src/HOLCF/Tools/Domain/domain_axioms.ML
src/HOLCF/Tools/Domain/domain_extender.ML
src/HOLCF/Tools/Domain/domain_isomorphism.ML
src/HOLCF/Tools/Domain/domain_library.ML
src/HOLCF/Tools/Domain/domain_theorems.ML
     1.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Wed Dec 02 11:29:49 2009 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Dec 04 12:17:43 2009 +0100
     1.3 @@ -374,7 +374,7 @@
     1.4            then NONE
     1.5            else Option.map (Integer.add 1 o snd) (find_nonempty descr (i::is) i)
     1.6        | arg_nonempty _ = SOME 0;
     1.7 -    fun max_inf (SOME i) (SOME j) = Integer.max i j
     1.8 +    fun max_inf (SOME i) (SOME j) = SOME (Integer.max i j)
     1.9        | max_inf _ _ = NONE;
    1.10      fun max xs = fold max_inf xs (SOME 0);
    1.11      val (_, _, constrs) = the (AList.lookup (op =) descr i);
     2.1 --- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Wed Dec 02 11:29:49 2009 +0100
     2.2 +++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Fri Dec 04 12:17:43 2009 +0100
     2.3 @@ -38,10 +38,10 @@
     2.4                   (@{type_name "u"}, @{const_name "u_map"})];
     2.5  
     2.6  fun copy_of_dtyp tab r dt =
     2.7 -    if DatatypeAux.is_rec_type dt then copy tab r dt else ID
     2.8 -and copy tab r (DatatypeAux.DtRec i) = r i
     2.9 -  | copy tab r (DatatypeAux.DtTFree a) = ID
    2.10 -  | copy tab r (DatatypeAux.DtType (c, ds)) =
    2.11 +    if Datatype_Aux.is_rec_type dt then copy tab r dt else ID
    2.12 +and copy tab r (Datatype_Aux.DtRec i) = r i
    2.13 +  | copy tab r (Datatype_Aux.DtTFree a) = ID
    2.14 +  | copy tab r (Datatype_Aux.DtType (c, ds)) =
    2.15      case Symtab.lookup tab c of
    2.16        SOME f => list_ccomb (%%:f, map (copy_of_dtyp tab r) ds)
    2.17      | NONE => (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID);
     3.1 --- a/src/HOLCF/Tools/Domain/domain_extender.ML	Wed Dec 02 11:29:49 2009 +0100
     3.2 +++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Fri Dec 04 12:17:43 2009 +0100
     3.3 @@ -162,7 +162,7 @@
     3.4      fun one_con (con,args,mx) =
     3.5          ((Syntax.const_name mx (Binding.name_of con)),
     3.6           ListPair.map (fn ((lazy,sel,tp),vn) =>
     3.7 -           mk_arg ((lazy, DatatypeAux.dtyp_of_typ new_dts tp),
     3.8 +           mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp),
     3.9                     Option.map Binding.name_of sel,vn))
    3.10                        (args,(mk_var_names(map (typid o third) args)))
    3.11          ) : cons;
    3.12 @@ -237,7 +237,7 @@
    3.13      fun one_con (con,args,mx) =
    3.14          ((Syntax.const_name mx (Binding.name_of con)),
    3.15           ListPair.map (fn ((lazy,sel,tp),vn) =>
    3.16 -           mk_arg ((lazy, DatatypeAux.dtyp_of_typ new_dts tp),
    3.17 +           mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp),
    3.18                     Option.map Binding.name_of sel,vn))
    3.19                        (args,(mk_var_names(map (typid o third) args)))
    3.20          ) : cons;
     4.1 --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Wed Dec 02 11:29:49 2009 +0100
     4.2 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Fri Dec 04 12:17:43 2009 +0100
     4.3 @@ -581,12 +581,12 @@
     4.4                  mk_fst t :: mk_copy_args xs (mk_snd t);
     4.5        in mk_copy_args doms copy_arg end;
     4.6      fun copy_of_dtyp (T, dt) =
     4.7 -        if DatatypeAux.is_rec_type dt
     4.8 +        if Datatype_Aux.is_rec_type dt
     4.9          then copy_of_dtyp' (T, dt)
    4.10          else ID_const T
    4.11 -    and copy_of_dtyp' (T, DatatypeAux.DtRec i) = nth copy_args i
    4.12 -      | copy_of_dtyp' (T, DatatypeAux.DtTFree a) = ID_const T
    4.13 -      | copy_of_dtyp' (T as Type (_, Ts), DatatypeAux.DtType (c, ds)) =
    4.14 +    and copy_of_dtyp' (T, Datatype_Aux.DtRec i) = nth copy_args i
    4.15 +      | copy_of_dtyp' (T, Datatype_Aux.DtTFree a) = ID_const T
    4.16 +      | copy_of_dtyp' (T as Type (_, Ts), Datatype_Aux.DtType (c, ds)) =
    4.17          case Symtab.lookup map_tab' c of
    4.18            SOME f =>
    4.19            Library.foldl mk_capply
    4.20 @@ -599,7 +599,7 @@
    4.21          val copy_bind = Binding.suffix_name "_copy" tbind;
    4.22          val (copy_const, thy) = thy |>
    4.23            Sign.declare_const ((copy_bind, copy_type), NoSyn);
    4.24 -        val dtyp = DatatypeAux.dtyp_of_typ new_dts rhsT;
    4.25 +        val dtyp = Datatype_Aux.dtyp_of_typ new_dts rhsT;
    4.26          val body = copy_of_dtyp (rhsT, dtyp);
    4.27          val comp = mk_cfcomp (abs_const, mk_cfcomp (body, rep_const));
    4.28          val rhs = big_lambda copy_arg comp;
     5.1 --- a/src/HOLCF/Tools/Domain/domain_library.ML	Wed Dec 02 11:29:49 2009 +0100
     5.2 +++ b/src/HOLCF/Tools/Domain/domain_library.ML	Fri Dec 04 12:17:43 2009 +0100
     5.3 @@ -230,7 +230,7 @@
     5.4  val mk_arg = I;
     5.5  
     5.6  fun rec_of ((_,dtyp),_,_) =
     5.7 -    case dtyp of DatatypeAux.DtRec i => i | _ => ~1;
     5.8 +    case dtyp of Datatype_Aux.DtRec i => i | _ => ~1;
     5.9  (* FIXME: what about indirect recursion? *)
    5.10  
    5.11  fun is_lazy arg = fst (first arg);
    5.12 @@ -246,12 +246,12 @@
    5.13  
    5.14  (* ----- combinators for making dtyps ----- *)
    5.15  
    5.16 -fun mk_uD T = DatatypeAux.DtType(@{type_name "u"}, [T]);
    5.17 -fun mk_sprodD (T, U) = DatatypeAux.DtType(@{type_name "**"}, [T, U]);
    5.18 -fun mk_ssumD (T, U) = DatatypeAux.DtType(@{type_name "++"}, [T, U]);
    5.19 -fun mk_liftD T = DatatypeAux.DtType(@{type_name "lift"}, [T]);
    5.20 -val unitD = DatatypeAux.DtType(@{type_name "unit"}, []);
    5.21 -val boolD = DatatypeAux.DtType(@{type_name "bool"}, []);
    5.22 +fun mk_uD T = Datatype_Aux.DtType(@{type_name "u"}, [T]);
    5.23 +fun mk_sprodD (T, U) = Datatype_Aux.DtType(@{type_name "**"}, [T, U]);
    5.24 +fun mk_ssumD (T, U) = Datatype_Aux.DtType(@{type_name "++"}, [T, U]);
    5.25 +fun mk_liftD T = Datatype_Aux.DtType(@{type_name "lift"}, [T]);
    5.26 +val unitD = Datatype_Aux.DtType(@{type_name "unit"}, []);
    5.27 +val boolD = Datatype_Aux.DtType(@{type_name "bool"}, []);
    5.28  val oneD = mk_liftD unitD;
    5.29  val trD = mk_liftD boolD;
    5.30  fun big_sprodD ds = case ds of [] => oneD | _ => foldr1 mk_sprodD ds;
     6.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Wed Dec 02 11:29:49 2009 +0100
     6.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Dec 04 12:17:43 2009 +0100
     6.3 @@ -600,7 +600,7 @@
     6.4      let
     6.5        val lhs = dc_copy`%"f"`(con_app con args);
     6.6        fun one_rhs arg =
     6.7 -          if DatatypeAux.is_rec_type (dtyp_of arg)
     6.8 +          if Datatype_Aux.is_rec_type (dtyp_of arg)
     6.9            then Domain_Axioms.copy_of_dtyp map_tab
    6.10                   (proj (%:"f") eqs) (dtyp_of arg) ` (%# arg)
    6.11            else (%# arg);
    6.12 @@ -730,7 +730,7 @@
    6.13          let
    6.14            fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n";
    6.15            fun one_rhs arg =
    6.16 -              if DatatypeAux.is_rec_type (dtyp_of arg)
    6.17 +              if Datatype_Aux.is_rec_type (dtyp_of arg)
    6.18                then Domain_Axioms.copy_of_dtyp map_tab
    6.19                       mk_take (dtyp_of arg) ` (%# arg)
    6.20                else (%# arg);