--- a/src/HOL/Code_Evaluation.thy Fri May 09 08:13:36 2014 +0200
+++ b/src/HOL/Code_Evaluation.thy Fri May 09 08:13:36 2014 +0200
@@ -77,8 +77,6 @@
code_reserved Eval Code_Evaluation
-setup {* Code_Evaluation.setup *}
-
subsection {* @{text term_of} instances *}
@@ -109,16 +107,9 @@
subsubsection {* Code generator setup *}
-lemmas [code del] = term.rec term.case term.size
-lemma [code, code del]: "HOL.equal (t1\<Colon>term) t2 \<longleftrightarrow> HOL.equal t1 t2" ..
-
-lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
-lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
-lemma [code, code del]: "(term_of \<Colon> String.literal \<Rightarrow> term) = term_of" ..
-lemma [code, code del]: "(Code_Evaluation.term_of \<Colon> 'a::{type, term_of} Predicate.pred \<Rightarrow> Code_Evaluation.term)
- = Code_Evaluation.term_of" ..
-lemma [code, code del]: "(Code_Evaluation.term_of \<Colon> 'a::{type, term_of} Predicate.seq \<Rightarrow> Code_Evaluation.term)
- = Code_Evaluation.term_of" ..
+declare [[code drop: rec_term case_term size_term "size :: term \<Rightarrow> _" "HOL.equal :: term \<Rightarrow> _"
+ "term_of :: typerep \<Rightarrow> _" "term_of :: term \<Rightarrow> _" "term_of :: String.literal \<Rightarrow> _"
+ "term_of :: _ Predicate.pred \<Rightarrow> term" "term_of :: _ Predicate.seq \<Rightarrow> term"]]
lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]:
"Code_Evaluation.term_of c = (case c of Char x y \<Rightarrow>
@@ -168,8 +159,7 @@
ML_file "~~/src/HOL/Tools/value.ML"
setup {*
- Value.setup
- #> Value.add_evaluator ("nbe", Nbe.dynamic_value)
+ Value.add_evaluator ("nbe", Nbe.dynamic_value)
#> Value.add_evaluator ("code", Code_Evaluation.dynamic_value_strict)
*}
--- a/src/HOL/Tools/code_evaluation.ML Fri May 09 08:13:36 2014 +0200
+++ b/src/HOL/Tools/code_evaluation.ML Fri May 09 08:13:36 2014 +0200
@@ -16,7 +16,6 @@
val static_conv: Proof.context -> string list -> typ list -> Proof.context -> conv
val put_term: (unit -> term) -> Proof.context -> Proof.context
val tracing: string -> 'a -> 'a
- val setup: theory -> theory
end;
structure Code_Evaluation : CODE_EVALUATION =
@@ -129,6 +128,15 @@
in if has_inst then add_abs_term_of_code tyco raw_vs abs ty proj thy else thy end;
+(* setup *)
+
+val _ = Context.>> (Context.map_theory
+ (Code.datatype_interpretation ensure_term_of
+ #> Code.abstype_interpretation ensure_term_of
+ #> Code.datatype_interpretation ensure_term_of_code
+ #> Code.abstype_interpretation ensure_abs_term_of_code));
+
+
(** termifying syntax **)
fun map_default f xs =
@@ -155,6 +163,8 @@
fun check_termify ctxt ts =
the_default ts (map_default subst_termify ts);
+val _ = Context.>> (Syntax_Phases.term_check 0 "termify" check_termify);
+
(** evaluation **)
@@ -220,14 +230,4 @@
fun tracing s x = (Output.tracing s; x);
-
-(** setup **)
-
-val setup =
- Code.datatype_interpretation ensure_term_of
- #> Code.abstype_interpretation ensure_term_of
- #> Code.datatype_interpretation ensure_term_of_code
- #> Code.abstype_interpretation ensure_abs_term_of_code
- #> Context.theory_map (Syntax_Phases.term_check 0 "termify" check_termify);
-
end;
--- a/src/HOL/Tools/value.ML Fri May 09 08:13:36 2014 +0200
+++ b/src/HOL/Tools/value.ML Fri May 09 08:13:36 2014 +0200
@@ -10,7 +10,6 @@
val value_select: string -> Proof.context -> term -> term
val value_cmd: string option -> string list -> string -> Toplevel.state -> unit
val add_evaluator: string * (Proof.context -> term -> term) -> theory -> theory
- val setup : theory -> theory
end;
structure Value : VALUE =
@@ -67,13 +66,11 @@
(opt_evaluator -- opt_modes -- Parse.term
>> (fn ((some_name, modes), t) => Toplevel.keep (value_cmd some_name modes t)));
-val antiq_setup =
- Thy_Output.antiquotation @{binding value}
+val _ = Context.>> (Context.map_theory
+ (Thy_Output.antiquotation @{binding value}
(Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
(fn {source, context, ...} => fn ((some_name, style), t) => Thy_Output.output context
(Thy_Output.maybe_pretty_source Thy_Output.pretty_term context source
- [style (value_maybe_select some_name context t)]));
-
-val setup = antiq_setup;
+ [style (value_maybe_select some_name context t)]))));
end;