--- a/NEWS Fri Oct 01 18:49:09 2010 +0200
+++ b/NEWS Fri Oct 01 22:44:36 2010 +0200
@@ -74,6 +74,9 @@
*** HOL ***
+* Constant `contents` renamed to `the_elem`, to free the generic name
+contents for other uses. INCOMPATIBILITY.
+
* Dropped old primrec package. INCOMPATIBILITY.
* Improved infrastructure for term evaluation using code generator
--- a/src/HOL/Algebra/AbelCoset.thy Fri Oct 01 18:49:09 2010 +0200
+++ b/src/HOL/Algebra/AbelCoset.thy Fri Oct 01 22:44:36 2010 +0200
@@ -607,20 +607,20 @@
by (rule group_hom.FactGroup_nonempty[OF a_group_hom,
folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule X)
-lemma (in abelian_group_hom) FactGroup_contents_mem:
+lemma (in abelian_group_hom) FactGroup_the_elem_mem:
assumes X: "X \<in> carrier (G A_Mod (a_kernel G H h))"
- shows "contents (h`X) \<in> carrier H"
-by (rule group_hom.FactGroup_contents_mem[OF a_group_hom,
+ shows "the_elem (h`X) \<in> carrier H"
+by (rule group_hom.FactGroup_the_elem_mem[OF a_group_hom,
folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule X)
lemma (in abelian_group_hom) A_FactGroup_hom:
- "(\<lambda>X. contents (h`X)) \<in> hom (G A_Mod (a_kernel G H h))
+ "(\<lambda>X. the_elem (h`X)) \<in> hom (G A_Mod (a_kernel G H h))
\<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr>"
by (rule group_hom.FactGroup_hom[OF a_group_hom,
folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
lemma (in abelian_group_hom) A_FactGroup_inj_on:
- "inj_on (\<lambda>X. contents (h ` X)) (carrier (G A_Mod a_kernel G H h))"
+ "inj_on (\<lambda>X. the_elem (h ` X)) (carrier (G A_Mod a_kernel G H h))"
by (rule group_hom.FactGroup_inj_on[OF a_group_hom,
folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
@@ -628,7 +628,7 @@
homomorphism from the quotient group*}
lemma (in abelian_group_hom) A_FactGroup_onto:
assumes h: "h ` carrier G = carrier H"
- shows "(\<lambda>X. contents (h ` X)) ` carrier (G A_Mod a_kernel G H h) = carrier H"
+ shows "(\<lambda>X. the_elem (h ` X)) ` carrier (G A_Mod a_kernel G H h) = carrier H"
by (rule group_hom.FactGroup_onto[OF a_group_hom,
folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule h)
@@ -636,7 +636,7 @@
quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.*}
theorem (in abelian_group_hom) A_FactGroup_iso:
"h ` carrier G = carrier H
- \<Longrightarrow> (\<lambda>X. contents (h`X)) \<in> (G A_Mod (a_kernel G H h)) \<cong>
+ \<Longrightarrow> (\<lambda>X. the_elem (h`X)) \<in> (G A_Mod (a_kernel G H h)) \<cong>
(| carrier = carrier H, mult = add H, one = zero H |)"
by (rule group_hom.FactGroup_iso[OF a_group_hom,
folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
--- a/src/HOL/Algebra/Coset.thy Fri Oct 01 18:49:09 2010 +0200
+++ b/src/HOL/Algebra/Coset.thy Fri Oct 01 22:44:36 2010 +0200
@@ -924,9 +924,9 @@
qed
-lemma (in group_hom) FactGroup_contents_mem:
+lemma (in group_hom) FactGroup_the_elem_mem:
assumes X: "X \<in> carrier (G Mod (kernel G H h))"
- shows "contents (h`X) \<in> carrier H"
+ shows "the_elem (h`X) \<in> carrier H"
proof -
from X
obtain g where g: "g \<in> carrier G"
@@ -937,8 +937,8 @@
qed
lemma (in group_hom) FactGroup_hom:
- "(\<lambda>X. contents (h`X)) \<in> hom (G Mod (kernel G H h)) H"
-apply (simp add: hom_def FactGroup_contents_mem normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)
+ "(\<lambda>X. the_elem (h`X)) \<in> hom (G Mod (kernel G H h)) H"
+apply (simp add: hom_def FactGroup_the_elem_mem normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)
proof (intro ballI)
fix X and X'
assume X: "X \<in> carrier (G Mod kernel G H h)"
@@ -955,7 +955,7 @@
by (auto dest!: FactGroup_nonempty
simp add: set_mult_def image_eq_UN
subsetD [OF Xsub] subsetD [OF X'sub])
- thus "contents (h ` (X <#> X')) = contents (h ` X) \<otimes>\<^bsub>H\<^esub> contents (h ` X')"
+ thus "the_elem (h ` (X <#> X')) = the_elem (h ` X) \<otimes>\<^bsub>H\<^esub> the_elem (h ` X')"
by (simp add: all image_eq_UN FactGroup_nonempty X X')
qed
@@ -971,7 +971,7 @@
done
lemma (in group_hom) FactGroup_inj_on:
- "inj_on (\<lambda>X. contents (h ` X)) (carrier (G Mod kernel G H h))"
+ "inj_on (\<lambda>X. the_elem (h ` X)) (carrier (G Mod kernel G H h))"
proof (simp add: inj_on_def, clarify)
fix X and X'
assume X: "X \<in> carrier (G Mod kernel G H h)"
@@ -983,7 +983,7 @@
by (auto simp add: FactGroup_def RCOSETS_def)
hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'"
by (force simp add: kernel_def r_coset_def image_def)+
- assume "contents (h ` X) = contents (h ` X')"
+ assume "the_elem (h ` X) = the_elem (h ` X')"
hence h: "h g = h g'"
by (simp add: image_eq_UN all FactGroup_nonempty X X')
show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX)
@@ -993,11 +993,11 @@
homomorphism from the quotient group*}
lemma (in group_hom) FactGroup_onto:
assumes h: "h ` carrier G = carrier H"
- shows "(\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h) = carrier H"
+ shows "(\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h) = carrier H"
proof
- show "(\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h) \<subseteq> carrier H"
- by (auto simp add: FactGroup_contents_mem)
- show "carrier H \<subseteq> (\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h)"
+ show "(\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h) \<subseteq> carrier H"
+ by (auto simp add: FactGroup_the_elem_mem)
+ show "carrier H \<subseteq> (\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h)"
proof
fix y
assume y: "y \<in> carrier H"
@@ -1005,7 +1005,7 @@
by (blast elim: equalityE)
hence "(\<Union>x\<in>kernel G H h #> g. {h x}) = {y}"
by (auto simp add: y kernel_def r_coset_def)
- with g show "y \<in> (\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h)"
+ with g show "y \<in> (\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h)"
by (auto intro!: bexI simp add: FactGroup_def RCOSETS_def image_eq_UN)
qed
qed
@@ -1015,7 +1015,7 @@
quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.*}
theorem (in group_hom) FactGroup_iso:
"h ` carrier G = carrier H
- \<Longrightarrow> (\<lambda>X. contents (h`X)) \<in> (G Mod (kernel G H h)) \<cong> H"
+ \<Longrightarrow> (\<lambda>X. the_elem (h`X)) \<in> (G Mod (kernel G H h)) \<cong> H"
by (simp add: iso_def FactGroup_hom FactGroup_inj_on bij_betw_def
FactGroup_onto)
--- a/src/HOL/Induct/QuoDataType.thy Fri Oct 01 18:49:09 2010 +0200
+++ b/src/HOL/Induct/QuoDataType.thy Fri Oct 01 22:44:36 2010 +0200
@@ -422,7 +422,7 @@
definition
discrim :: "msg \<Rightarrow> int" where
- "discrim X = contents (\<Union>U \<in> Rep_Msg X. {freediscrim U})"
+ "discrim X = the_elem (\<Union>U \<in> Rep_Msg X. {freediscrim U})"
lemma discrim_congruent: "(\<lambda>U. {freediscrim U}) respects msgrel"
by (simp add: congruent_def msgrel_imp_eq_freediscrim)
--- a/src/HOL/Induct/QuoNestedDataType.thy Fri Oct 01 18:49:09 2010 +0200
+++ b/src/HOL/Induct/QuoNestedDataType.thy Fri Oct 01 22:44:36 2010 +0200
@@ -337,7 +337,7 @@
definition
"fun" :: "exp \<Rightarrow> nat" where
- "fun X = contents (\<Union>U \<in> Rep_Exp X. {freefun U})"
+ "fun X = the_elem (\<Union>U \<in> Rep_Exp X. {freefun U})"
lemma fun_respects: "(%U. {freefun U}) respects exprel"
by (simp add: congruent_def exprel_imp_eq_freefun)
@@ -349,7 +349,7 @@
definition
args :: "exp \<Rightarrow> exp list" where
- "args X = contents (\<Union>U \<in> Rep_Exp X. {Abs_ExpList (freeargs U)})"
+ "args X = the_elem (\<Union>U \<in> Rep_Exp X. {Abs_ExpList (freeargs U)})"
text{*This result can probably be generalized to arbitrary equivalence
relations, but with little benefit here.*}
@@ -384,7 +384,7 @@
definition
discrim :: "exp \<Rightarrow> int" where
- "discrim X = contents (\<Union>U \<in> Rep_Exp X. {freediscrim U})"
+ "discrim X = the_elem (\<Union>U \<in> Rep_Exp X. {freediscrim U})"
lemma discrim_respects: "(\<lambda>U. {freediscrim U}) respects exprel"
by (simp add: congruent_def exprel_imp_eq_freediscrim)
--- a/src/HOL/Int.thy Fri Oct 01 18:49:09 2010 +0200
+++ b/src/HOL/Int.thy Fri Oct 01 22:44:36 2010 +0200
@@ -283,7 +283,7 @@
begin
definition of_int :: "int \<Rightarrow> 'a" where
- "of_int z = contents (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
+ "of_int z = the_elem (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
proof -
@@ -389,7 +389,7 @@
subsection {* Magnitude of an Integer, as a Natural Number: @{text nat} *}
definition nat :: "int \<Rightarrow> nat" where
- "nat z = contents (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
+ "nat z = the_elem (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
proof -
--- a/src/HOL/Library/Fraction_Field.thy Fri Oct 01 18:49:09 2010 +0200
+++ b/src/HOL/Library/Fraction_Field.thy Fri Oct 01 22:44:36 2010 +0200
@@ -319,7 +319,7 @@
definition
le_fract_def:
- "q \<le> r \<longleftrightarrow> contents (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r.
+ "q \<le> r \<longleftrightarrow> the_elem (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r.
{(fst x * snd y)*(snd x * snd y) \<le> (fst y * snd x)*(snd x * snd y)})"
definition
--- a/src/HOL/Probability/Lebesgue_Integration.thy Fri Oct 01 18:49:09 2010 +0200
+++ b/src/HOL/Probability/Lebesgue_Integration.thy Fri Oct 01 22:44:36 2010 +0200
@@ -495,7 +495,7 @@
lemma (in measure_space) simple_function_partition:
assumes "simple_function f" and "simple_function g"
- shows "simple_integral f = (\<Sum>A\<in>(\<lambda>x. f -` {f x} \<inter> g -` {g x} \<inter> space M) ` space M. contents (f`A) * \<mu> A)"
+ shows "simple_integral f = (\<Sum>A\<in>(\<lambda>x. f -` {f x} \<inter> g -` {g x} \<inter> space M) ` space M. the_elem (f`A) * \<mu> A)"
(is "_ = setsum _ (?p ` space M)")
proof-
let "?sub x" = "?p ` (f -` {x} \<inter> space M)"
@@ -530,18 +530,18 @@
unfolding simple_integral_def
by (subst setsum_Sigma[symmetric],
auto intro!: setsum_cong simp: setsum_right_distrib[symmetric])
- also have "\<dots> = (\<Sum>A\<in>?p ` space M. contents (f`A) * \<mu> A)"
+ also have "\<dots> = (\<Sum>A\<in>?p ` space M. the_elem (f`A) * \<mu> A)"
proof -
have [simp]: "\<And>x. x \<in> space M \<Longrightarrow> f ` ?p x = {f x}" by (auto intro!: imageI)
- have "(\<lambda>A. (contents (f ` A), A)) ` ?p ` space M
+ have "(\<lambda>A. (the_elem (f ` A), A)) ` ?p ` space M
= (\<lambda>x. (f x, ?p x)) ` space M"
proof safe
fix x assume "x \<in> space M"
- thus "(f x, ?p x) \<in> (\<lambda>A. (contents (f`A), A)) ` ?p ` space M"
+ thus "(f x, ?p x) \<in> (\<lambda>A. (the_elem (f`A), A)) ` ?p ` space M"
by (auto intro!: image_eqI[of _ _ "?p x"])
qed auto
thus ?thesis
- apply (auto intro!: setsum_reindex_cong[of "\<lambda>A. (contents (f`A), A)"] inj_onI)
+ apply (auto intro!: setsum_reindex_cong[of "\<lambda>A. (the_elem (f`A), A)"] inj_onI)
apply (rule_tac x="xa" in image_eqI)
by simp_all
qed
@@ -602,7 +602,7 @@
fix x let ?S = "g -` {g x} \<inter> f -` {f x} \<inter> space M"
assume "x \<in> space M"
hence "f ` ?S = {f x}" "g ` ?S = {g x}" by auto
- thus "contents (f`?S) * \<mu> ?S \<le> contents (g`?S) * \<mu> ?S"
+ thus "the_elem (f`?S) * \<mu> ?S \<le> the_elem (g`?S) * \<mu> ?S"
using mono[OF `x \<in> space M`] by (auto intro!: mult_right_mono)
qed
--- a/src/HOL/Rat.thy Fri Oct 01 18:49:09 2010 +0200
+++ b/src/HOL/Rat.thy Fri Oct 01 22:44:36 2010 +0200
@@ -470,7 +470,7 @@
definition
le_rat_def:
- "q \<le> r \<longleftrightarrow> contents (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
+ "q \<le> r \<longleftrightarrow> the_elem (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
{(fst x * snd y) * (snd x * snd y) \<le> (fst y * snd x) * (snd x * snd y)})"
lemma le_rat [simp]:
@@ -775,7 +775,7 @@
begin
definition of_rat :: "rat \<Rightarrow> 'a" where
- "of_rat q = contents (\<Union>(a,b) \<in> Rep_Rat q. {of_int a / of_int b})"
+ "of_rat q = the_elem (\<Union>(a,b) \<in> Rep_Rat q. {of_int a / of_int b})"
end
--- a/src/HOL/Set.thy Fri Oct 01 18:49:09 2010 +0200
+++ b/src/HOL/Set.thy Fri Oct 01 22:44:36 2010 +0200
@@ -1656,11 +1656,11 @@
subsubsection {* Getting the Contents of a Singleton Set *}
-definition contents :: "'a set \<Rightarrow> 'a" where
- "contents X = (THE x. X = {x})"
+definition the_elem :: "'a set \<Rightarrow> 'a" where
+ "the_elem X = (THE x. X = {x})"
-lemma contents_eq [simp]: "contents {x} = x"
- by (simp add: contents_def)
+lemma the_elem_eq [simp]: "the_elem {x} = x"
+ by (simp add: the_elem_def)
subsubsection {* Least value operator *}
--- a/src/HOL/Word/Misc_Numeric.thy Fri Oct 01 18:49:09 2010 +0200
+++ b/src/HOL/Word/Misc_Numeric.thy Fri Oct 01 22:44:36 2010 +0200
@@ -8,8 +8,8 @@
imports Main Parity
begin
-lemma contentsI: "y = {x} ==> contents y = x"
- unfolding contents_def by auto -- {* FIXME move *}
+lemma the_elemI: "y = {x} ==> the_elem y = x"
+ by simp
lemmas split_split = prod.split
lemmas split_split_asm = prod.split_asm
--- a/src/HOL/Word/Word.thy Fri Oct 01 18:49:09 2010 +0200
+++ b/src/HOL/Word/Word.thy Fri Oct 01 22:44:36 2010 +0200
@@ -1772,7 +1772,7 @@
lemma word_of_int: "of_int = word_of_int"
apply (rule ext)
apply (unfold of_int_def)
- apply (rule contentsI)
+ apply (rule the_elemI)
apply safe
apply (simp_all add: word_of_nat word_of_int_homs)
defer
--- a/src/HOL/ZF/Games.thy Fri Oct 01 18:49:09 2010 +0200
+++ b/src/HOL/ZF/Games.thy Fri Oct 01 22:44:36 2010 +0200
@@ -859,10 +859,10 @@
Pg_less_def: "G < H \<longleftrightarrow> G \<le> H \<and> G \<noteq> (H::Pg)"
definition
- Pg_minus_def: "- G = contents (\<Union> g \<in> Rep_Pg G. {Abs_Pg (eq_game_rel `` {neg_game g})})"
+ Pg_minus_def: "- G = the_elem (\<Union> g \<in> Rep_Pg G. {Abs_Pg (eq_game_rel `` {neg_game g})})"
definition
- Pg_plus_def: "G + H = contents (\<Union> g \<in> Rep_Pg G. \<Union> h \<in> Rep_Pg H. {Abs_Pg (eq_game_rel `` {plus_game g h})})"
+ Pg_plus_def: "G + H = the_elem (\<Union> g \<in> Rep_Pg G. \<Union> h \<in> Rep_Pg H. {Abs_Pg (eq_game_rel `` {plus_game g h})})"
definition
Pg_diff_def: "G - H = G + (- (H::Pg))"
--- a/src/HOL/ex/Dedekind_Real.thy Fri Oct 01 18:49:09 2010 +0200
+++ b/src/HOL/ex/Dedekind_Real.thy Fri Oct 01 22:44:36 2010 +0200
@@ -1183,11 +1183,11 @@
definition
real_add_def: "z + w =
- contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
+ the_elem (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
{ Abs_Real(realrel``{(x+u, y+v)}) })"
definition
- real_minus_def: "- r = contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
+ real_minus_def: "- r = the_elem (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
definition
real_diff_def: "r - (s::real) = r + - s"
@@ -1195,7 +1195,7 @@
definition
real_mult_def:
"z * w =
- contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
+ the_elem (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
{ Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })"
definition
--- a/src/Pure/ML/ml_context.ML Fri Oct 01 18:49:09 2010 +0200
+++ b/src/Pure/ML/ml_context.ML Fri Oct 01 22:44:36 2010 +0200
@@ -36,9 +36,6 @@
val eval_text_in: Proof.context option -> bool -> Position.T -> Symbol_Pos.text -> unit
val expression: Position.T -> string -> string -> ML_Lex.token Antiquote.antiquote list ->
Context.generic -> Context.generic
- val value: Proof.context ->
- (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string ->
- string * string -> 'a
end
structure ML_Context: ML_CONTEXT =
@@ -215,17 +212,6 @@
(ML_Lex.read Position.none ("Context.set_thread_data (SOME (let " ^ bind ^ " = ") @ ants @
ML_Lex.read Position.none (" in " ^ body ^ " end (ML_Context.the_generic_context ())));")));
-fun value ctxt (get, put, put_ml) (prelude, value) =
- let
- val code = (prelude
- ^ "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
- ^ " (fn () => " ^ value ^ ")) (ML_Context.the_generic_context ())))");
- val ctxt' = ctxt
- |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
- |> Context.proof_map (exec
- (fn () => Secure.use_text ML_Env.local_context (0, "value") false code));
- in get ctxt' () end;
-
end;
structure Basic_ML_Context: BASIC_ML_CONTEXT = ML_Context;
--- a/src/Tools/Code/code_runtime.ML Fri Oct 01 18:49:09 2010 +0200
+++ b/src/Tools/Code/code_runtime.ML Fri Oct 01 22:44:36 2010 +0200
@@ -7,6 +7,9 @@
signature CODE_RUNTIME =
sig
val target: string
+ val value: Proof.context ->
+ (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string ->
+ string * string -> 'a
type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string
val dynamic_value: 'a cookie -> theory -> string option
-> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a option
@@ -56,6 +59,19 @@
#> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"]));
(*avoid further pervasive infix names*)
+fun exec verbose code =
+ ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") false code);
+
+fun value ctxt (get, put, put_ml) (prelude, value) =
+ let
+ val code = (prelude
+ ^ "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
+ ^ " (fn () => " ^ value ^ ")) (ML_Context.the_generic_context ())))");
+ val ctxt' = ctxt
+ |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
+ |> Context.proof_map (exec false code);
+ in get ctxt' () end;
+
(* evaluation into target language values *)
@@ -85,7 +101,7 @@
val (program_code, [SOME value_name']) = serializer naming program' [value_name];
val value_code = space_implode " "
(value_name' :: "()" :: map (enclose "(" ")") args);
- in Exn.capture (ML_Context.value ctxt cookie) (program_code, value_code) end;
+ in Exn.capture (value ctxt cookie) (program_code, value_code) end;
fun partiality_as_none e = SOME (Exn.release e)
handle General.Match => NONE
@@ -277,20 +293,19 @@
fun add_eval_const (const, const') = Code_Target.add_const_syntax target
const (SOME (Code_Printer.simple_const_syntax (0, (K o K o K) const')));
-fun process_reflection (code_body, (tyco_map, (constr_map, const_map))) module_name NONE thy =
+fun process_reflection (code, (tyco_map, (constr_map, const_map))) module_name NONE thy =
thy
|> Code_Target.add_reserved target module_name
- |> Context.theory_map
- (ML_Context.exec (fn () => ML_Context.eval_text true Position.none code_body))
+ |> Context.theory_map (exec true code)
|> fold (add_eval_tyco o apsnd Code_Printer.str) tyco_map
|> fold (add_eval_constr o apsnd Code_Printer.str) constr_map
|> fold (add_eval_const o apsnd Code_Printer.str) const_map
- | process_reflection (code_body, _) _ (SOME file_name) thy =
+ | process_reflection (code, _) _ (SOME file_name) thy =
let
val preamble =
"(* Generated from " ^ Path.implode (Thy_Header.thy_path (Context.theory_name thy))
^ "; DO NOT EDIT! *)";
- val _ = File.write (Path.explode file_name) (preamble ^ "\n\n" ^ code_body);
+ val _ = File.write (Path.explode file_name) (preamble ^ "\n\n" ^ code);
in
thy
end;
@@ -397,9 +412,10 @@
val _ = Context.set_thread_data ((SOME o Context.Theory) thy');
val _ = Secure.use_text notifying_context
(0, Path.implode filepath) false (File.read filepath);
- val thy'' = (Context.the_theory o the) (Context.thread_data ())
- val names = Loaded_Values.get thy''
- in (names, thy'') end;
+ val thy'' = (Context.the_theory o the) (Context.thread_data ());
+ val names = Loaded_Values.get thy'';
+ val thy''' = Thy_Load.provide_file filepath thy'';
+ in (names, thy''') end;
end;
@@ -409,7 +425,8 @@
|> Specification.axiomatization [(b, SOME T, NoSyn)] []
|-> (fn ([Const (const, _)], _) =>
Code_Target.add_const_syntax target const
- (SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name))));
+ (SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))
+ #> tap (fn thy => Code_Target.produce_code thy [const] target NONE "Code" []));
fun process_file filepath (definienda, thy) =
let
--- a/src/Tools/Code_Generator.thy Fri Oct 01 18:49:09 2010 +0200
+++ b/src/Tools/Code_Generator.thy Fri Oct 01 22:44:36 2010 +0200
@@ -2,7 +2,7 @@
Author: Florian Haftmann, TU Muenchen
*)
-header {* Loading the code generator modules *}
+header {* Loading the code generator and related modules *}
theory Code_Generator
imports Pure
@@ -21,8 +21,8 @@
"~~/src/Tools/Code/code_ml.ML"
"~~/src/Tools/Code/code_haskell.ML"
"~~/src/Tools/Code/code_scala.ML"
- "~~/src/Tools/nbe.ML"
("~~/src/Tools/Code/code_runtime.ML")
+ ("~~/src/Tools/nbe.ML")
begin
setup {*
@@ -32,7 +32,6 @@
#> Code_ML.setup
#> Code_Haskell.setup
#> Code_Scala.setup
- #> Nbe.setup
#> Quickcheck.setup
*}
@@ -64,6 +63,9 @@
qed
use "~~/src/Tools/Code/code_runtime.ML"
+use "~~/src/Tools/nbe.ML"
+
+setup Nbe.setup
hide_const (open) holds
--- a/src/Tools/nbe.ML Fri Oct 01 18:49:09 2010 +0200
+++ b/src/Tools/nbe.ML Fri Oct 01 22:44:36 2010 +0200
@@ -396,7 +396,7 @@
s
|> traced (fn s => "\n--- code to be evaluated:\n" ^ s)
|> pair ""
- |> ML_Context.value ctxt univs_cookie
+ |> Code_Runtime.value ctxt univs_cookie
|> (fn f => f deps_vals)
|> (fn univs => cs ~~ univs)
end;