--- 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
@@ -6,6 +6,7 @@
theory Code_Evaluation
imports Typerep Limited_Sequence
+keywords "value" :: diag
begin
subsection {* Term representation *}
@@ -162,6 +163,17 @@
constant "tracing :: String.literal => 'a => 'a" \<rightharpoonup> (Eval) "Code'_Evaluation.tracing"
+subsection {* Interactive evaluation *}
+
+ML_file "~~/src/HOL/Tools/value.ML"
+
+setup {*
+ Value.setup
+ #> Value.add_evaluator ("nbe", Nbe.dynamic_value)
+ #> Value.add_evaluator ("code", Code_Evaluation.dynamic_value_strict)
+*}
+
+
subsection {* Generic reification *}
ML_file "~~/src/HOL/Tools/reification.ML"
--- 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
@@ -228,7 +228,6 @@
#> 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)
- #> Value.add_evaluator ("code", dynamic_value_strict);
+ #> Context.theory_map (Syntax_Phases.term_check 0 "termify" check_termify);
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/value.ML Fri May 09 08:13:36 2014 +0200
@@ -0,0 +1,79 @@
+(* Title: Tools/value.ML
+ Author: Florian Haftmann, TU Muenchen
+
+Generic value command for arbitrary evaluators.
+*)
+
+signature VALUE =
+sig
+ val value: Proof.context -> term -> term
+ 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 =
+struct
+
+structure Evaluator = Theory_Data
+(
+ type T = (string * (Proof.context -> term -> term)) list;
+ val empty = [];
+ val extend = I;
+ fun merge data : T = AList.merge (op =) (K true) data;
+)
+
+val add_evaluator = Evaluator.map o AList.update (op =);
+
+fun value_select name ctxt =
+ case AList.lookup (op =) (Evaluator.get (Proof_Context.theory_of ctxt)) name
+ of NONE => error ("No such evaluator: " ^ name)
+ | SOME f => f ctxt;
+
+fun value ctxt t = let val evaluators = Evaluator.get (Proof_Context.theory_of ctxt)
+ in if null evaluators then error "No evaluators"
+ else let val (evaluators, (_, evaluator)) = split_last evaluators
+ in case get_first (fn (_, f) => try (f ctxt) t) evaluators
+ of SOME t' => t'
+ | NONE => evaluator ctxt t
+ end end;
+
+fun value_maybe_select some_name =
+ case some_name
+ of NONE => value
+ | SOME name => value_select name;
+
+fun value_cmd some_name modes raw_t state =
+ let
+ val ctxt = Toplevel.context_of state;
+ val t = Syntax.read_term ctxt raw_t;
+ val t' = value_maybe_select some_name ctxt t;
+ val ty' = Term.type_of t';
+ val ctxt' = Variable.auto_fixes t' ctxt;
+ val p = Print_Mode.with_modes modes (fn () =>
+ Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
+ Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
+ in Pretty.writeln p end;
+
+val opt_modes =
+ Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
+
+val opt_evaluator =
+ Scan.option (@{keyword "["} |-- Parse.xname --| @{keyword "]"})
+
+val _ =
+ Outer_Syntax.improper_command @{command_spec "value"} "evaluate and print term"
+ (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}
+ (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;
+
+end;
--- a/src/Tools/Code_Generator.thy Fri May 09 08:13:36 2014 +0200
+++ b/src/Tools/Code_Generator.thy Fri May 09 08:13:36 2014 +0200
@@ -7,14 +7,13 @@
theory Code_Generator
imports Pure
keywords
- "value" "print_codeproc" "code_thms" "code_deps" :: diag and
+ "print_codeproc" "code_thms" "code_deps" :: diag and
"export_code" "code_identifier" "code_printing" "code_reserved"
"code_monad" "code_reflect" :: thy_decl and
"datatypes" "functions" "module_name" "file" "checking"
"constant" "type_constructor" "type_class" "class_relation" "class_instance" "code_module"
begin
-ML_file "~~/src/Tools/value.ML"
ML_file "~~/src/Tools/cache_io.ML"
ML_file "~~/src/Tools/Code/code_preproc.ML"
ML_file "~~/src/Tools/Code/code_symbol.ML"
@@ -28,8 +27,7 @@
ML_file "~~/src/Tools/Code/code_scala.ML"
setup {*
- Value.setup
- #> Code_Preproc.setup
+ Code_Preproc.setup
#> Code_Simp.setup
#> Code_Target.setup
#> Code_ML.setup
@@ -66,7 +64,6 @@
ML_file "~~/src/Tools/Code/code_runtime.ML"
ML_file "~~/src/Tools/nbe.ML"
-setup Nbe.setup
hide_const (open) holds
--- a/src/Tools/nbe.ML Fri May 09 08:13:36 2014 +0200
+++ b/src/Tools/nbe.ML Fri May 09 08:13:36 2014 +0200
@@ -24,7 +24,6 @@
val put_result: (unit -> Univ list -> Univ list) -> Proof.context -> Proof.context
val trace: bool Unsynchronized.ref
- val setup: theory -> theory
val add_const_alias: thm -> theory -> theory
end;
@@ -617,9 +616,4 @@
(fn program => fn _ => K (eval_term ctxt (compile true ctxt program)));
in fn ctxt' => lift_triv_classes_rew ctxt' (evaluator ctxt') end;
-
-(** setup **)
-
-val setup = Value.add_evaluator ("nbe", dynamic_value);
-
end;
--- a/src/Tools/value.ML Fri May 09 08:13:36 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,79 +0,0 @@
-(* Title: Tools/value.ML
- Author: Florian Haftmann, TU Muenchen
-
-Generic value command for arbitrary evaluators.
-*)
-
-signature VALUE =
-sig
- val value: Proof.context -> term -> term
- 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 =
-struct
-
-structure Evaluator = Theory_Data
-(
- type T = (string * (Proof.context -> term -> term)) list;
- val empty = [];
- val extend = I;
- fun merge data : T = AList.merge (op =) (K true) data;
-)
-
-val add_evaluator = Evaluator.map o AList.update (op =);
-
-fun value_select name ctxt =
- case AList.lookup (op =) (Evaluator.get (Proof_Context.theory_of ctxt)) name
- of NONE => error ("No such evaluator: " ^ name)
- | SOME f => f ctxt;
-
-fun value ctxt t = let val evaluators = Evaluator.get (Proof_Context.theory_of ctxt)
- in if null evaluators then error "No evaluators"
- else let val (evaluators, (_, evaluator)) = split_last evaluators
- in case get_first (fn (_, f) => try (f ctxt) t) evaluators
- of SOME t' => t'
- | NONE => evaluator ctxt t
- end end;
-
-fun value_maybe_select some_name =
- case some_name
- of NONE => value
- | SOME name => value_select name;
-
-fun value_cmd some_name modes raw_t state =
- let
- val ctxt = Toplevel.context_of state;
- val t = Syntax.read_term ctxt raw_t;
- val t' = value_maybe_select some_name ctxt t;
- val ty' = Term.type_of t';
- val ctxt' = Variable.auto_fixes t' ctxt;
- val p = Print_Mode.with_modes modes (fn () =>
- Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
- Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
- in Pretty.writeln p end;
-
-val opt_modes =
- Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
-
-val opt_evaluator =
- Scan.option (@{keyword "["} |-- Parse.xname --| @{keyword "]"})
-
-val _ =
- Outer_Syntax.improper_command @{command_spec "value"} "evaluate and print term"
- (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}
- (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;
-
-end;