--- 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 \<Rightarrow> rtype \<Rightarrow> term"
+ Const :: "message_string \<Rightarrow> typerep \<Rightarrow> 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 \<Rightarrow> term"
lemma term_of_anything: "term_of x \<equiv> 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\<Colon>term) = t2 \<longleftrightarrow> t1 = t2" ..
-lemma [code func, code func del]: "(term_of \<Colon> rtype \<Rightarrow> term) = term_of" ..
+lemma [code func, code func del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
lemma [code func, code func del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
lemma [code func, code func del]: "(term_of \<Colon> message_string \<Rightarrow> 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 \<Rightarrow> nibble \<Rightarrow> char)))
+ in Code_Eval.App (Code_Eval.App (Code_Eval.Const (STR ''Pair'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
(Code_Eval.term_of n)) (Code_Eval.term_of m))"
by (subst term_of_anything) rule
--- 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 \<Rightarrow> 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 \<Rightarrow> 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 "(\<forall>t'. to_nat_rtype t = to_nat_rtype t' \<longrightarrow> t = t')
- \<and> (\<forall>ts'. map to_nat_rtype ts = map to_nat_rtype ts' \<longrightarrow> ts = ts')"
- proof (induct rule: rtype.induct)
- case (RType c ts) show ?case
+ fix t t' :: typerep and ts
+ have "(\<forall>t'. to_nat_typerep t = to_nat_typerep t' \<longrightarrow> t = t')
+ \<and> (\<forall>ts'. map to_nat_typerep ts = map to_nat_typerep ts' \<longrightarrow> 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' \<Longrightarrow> t = t'" by auto
- moreover assume "to_nat_rtype t = to_nat_rtype t'"
+ then have "to_nat_typerep t = to_nat_typerep t' \<Longrightarrow> 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 \<Rightarrow> addr \<Rightarrow> heap_rep list"
- refs :: "rtype \<Rightarrow> addr \<Rightarrow> heap_rep"
+ arrays :: "typerep \<Rightarrow> addr \<Rightarrow> heap_rep list"
+ refs :: "typerep \<Rightarrow> addr \<Rightarrow> heap_rep"
lim :: addr
definition empty :: heap where
@@ -145,21 +145,21 @@
definition
get_ref :: "'a\<Colon>heap ref \<Rightarrow> heap \<Rightarrow> '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\<Colon>heap array \<Rightarrow> heap \<Rightarrow> '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\<Colon>heap ref \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where
"set_ref r x =
- refs_update (\<lambda>h. h( RTYPE('a) := ((h (RTYPE('a))) (addr_of_ref r:=to_nat x))))"
+ refs_update (\<lambda>h. h(TYPEREP('a) := ((h (TYPEREP('a))) (addr_of_ref r:=to_nat x))))"
definition
set_array :: "'a\<Colon>heap array \<Rightarrow> 'a list \<Rightarrow> heap \<Rightarrow> heap" where
"set_array a x =
- arrays_update (\<lambda>h. h( RTYPE('a) := ((h (RTYPE('a))) (addr_of_array a:=map to_nat x))))"
+ arrays_update (\<lambda>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\<Colon>heap) ref \<Rightarrow> ('b\<Colon>heap) ref \<Rightarrow> bool" (infix "=!=" 70)
where
- "r =!= s \<longleftrightarrow> RTYPE('a) \<noteq> RTYPE('b) \<or> addr_of_ref r \<noteq> addr_of_ref s"
+ "r =!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_ref r \<noteq> addr_of_ref s"
definition
noteq_arrs :: "('a\<Colon>heap) array \<Rightarrow> ('b\<Colon>heap) array \<Rightarrow> bool" (infix "=!!=" 70)
where
- "r =!!= s \<longleftrightarrow> RTYPE('a) \<noteq> RTYPE('b) \<or> addr_of_array r \<noteq> addr_of_array s"
+ "r =!!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_array r \<noteq> addr_of_array s"
lemma noteq_refs_sym: "r =!= s \<Longrightarrow> s =!= r"
and noteq_arrs_sym: "a =!!= b \<Longrightarrow> b =!!= a"
--- 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\<Colon>{} itself \<Rightarrow> rtype"
+class typerep =
+ fixes typerep :: "'a\<Colon>{} itself \<Rightarrow> typerep"
begin
definition
- rtype_of :: "'a \<Rightarrow> rtype"
+ typerep_of :: "'a \<Rightarrow> 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 \<longleftrightarrow> tyco1 = tyco2
+ "Typerep tyco1 tys1 = Typerep tyco2 tys2 \<longleftrightarrow> tyco1 = tyco2
\<and> 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
--- 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 -
--- 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 -
--- 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 \<Rightarrow> seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> seed"
text {* Type @{typ "'a itself"} *}
-instantiation itself :: ("{type, rtype}") random
+instantiation itself :: ("{type, typerep}") random
begin
definition
- "random _ = return (TYPE('a), \<lambda>u. Code_Eval.Const (STR ''TYPE'') RTYPE('a))"
+ "random _ = return (TYPE('a), \<lambda>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, _) \<leftarrow> random n;
(m, t) \<leftarrow> random n;
- return (if b then (int m, \<lambda>u. Code_Eval.App (Code_Eval.Const (STR ''Int.int'') RTYPE(nat \<Rightarrow> int)) (t ()))
- else (- int m, \<lambda>u. Code_Eval.App (Code_Eval.Const (STR ''HOL.uminus_class.uminus'') RTYPE(int \<Rightarrow> int))
- (Code_Eval.App (Code_Eval.Const (STR ''Int.int'') RTYPE(nat \<Rightarrow> int)) (t ()))))
+ return (if b then (int m, \<lambda>u. Code_Eval.App (Code_Eval.Const (STR ''Int.int'') TYPEREP(nat \<Rightarrow> int)) (t ()))
+ else (- int m, \<lambda>u. Code_Eval.App (Code_Eval.Const (STR ''HOL.uminus_class.uminus'') TYPEREP(int \<Rightarrow> int))
+ (Code_Eval.App (Code_Eval.Const (STR ''Int.int'') TYPEREP(nat \<Rightarrow> int)) (t ()))))
done)"
instance ..
@@ -219,7 +219,7 @@
*}
axiomatization
- random_fun_aux :: "rtype \<Rightarrow> rtype \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term)
+ random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term)
\<Rightarrow> (seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> seed) \<Rightarrow> (seed \<Rightarrow> seed \<times> seed)
\<Rightarrow> seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> seed"
@@ -229,7 +229,7 @@
begin
definition random_fun :: "index \<Rightarrow> seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> 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 ..
--- 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})