# HG changeset patch # User huffman # Date 1290813851 28800 # Node ID 2037021f034f1cb75f7a5c8aa570bf1ab0b55e19 # Parent 72857de906215b33d115cc5f034308ffee089b6c remove map function names from domain package theory data diff -r 72857de90621 -r 2037021f034f src/HOLCF/Domain.thy --- a/src/HOLCF/Domain.thy Fri Nov 26 14:13:34 2010 -0800 +++ b/src/HOLCF/Domain.thy Fri Nov 26 15:24:11 2010 -0800 @@ -340,13 +340,13 @@ deflation_sprod_map deflation_cprod_map deflation_u_map setup {* - fold Domain_Take_Proofs.add_map_function - [(@{type_name cfun}, @{const_name cfun_map}, [true, true]), - (@{type_name "sfun"}, @{const_name sfun_map}, [true, true]), - (@{type_name ssum}, @{const_name ssum_map}, [true, true]), - (@{type_name sprod}, @{const_name sprod_map}, [true, true]), - (@{type_name prod}, @{const_name cprod_map}, [true, true]), - (@{type_name "u"}, @{const_name u_map}, [true])] + fold Domain_Take_Proofs.add_rec_type + [(@{type_name cfun}, [true, true]), + (@{type_name "sfun"}, [true, true]), + (@{type_name ssum}, [true, true]), + (@{type_name sprod}, [true, true]), + (@{type_name prod}, [true, true]), + (@{type_name "u"}, [true])] *} end diff -r 72857de90621 -r 2037021f034f src/HOLCF/Powerdomains.thy --- a/src/HOLCF/Powerdomains.thy Fri Nov 26 14:13:34 2010 -0800 +++ b/src/HOLCF/Powerdomains.thy Fri Nov 26 15:24:11 2010 -0800 @@ -42,10 +42,10 @@ deflation_upper_map deflation_lower_map deflation_convex_map setup {* - fold Domain_Take_Proofs.add_map_function - [(@{type_name "upper_pd"}, @{const_name upper_map}, [true]), - (@{type_name "lower_pd"}, @{const_name lower_map}, [true]), - (@{type_name "convex_pd"}, @{const_name convex_map}, [true])] + fold Domain_Take_Proofs.add_rec_type + [(@{type_name "upper_pd"}, [true]), + (@{type_name "lower_pd"}, [true]), + (@{type_name "convex_pd"}, [true])] *} end diff -r 72857de90621 -r 2037021f034f src/HOLCF/Tools/Domain/domain.ML --- a/src/HOLCF/Tools/Domain/domain.ML Fri Nov 26 14:13:34 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain.ML Fri Nov 26 15:24:11 2010 -0800 @@ -118,14 +118,14 @@ (* test for free type variables, illegal sort constraints on rhs, non-pcpo-types and invalid use of recursive type; replace sorts in type variables on rhs *) - val map_tab = Domain_Take_Proofs.get_map_tab thy; + val rec_tab = Domain_Take_Proofs.get_rec_tab thy; fun check_rec rec_ok (T as TFree (v,_)) = if AList.defined (op =) sorts v then T else error ("Free type variable " ^ quote v ^ " on rhs.") | check_rec rec_ok (T as Type (s, Ts)) = (case AList.lookup (op =) dtnvs' s of NONE => - let val rec_ok' = rec_ok andalso Symtab.defined map_tab s; + let val rec_ok' = rec_ok andalso Symtab.defined rec_tab s; in Type (s, map (check_rec rec_ok') Ts) end | SOME typevars => if typevars <> Ts diff -r 72857de90621 -r 2037021f034f src/HOLCF/Tools/Domain/domain_isomorphism.ML --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Nov 26 14:13:34 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Nov 26 15:24:11 2010 -0800 @@ -350,17 +350,17 @@ (Global_Theory.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes)) (conjuncts deflation_map_binds deflation_map_thm); - (* register map functions in theory data *) + (* register indirect recursion in theory data *) local - fun register_map ((dname, map_name), args) = - Domain_Take_Proofs.add_map_function (dname, map_name, args); + fun register_map (dname, args) = + Domain_Take_Proofs.add_rec_type (dname, args); val dnames = map (fst o dest_Type o fst) dom_eqns; val map_names = map (fst o dest_Const) map_consts; fun args (T, _) = case T of Type (_, Ts) => map (is_cpo thy) Ts | _ => []; val argss = map args dom_eqns; in val thy = - fold register_map (dnames ~~ map_names ~~ argss) thy; + fold register_map (dnames ~~ argss) thy; end; (* register deflation theorems *) diff -r 72857de90621 -r 2037021f034f src/HOLCF/Tools/Domain/domain_take_proofs.ML --- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML Fri Nov 26 14:13:34 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML Fri Nov 26 15:24:11 2010 -0800 @@ -55,8 +55,8 @@ val map_of_typ : theory -> (typ * term) list -> typ -> term - val add_map_function : (string * string * bool list) -> theory -> theory - val get_map_tab : theory -> (string * bool list) Symtab.table + val add_rec_type : (string * bool list) -> theory -> theory + val get_rec_tab : theory -> (bool list) Symtab.table val add_deflation_thm : thm -> theory -> theory val get_deflation_thms : theory -> thm list val map_ID_add : attribute @@ -119,12 +119,10 @@ (******************************** theory data *********************************) (******************************************************************************) -structure MapData = Theory_Data +structure Rec_Data = Theory_Data ( - (* constant names like "foo_map" *) - (* list indicates which type arguments correspond to map arguments *) - (* alternatively, which type arguments allow indirect recursion *) - type T = (string * bool list) Symtab.table; + (* list indicates which type arguments allow indirect recursion *) + type T = (bool list) Symtab.table; val empty = Symtab.empty; val extend = I; fun merge data = Symtab.merge (K true) data; @@ -142,13 +140,13 @@ val description = "theorems like foo_map$ID = ID" ); -fun add_map_function (tname, map_name, bs) = - MapData.map (Symtab.insert (K true) (tname, (map_name, bs))); +fun add_rec_type (tname, bs) = + Rec_Data.map (Symtab.insert (K true) (tname, bs)); fun add_deflation_thm thm = Context.theory_map (DeflMapData.add_thm thm); -val get_map_tab = MapData.get; +val get_rec_tab = Rec_Data.get; fun get_deflation_thms thy = DeflMapData.get (ProofContext.init_global thy); val map_ID_add = Map_Id_Data.add;