# HG changeset patch # User haftmann # Date 1285965876 -7200 # Node ID 721ba2c1a79917f23f00ad8bd87c4cb3b0605354 # Parent b93f273581001de39c00bc0c45767d78dcb3d98d# Parent 2ffe7060ca75ec3c416025f286ee878ad00a83ae merged diff -r b93f27358100 -r 721ba2c1a799 NEWS --- 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 diff -r b93f27358100 -r 721ba2c1a799 src/HOL/Algebra/AbelCoset.thy --- 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 \ carrier (G A_Mod (a_kernel G H h))" - shows "contents (h`X) \ carrier H" -by (rule group_hom.FactGroup_contents_mem[OF a_group_hom, + shows "the_elem (h`X) \ 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: - "(\X. contents (h`X)) \ hom (G A_Mod (a_kernel G H h)) + "(\X. the_elem (h`X)) \ hom (G A_Mod (a_kernel G H h)) \carrier = carrier H, mult = add H, one = zero H\" 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 (\X. contents (h ` X)) (carrier (G A_Mod a_kernel G H h))" + "inj_on (\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 "(\X. contents (h ` X)) ` carrier (G A_Mod a_kernel G H h) = carrier H" + shows "(\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 - \ (\X. contents (h`X)) \ (G A_Mod (a_kernel G H h)) \ + \ (\X. the_elem (h`X)) \ (G A_Mod (a_kernel G H h)) \ (| 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]) diff -r b93f27358100 -r 721ba2c1a799 src/HOL/Algebra/Coset.thy --- 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 \ carrier (G Mod (kernel G H h))" - shows "contents (h`X) \ carrier H" + shows "the_elem (h`X) \ carrier H" proof - from X obtain g where g: "g \ carrier G" @@ -937,8 +937,8 @@ qed lemma (in group_hom) FactGroup_hom: - "(\X. contents (h`X)) \ 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) + "(\X. the_elem (h`X)) \ 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 \ 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) \\<^bsub>H\<^esub> contents (h ` X')" + thus "the_elem (h ` (X <#> X')) = the_elem (h ` X) \\<^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 (\X. contents (h ` X)) (carrier (G Mod kernel G H h))" + "inj_on (\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 \ carrier (G Mod kernel G H h)" @@ -983,7 +983,7 @@ by (auto simp add: FactGroup_def RCOSETS_def) hence all: "\x\X. h x = h g" "\x\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 "(\X. contents (h ` X)) ` carrier (G Mod kernel G H h) = carrier H" + shows "(\X. the_elem (h ` X)) ` carrier (G Mod kernel G H h) = carrier H" proof - show "(\X. contents (h ` X)) ` carrier (G Mod kernel G H h) \ carrier H" - by (auto simp add: FactGroup_contents_mem) - show "carrier H \ (\X. contents (h ` X)) ` carrier (G Mod kernel G H h)" + show "(\X. the_elem (h ` X)) ` carrier (G Mod kernel G H h) \ carrier H" + by (auto simp add: FactGroup_the_elem_mem) + show "carrier H \ (\X. the_elem (h ` X)) ` carrier (G Mod kernel G H h)" proof fix y assume y: "y \ carrier H" @@ -1005,7 +1005,7 @@ by (blast elim: equalityE) hence "(\x\kernel G H h #> g. {h x}) = {y}" by (auto simp add: y kernel_def r_coset_def) - with g show "y \ (\X. contents (h ` X)) ` carrier (G Mod kernel G H h)" + with g show "y \ (\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 - \ (\X. contents (h`X)) \ (G Mod (kernel G H h)) \ H" + \ (\X. the_elem (h`X)) \ (G Mod (kernel G H h)) \ H" by (simp add: iso_def FactGroup_hom FactGroup_inj_on bij_betw_def FactGroup_onto) diff -r b93f27358100 -r 721ba2c1a799 src/HOL/Induct/QuoDataType.thy --- 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 \ int" where - "discrim X = contents (\U \ Rep_Msg X. {freediscrim U})" + "discrim X = the_elem (\U \ Rep_Msg X. {freediscrim U})" lemma discrim_congruent: "(\U. {freediscrim U}) respects msgrel" by (simp add: congruent_def msgrel_imp_eq_freediscrim) diff -r b93f27358100 -r 721ba2c1a799 src/HOL/Induct/QuoNestedDataType.thy --- 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 \ nat" where - "fun X = contents (\U \ Rep_Exp X. {freefun U})" + "fun X = the_elem (\U \ 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 \ exp list" where - "args X = contents (\U \ Rep_Exp X. {Abs_ExpList (freeargs U)})" + "args X = the_elem (\U \ 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 \ int" where - "discrim X = contents (\U \ Rep_Exp X. {freediscrim U})" + "discrim X = the_elem (\U \ Rep_Exp X. {freediscrim U})" lemma discrim_respects: "(\U. {freediscrim U}) respects exprel" by (simp add: congruent_def exprel_imp_eq_freediscrim) diff -r b93f27358100 -r 721ba2c1a799 src/HOL/Int.thy --- 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 \ 'a" where - "of_int z = contents (\(i, j) \ Rep_Integ z. { of_nat i - of_nat j })" + "of_int z = the_elem (\(i, j) \ 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 \ nat" where - "nat z = contents (\(x, y) \ Rep_Integ z. {x-y})" + "nat z = the_elem (\(x, y) \ Rep_Integ z. {x-y})" lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y" proof - diff -r b93f27358100 -r 721ba2c1a799 src/HOL/Library/Fraction_Field.thy --- 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 \ r \ contents (\x \ Rep_fract q. \y \ Rep_fract r. + "q \ r \ the_elem (\x \ Rep_fract q. \y \ Rep_fract r. {(fst x * snd y)*(snd x * snd y) \ (fst y * snd x)*(snd x * snd y)})" definition diff -r b93f27358100 -r 721ba2c1a799 src/HOL/Probability/Lebesgue_Integration.thy --- 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 = (\A\(\x. f -` {f x} \ g -` {g x} \ space M) ` space M. contents (f`A) * \ A)" + shows "simple_integral f = (\A\(\x. f -` {f x} \ g -` {g x} \ space M) ` space M. the_elem (f`A) * \ A)" (is "_ = setsum _ (?p ` space M)") proof- let "?sub x" = "?p ` (f -` {x} \ 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 "\ = (\A\?p ` space M. contents (f`A) * \ A)" + also have "\ = (\A\?p ` space M. the_elem (f`A) * \ A)" proof - have [simp]: "\x. x \ space M \ f ` ?p x = {f x}" by (auto intro!: imageI) - have "(\A. (contents (f ` A), A)) ` ?p ` space M + have "(\A. (the_elem (f ` A), A)) ` ?p ` space M = (\x. (f x, ?p x)) ` space M" proof safe fix x assume "x \ space M" - thus "(f x, ?p x) \ (\A. (contents (f`A), A)) ` ?p ` space M" + thus "(f x, ?p x) \ (\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 "\A. (contents (f`A), A)"] inj_onI) + apply (auto intro!: setsum_reindex_cong[of "\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} \ f -` {f x} \ space M" assume "x \ space M" hence "f ` ?S = {f x}" "g ` ?S = {g x}" by auto - thus "contents (f`?S) * \ ?S \ contents (g`?S) * \ ?S" + thus "the_elem (f`?S) * \ ?S \ the_elem (g`?S) * \ ?S" using mono[OF `x \ space M`] by (auto intro!: mult_right_mono) qed diff -r b93f27358100 -r 721ba2c1a799 src/HOL/Rat.thy --- 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 \ r \ contents (\x \ Rep_Rat q. \y \ Rep_Rat r. + "q \ r \ the_elem (\x \ Rep_Rat q. \y \ Rep_Rat r. {(fst x * snd y) * (snd x * snd y) \ (fst y * snd x) * (snd x * snd y)})" lemma le_rat [simp]: @@ -775,7 +775,7 @@ begin definition of_rat :: "rat \ 'a" where - "of_rat q = contents (\(a,b) \ Rep_Rat q. {of_int a / of_int b})" + "of_rat q = the_elem (\(a,b) \ Rep_Rat q. {of_int a / of_int b})" end diff -r b93f27358100 -r 721ba2c1a799 src/HOL/Set.thy --- 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 \ 'a" where - "contents X = (THE x. X = {x})" +definition the_elem :: "'a set \ '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 *} diff -r b93f27358100 -r 721ba2c1a799 src/HOL/Word/Misc_Numeric.thy --- 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 diff -r b93f27358100 -r 721ba2c1a799 src/HOL/Word/Word.thy --- 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 diff -r b93f27358100 -r 721ba2c1a799 src/HOL/ZF/Games.thy --- 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 \ G \ H \ G \ (H::Pg)" definition - Pg_minus_def: "- G = contents (\ g \ Rep_Pg G. {Abs_Pg (eq_game_rel `` {neg_game g})})" + Pg_minus_def: "- G = the_elem (\ g \ Rep_Pg G. {Abs_Pg (eq_game_rel `` {neg_game g})})" definition - Pg_plus_def: "G + H = contents (\ g \ Rep_Pg G. \ h \ Rep_Pg H. {Abs_Pg (eq_game_rel `` {plus_game g h})})" + Pg_plus_def: "G + H = the_elem (\ g \ Rep_Pg G. \ h \ Rep_Pg H. {Abs_Pg (eq_game_rel `` {plus_game g h})})" definition Pg_diff_def: "G - H = G + (- (H::Pg))" diff -r b93f27358100 -r 721ba2c1a799 src/HOL/ex/Dedekind_Real.thy --- 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 (\(x,y) \ Rep_Real(z). \(u,v) \ Rep_Real(w). + the_elem (\(x,y) \ Rep_Real(z). \(u,v) \ Rep_Real(w). { Abs_Real(realrel``{(x+u, y+v)}) })" definition - real_minus_def: "- r = contents (\(x,y) \ Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })" + real_minus_def: "- r = the_elem (\(x,y) \ 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 (\(x,y) \ Rep_Real(z). \(u,v) \ Rep_Real(w). + the_elem (\(x,y) \ Rep_Real(z). \(u,v) \ Rep_Real(w). { Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })" definition diff -r b93f27358100 -r 721ba2c1a799 src/Pure/ML/ml_context.ML --- 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; diff -r b93f27358100 -r 721ba2c1a799 src/Tools/Code/code_runtime.ML --- 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 diff -r b93f27358100 -r 721ba2c1a799 src/Tools/Code_Generator.thy --- 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 diff -r b93f27358100 -r 721ba2c1a799 src/Tools/nbe.ML --- 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;