remove copy_of_dtyp from domain_axioms.ML
authorhuffman
Wed Mar 03 08:14:56 2010 -0800 (2010-03-03)
changeset 35559119653afcd6e
parent 35558 bb088a6fafbc
child 35560 d607ea103dcb
remove copy_of_dtyp from domain_axioms.ML
src/HOLCF/Tools/Domain/domain_axioms.ML
src/HOLCF/Tools/Domain/domain_theorems.ML
     1.1 --- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Wed Mar 03 07:55:52 2010 -0800
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Wed Mar 03 08:14:56 2010 -0800
     1.3 @@ -14,9 +14,6 @@
     1.4    val axiomatize_lub_take :
     1.5        binding * term -> theory -> thm * theory
     1.6  
     1.7 -  val copy_of_dtyp :
     1.8 -      string Symtab.table -> (int -> term) -> Datatype.dtyp -> term
     1.9 -
    1.10    val add_axioms :
    1.11        (binding * (typ * typ)) list -> theory ->
    1.12        Domain_Take_Proofs.iso_info list * theory
    1.13 @@ -26,32 +23,6 @@
    1.14  structure Domain_Axioms : DOMAIN_AXIOMS =
    1.15  struct
    1.16  
    1.17 -(* TODO: move copy_of_dtyp somewhere else! *)
    1.18 -local open Domain_Library in
    1.19 -
    1.20 -infixr 0 ===>;infixr 0 ==>;infix 0 == ; 
    1.21 -infix 1 ===; infix 1 ~= ; infix 1 <<; infix 1 ~<<;
    1.22 -infix 9 `   ; infix 9 `% ; infix 9 `%%; infixr 9 oo;
    1.23 -
    1.24 -(* FIXME: use theory data for this *)
    1.25 -val copy_tab : string Symtab.table =
    1.26 -    Symtab.make [(@{type_name cfun}, @{const_name "cfun_map"}),
    1.27 -                 (@{type_name ssum}, @{const_name "ssum_map"}),
    1.28 -                 (@{type_name sprod}, @{const_name "sprod_map"}),
    1.29 -                 (@{type_name "*"}, @{const_name "cprod_map"}),
    1.30 -                 (@{type_name "u"}, @{const_name "u_map"})];
    1.31 -
    1.32 -fun copy_of_dtyp tab r dt =
    1.33 -    if Datatype_Aux.is_rec_type dt then copy tab r dt else ID
    1.34 -and copy tab r (Datatype_Aux.DtRec i) = r i
    1.35 -  | copy tab r (Datatype_Aux.DtTFree a) = ID
    1.36 -  | copy tab r (Datatype_Aux.DtType (c, ds)) =
    1.37 -    case Symtab.lookup tab c of
    1.38 -      SOME f => list_ccomb (%%:f, map (copy_of_dtyp tab r) ds)
    1.39 -    | NONE => (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID);
    1.40 -
    1.41 -end; (* local open *)
    1.42 -
    1.43  open HOLCF_Library;
    1.44  
    1.45  fun axiomatize_isomorphism
     2.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Wed Mar 03 07:55:52 2010 -0800
     2.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Wed Mar 03 08:14:56 2010 -0800
     2.3 @@ -160,12 +160,21 @@
     2.4    fun get_deflation_take dn = PureThy.get_thm thy (dn ^ ".deflation_take");
     2.5    val axs_deflation_take = map get_deflation_take dnames;
     2.6  
     2.7 +  fun copy_of_dtyp tab r dt =
     2.8 +      if Datatype_Aux.is_rec_type dt then copy tab r dt else ID
     2.9 +  and copy tab r (Datatype_Aux.DtRec i) = r i
    2.10 +    | copy tab r (Datatype_Aux.DtTFree a) = ID
    2.11 +    | copy tab r (Datatype_Aux.DtType (c, ds)) =
    2.12 +      case Symtab.lookup tab c of
    2.13 +        SOME f => list_ccomb (%%:f, map (copy_of_dtyp tab r) ds)
    2.14 +      | NONE => (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID);
    2.15 +
    2.16    fun one_take_app (con, args) =
    2.17      let
    2.18        fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n";
    2.19        fun one_rhs arg =
    2.20            if Datatype_Aux.is_rec_type (dtyp_of arg)
    2.21 -          then Domain_Axioms.copy_of_dtyp map_tab
    2.22 +          then copy_of_dtyp map_tab
    2.23                   mk_take (dtyp_of arg) ` (%# arg)
    2.24            else (%# arg);
    2.25        val lhs = (dc_take dname $ (%%:"Suc" $ %:"n"))`(con_app con args);