# HG changeset patch # User haftmann # Date 1222186302 -7200 # Node ID 25326092cf9a15f95ff3fb8f6a91336e20ecaf19 # Parent 7c693bb763665ba6d217857e7f514d49b9c7c900 renamed rtype to typerep diff -r 7c693bb76366 -r 25326092cf9a src/HOL/Code_Eval.thy --- a/src/HOL/Code_Eval.thy Tue Sep 23 17:28:58 2008 +0200 +++ b/src/HOL/Code_Eval.thy Tue Sep 23 18:11:42 2008 +0200 @@ -16,7 +16,7 @@ datatype "term" = dummy_term definition - Const :: "message_string \ rtype \ term" + Const :: "message_string \ typerep \ term" where "Const _ _ = dummy_term" @@ -27,7 +27,7 @@ code_datatype Const App -class term_of = rtype + +class term_of = typerep + fixes term_of :: "'a \ term" lemma term_of_anything: "term_of x \ t" @@ -82,7 +82,7 @@ val ty = Type (tyco, map TFree vs); in thy - |> RType.perhaps_add_def tyco + |> Typerep.perhaps_add_def tyco |> not has_inst ? add_term_of_def ty vs tyco end; in @@ -98,7 +98,7 @@ map Free (Name.names Name.context "a" tys)); in (map_aterms (fn Free (v, ty) => Var ((v, 0), ty) | t => t) t, Eval.mk_term (fn (v, ty) => Eval.mk_term_of ty (Var ((v, 0), ty))) - (RType.mk (fn (v, sort) => RType.rtype (TFree (v, sort)))) t) + (Typerep.mk (fn (v, sort) => Typerep.typerep (TFree (v, sort)))) t) end; fun prove_term_of_eq ty eq thy = let @@ -137,13 +137,13 @@ lemmas [code func del] = term.recs term.cases term.size lemma [code func, code func del]: "(t1\term) = t2 \ t1 = t2" .. -lemma [code func, code func del]: "(term_of \ rtype \ term) = term_of" .. +lemma [code func, code func del]: "(term_of \ typerep \ term) = term_of" .. lemma [code func, code func del]: "(term_of \ term \ term) = term_of" .. lemma [code func, code func del]: "(term_of \ message_string \ term) = term_of" .. -lemma term_of_char [unfolded rtype_fun_def rtype_char_def rtype_nibble_def, code func]: "Code_Eval.term_of c = +lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code func]: "Code_Eval.term_of c = (let (n, m) = nibble_pair_of_char c - in Code_Eval.App (Code_Eval.App (Code_Eval.Const (STR ''Pair'') (RTYPE(nibble \ nibble \ char))) + in Code_Eval.App (Code_Eval.App (Code_Eval.Const (STR ''Pair'') (TYPEREP(nibble \ nibble \ char))) (Code_Eval.term_of n)) (Code_Eval.term_of m))" by (subst term_of_anything) rule diff -r 7c693bb76366 -r 25326092cf9a src/HOL/Library/Heap.thy --- a/src/HOL/Library/Heap.thy Tue Sep 23 17:28:58 2008 +0200 +++ b/src/HOL/Library/Heap.thy Tue Sep 23 18:11:42 2008 +0200 @@ -13,7 +13,7 @@ text {* The type class of representable types *} -class heap = rtype + countable +class heap = typerep + countable text {* Instances for common HOL types *} @@ -37,40 +37,40 @@ text {* Reflected types themselves are heap-representable *} -instantiation rtype :: countable +instantiation typerep :: countable begin -fun to_nat_rtype :: "rtype \ nat" where - "to_nat_rtype (RType.RType c ts) = to_nat (to_nat c, to_nat (map to_nat_rtype ts))" +fun to_nat_typerep :: "typerep \ nat" where + "to_nat_typerep (RType.Typerep c ts) = to_nat (to_nat c, to_nat (map to_nat_typerep ts))" instance proof (rule countable_classI) - fix t t' :: rtype and ts - have "(\t'. to_nat_rtype t = to_nat_rtype t' \ t = t') - \ (\ts'. map to_nat_rtype ts = map to_nat_rtype ts' \ ts = ts')" - proof (induct rule: rtype.induct) - case (RType c ts) show ?case + fix t t' :: typerep and ts + have "(\t'. to_nat_typerep t = to_nat_typerep t' \ t = t') + \ (\ts'. map to_nat_typerep ts = map to_nat_typerep ts' \ ts = ts')" + proof (induct rule: typerep.induct) + case (Typerep c ts) show ?case proof (rule allI, rule impI) fix t' - assume hyp: "to_nat_rtype (rtype.RType c ts) = to_nat_rtype t'" - then obtain c' ts' where t': "t' = (rtype.RType c' ts')" + assume hyp: "to_nat_typerep (RType.Typerep c ts) = to_nat_typerep t'" + then obtain c' ts' where t': "t' = (RType.Typerep c' ts')" by (cases t') auto - with RType hyp have "c = c'" and "ts = ts'" by simp_all - with t' show "rtype.RType c ts = t'" by simp + with Typerep hyp have "c = c'" and "ts = ts'" by simp_all + with t' show "RType.Typerep c ts = t'" by simp qed next - case Nil_rtype then show ?case by simp + case Nil_typerep then show ?case by simp next - case (Cons_rtype t ts) then show ?case by auto + case (Cons_typerep t ts) then show ?case by auto qed - then have "to_nat_rtype t = to_nat_rtype t' \ t = t'" by auto - moreover assume "to_nat_rtype t = to_nat_rtype t'" + then have "to_nat_typerep t = to_nat_typerep t' \ t = t'" by auto + moreover assume "to_nat_typerep t = to_nat_typerep t'" ultimately show "t = t'" by simp qed end -instance rtype :: heap .. +instance typerep :: heap .. subsection {* A polymorphic heap with dynamic arrays and references *} @@ -110,8 +110,8 @@ types heap_rep = nat -- "representable values" record heap = - arrays :: "rtype \ addr \ heap_rep list" - refs :: "rtype \ addr \ heap_rep" + arrays :: "typerep \ addr \ heap_rep list" + refs :: "typerep \ addr \ heap_rep" lim :: addr definition empty :: heap where @@ -145,21 +145,21 @@ definition get_ref :: "'a\heap ref \ heap \ 'a" where - "get_ref r h = from_nat (refs h (RTYPE('a)) (addr_of_ref r))" + "get_ref r h = from_nat (refs h (TYPEREP('a)) (addr_of_ref r))" definition get_array :: "'a\heap array \ heap \ 'a list" where - "get_array a h = map from_nat (arrays h (RTYPE('a)) (addr_of_array a))" + "get_array a h = map from_nat (arrays h (TYPEREP('a)) (addr_of_array a))" definition set_ref :: "'a\heap ref \ 'a \ heap \ heap" where "set_ref r x = - refs_update (\h. h( RTYPE('a) := ((h (RTYPE('a))) (addr_of_ref r:=to_nat x))))" + refs_update (\h. h(TYPEREP('a) := ((h (TYPEREP('a))) (addr_of_ref r:=to_nat x))))" definition set_array :: "'a\heap array \ 'a list \ heap \ heap" where "set_array a x = - arrays_update (\h. h( RTYPE('a) := ((h (RTYPE('a))) (addr_of_array a:=map to_nat x))))" + arrays_update (\h. h(TYPEREP('a) := ((h(TYPEREP('a))) (addr_of_array a:=map to_nat x))))" subsubsection {* Interface operations *} @@ -204,12 +204,12 @@ definition noteq_refs :: "('a\heap) ref \ ('b\heap) ref \ bool" (infix "=!=" 70) where - "r =!= s \ RTYPE('a) \ RTYPE('b) \ addr_of_ref r \ addr_of_ref s" + "r =!= s \ TYPEREP('a) \ TYPEREP('b) \ addr_of_ref r \ addr_of_ref s" definition noteq_arrs :: "('a\heap) array \ ('b\heap) array \ bool" (infix "=!!=" 70) where - "r =!!= s \ RTYPE('a) \ RTYPE('b) \ addr_of_array r \ addr_of_array s" + "r =!!= s \ TYPEREP('a) \ TYPEREP('b) \ addr_of_array r \ addr_of_array s" lemma noteq_refs_sym: "r =!= s \ s =!= r" and noteq_arrs_sym: "a =!!= b \ b =!!= a" diff -r 7c693bb76366 -r 25326092cf9a src/HOL/Library/RType.thy --- a/src/HOL/Library/RType.thy Tue Sep 23 17:28:58 2008 +0200 +++ b/src/HOL/Library/RType.thy Tue Sep 23 18:11:42 2008 +0200 @@ -9,63 +9,63 @@ imports Plain "~~/src/HOL/List" "~~/src/HOL/Library/Code_Message" begin -datatype "rtype" = RType message_string "rtype list" +datatype typerep = Typerep message_string "typerep list" -class rtype = - fixes rtype :: "'a\{} itself \ rtype" +class typerep = + fixes typerep :: "'a\{} itself \ typerep" begin definition - rtype_of :: "'a \ rtype" + typerep_of :: "'a \ typerep" where - [simp]: "rtype_of x = rtype TYPE('a)" + [simp]: "typerep_of x = typerep TYPE('a)" end setup {* let - fun rtype_tr (*"_RTYPE"*) [ty] = - Lexicon.const @{const_syntax rtype} $ (Lexicon.const "_constrain" $ Lexicon.const "TYPE" $ + fun typerep_tr (*"_TYPEREP"*) [ty] = + Lexicon.const @{const_syntax typerep} $ (Lexicon.const "_constrain" $ Lexicon.const "TYPE" $ (Lexicon.const "itself" $ ty)) - | rtype_tr (*"_RTYPE"*) ts = raise TERM ("rtype_tr", ts); - fun rtype_tr' show_sorts (*"rtype"*) + | typerep_tr (*"_TYPEREP"*) ts = raise TERM ("typerep_tr", ts); + fun typerep_tr' show_sorts (*"typerep"*) (Type ("fun", [Type ("itself", [T]), _])) (Const (@{const_syntax TYPE}, _) :: ts) = - Term.list_comb (Lexicon.const "_RTYPE" $ Syntax.term_of_typ show_sorts T, ts) - | rtype_tr' _ T ts = raise Match; + Term.list_comb (Lexicon.const "_TYPEREP" $ Syntax.term_of_typ show_sorts T, ts) + | typerep_tr' _ T ts = raise Match; in Sign.add_syntax_i - [("_RTYPE", SimpleSyntax.read_typ "type => logic", Delimfix "(1RTYPE/(1'(_')))")] - #> Sign.add_trfuns ([], [("_RTYPE", rtype_tr)], [], []) - #> Sign.add_trfunsT [(@{const_syntax rtype}, rtype_tr')] + [("_TYPEREP", SimpleSyntax.read_typ "type => logic", Delimfix "(1TYPEREP/(1'(_')))")] + #> Sign.add_trfuns ([], [("_TYPEREP", typerep_tr)], [], []) + #> Sign.add_trfunsT [(@{const_syntax typerep}, typerep_tr')] end *} ML {* -structure RType = +structure Typerep = struct fun mk f (Type (tyco, tys)) = - @{term RType} $ Message_String.mk tyco - $ HOLogic.mk_list @{typ rtype} (map (mk f) tys) + @{term Typerep} $ Message_String.mk tyco + $ HOLogic.mk_list @{typ typerep} (map (mk f) tys) | mk f (TFree v) = f v; -fun rtype ty = - Const (@{const_name rtype}, Term.itselfT ty --> @{typ rtype}) +fun typerep ty = + Const (@{const_name typerep}, Term.itselfT ty --> @{typ typerep}) $ Logic.mk_type ty; fun add_def tyco thy = let - val sorts = replicate (Sign.arity_number thy tyco) @{sort rtype}; + val sorts = replicate (Sign.arity_number thy tyco) @{sort typerep}; val vs = Name.names Name.context "'a" sorts; val ty = Type (tyco, map TFree vs); - val lhs = Const (@{const_name rtype}, Term.itselfT ty --> @{typ rtype}) + val lhs = Const (@{const_name typerep}, Term.itselfT ty --> @{typ typerep}) $ Free ("T", Term.itselfT ty); - val rhs = mk (rtype o TFree) ty; + val rhs = mk (typerep o TFree) ty; val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); in thy - |> TheoryTarget.instantiation ([tyco], vs, @{sort rtype}) + |> TheoryTarget.instantiation ([tyco], vs, @{sort typerep}) |> `(fn lthy => Syntax.check_term lthy eq) |-> (fn eq => Specification.definition (NONE, (Attrib.no_binding, eq))) |> snd @@ -76,33 +76,33 @@ fun perhaps_add_def tyco thy = let - val inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort rtype} + val inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep} in if inst then thy else add_def tyco thy end; end; *} setup {* - RType.add_def @{type_name prop} - #> RType.add_def @{type_name fun} - #> RType.add_def @{type_name itself} - #> RType.add_def @{type_name bool} - #> TypedefPackage.interpretation RType.perhaps_add_def + Typerep.add_def @{type_name prop} + #> Typerep.add_def @{type_name fun} + #> Typerep.add_def @{type_name itself} + #> Typerep.add_def @{type_name bool} + #> TypedefPackage.interpretation Typerep.perhaps_add_def *} lemma [code func]: - "RType tyco1 tys1 = RType tyco2 tys2 \ tyco1 = tyco2 + "Typerep tyco1 tys1 = Typerep tyco2 tys2 \ tyco1 = tyco2 \ list_all2 (op =) tys1 tys2" by (auto simp add: list_all2_eq [symmetric]) -code_type rtype +code_type typerep (SML "Term.typ") -code_const RType +code_const Typerep (SML "Term.Type/ (_, _)") code_reserved SML Term -hide (open) const rtype RType +hide (open) const typerep Typerep end diff -r 7c693bb76366 -r 25326092cf9a src/HOL/ex/Codegenerator.thy --- a/src/HOL/ex/Codegenerator.thy Tue Sep 23 17:28:58 2008 +0200 +++ b/src/HOL/ex/Codegenerator.thy Tue Sep 23 18:11:42 2008 +0200 @@ -14,6 +14,7 @@ nonfix upto; *} +export_code "RType.*" -- "workaround for cache problem" export_code * in SML module_name CodegenTest in OCaml module_name CodegenTest file - in Haskell file - diff -r 7c693bb76366 -r 25326092cf9a src/HOL/ex/Codegenerator_Pretty.thy --- a/src/HOL/ex/Codegenerator_Pretty.thy Tue Sep 23 17:28:58 2008 +0200 +++ b/src/HOL/ex/Codegenerator_Pretty.thy Tue Sep 23 18:11:42 2008 +0200 @@ -17,6 +17,7 @@ nonfix upto; *} +export_code "RType.*" -- "workaround for cache problem" export_code * in SML module_name CodegenTest in OCaml module_name CodegenTest file - in Haskell file - diff -r 7c693bb76366 -r 25326092cf9a src/HOL/ex/Quickcheck.thy --- a/src/HOL/ex/Quickcheck.thy Tue Sep 23 17:28:58 2008 +0200 +++ b/src/HOL/ex/Quickcheck.thy Tue Sep 23 18:11:42 2008 +0200 @@ -10,16 +10,16 @@ subsection {* The @{text random} class *} -class random = rtype + +class random = typerep + fixes random :: "index \ seed \ ('a \ (unit \ term)) \ seed" text {* Type @{typ "'a itself"} *} -instantiation itself :: ("{type, rtype}") random +instantiation itself :: ("{type, typerep}") random begin definition - "random _ = return (TYPE('a), \u. Code_Eval.Const (STR ''TYPE'') RTYPE('a))" + "random _ = return (TYPE('a), \u. Code_Eval.Const (STR ''TYPE'') TYPEREP('a))" instance .. @@ -72,7 +72,7 @@ val t_indices = map (curry ( op * ) 2) (length tys - 1 downto 0); val c_indices = map (curry ( op + ) 1) t_indices; val c_t = list_comb (c, map Bound c_indices); - val t_t = Abs ("", @{typ unit}, Eval.mk_term Free RType.rtype + val t_t = Abs ("", @{typ unit}, Eval.mk_term Free Typerep.typerep (list_comb (c, map (fn k => Bound (k + 1)) t_indices)) |> map_aterms (fn t as Bound _ => t $ @{term "()"} | t => t)); val return = StateMonad.return (term_ty this_ty) @{typ seed} @@ -173,9 +173,9 @@ "random n = (do (b, _) \ random n; (m, t) \ random n; - return (if b then (int m, \u. Code_Eval.App (Code_Eval.Const (STR ''Int.int'') RTYPE(nat \ int)) (t ())) - else (- int m, \u. Code_Eval.App (Code_Eval.Const (STR ''HOL.uminus_class.uminus'') RTYPE(int \ int)) - (Code_Eval.App (Code_Eval.Const (STR ''Int.int'') RTYPE(nat \ int)) (t ())))) + return (if b then (int m, \u. Code_Eval.App (Code_Eval.Const (STR ''Int.int'') TYPEREP(nat \ int)) (t ())) + else (- int m, \u. Code_Eval.App (Code_Eval.Const (STR ''HOL.uminus_class.uminus'') TYPEREP(int \ int)) + (Code_Eval.App (Code_Eval.Const (STR ''Int.int'') TYPEREP(nat \ int)) (t ())))) done)" instance .. @@ -219,7 +219,7 @@ *} axiomatization - random_fun_aux :: "rtype \ rtype \ ('a \ 'a \ bool) \ ('a \ term) + random_fun_aux :: "typerep \ typerep \ ('a \ 'a \ bool) \ ('a \ term) \ (seed \ ('b \ (unit \ term)) \ seed) \ (seed \ seed \ seed) \ seed \ (('a \ 'b) \ (unit \ term)) \ seed" @@ -229,7 +229,7 @@ begin definition random_fun :: "index \ seed \ (('a \ 'b) \ (unit \ term)) \ seed" where - "random n = random_fun_aux RTYPE('a) RTYPE('b) (op =) Code_Eval.term_of (random n) split_seed" + "random n = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of (random n) split_seed" instance .. diff -r 7c693bb76366 -r 25326092cf9a src/HOL/ex/Term_Of_Syntax.thy --- a/src/HOL/ex/Term_Of_Syntax.thy Tue Sep 23 17:28:58 2008 +0200 +++ b/src/HOL/ex/Term_Of_Syntax.thy Tue Sep 23 18:11:42 2008 +0200 @@ -33,7 +33,7 @@ let val subst_rterm_of = Eval.mk_term (fn (v, _) => error ("illegal free variable in term quotation: " ^ quote v)) - (RType.mk (fn (v, sort) => RType.rtype (TFree (v, sort)))); + (Typerep.mk (fn (v, sort) => Typerep.typerep (TFree (v, sort)))); fun subst_rterm_of' (Const (@{const_name rterm_of}, _), [t]) = subst_rterm_of t | subst_rterm_of' (Const (@{const_name rterm_of}, _), _) = error ("illegal number of arguments for " ^ quote @{const_name rterm_of})