# HG changeset patch # User haftmann # Date 1399616016 -7200 # Node ID 601edd9a68597365f53aea5a3fb8af4ceaf90c88 # Parent 2f94c9a50f06496947ff4439fadc573e6945833e degeneralized value command into HOL diff -r 2f94c9a50f06 -r 601edd9a6859 src/HOL/Code_Evaluation.thy --- 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" \ (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" diff -r 2f94c9a50f06 -r 601edd9a6859 src/HOL/Tools/code_evaluation.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; diff -r 2f94c9a50f06 -r 601edd9a6859 src/HOL/Tools/value.ML --- /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; diff -r 2f94c9a50f06 -r 601edd9a6859 src/Tools/Code_Generator.thy --- 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 diff -r 2f94c9a50f06 -r 601edd9a6859 src/Tools/nbe.ML --- 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; diff -r 2f94c9a50f06 -r 601edd9a6859 src/Tools/value.ML --- 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;