--- a/NEWS Mon Sep 15 20:51:58 2008 +0200
+++ b/NEWS Tue Sep 16 09:21:22 2008 +0200
@@ -63,6 +63,11 @@
*** HOL ***
+* HOL/Main: command "value" now integrates different evaluation mechanisms.
+The result of the first successful evaluation mechanism is printed.
+In square brackets a particular named evaluation mechanisms may be specified
+(currently, [SML], [code] or [nbe]). See further HOL/ex/Eval_Examples.thy.
+
* HOL/Orderings: class "wellorder" moved here, with explicit induction
rule "less_induct" as assumption. For instantiation of "wellorder" by
means of predicate "wf", use rule wf_wellorderI. INCOMPATIBILITY.
--- a/src/HOL/HOL.thy Mon Sep 15 20:51:58 2008 +0200
+++ b/src/HOL/HOL.thy Tue Sep 16 09:21:22 2008 +0200
@@ -1711,6 +1711,7 @@
#> Code_ML.setup
#> Code_Haskell.setup
#> Nbe.setup
+ #> Codegen.setup
*}
lemma [code func]:
--- a/src/HOL/IsaMakefile Mon Sep 15 20:51:58 2008 +0200
+++ b/src/HOL/IsaMakefile Tue Sep 16 09:21:22 2008 +0200
@@ -184,6 +184,7 @@
ROOT.ML \
Arith_Tools.thy \
ATP_Linkup.thy \
+ Code_Eval.thy \
Complex/Complex_Main.thy \
Complex/Complex.thy \
Complex/Fundamental_Theorem_Algebra.thy \
@@ -210,6 +211,7 @@
Library/GCD.thy \
Library/Order_Relation.thy \
Library/Parity.thy \
+ Library/RType.thy \
Library/Univ_Poly.thy \
List.thy \
Main.thy \
@@ -301,7 +303,7 @@
Library/List_lexord.thy Library/Commutative_Ring.thy \
Library/comm_ring.ML Library/Coinductive_List.thy \
Library/AssocList.thy \
- Library/Binomial.thy Library/Eval.thy Library/Eval_Witness.thy \
+ Library/Binomial.thy Library/Eval_Witness.thy \
Library/Code_Index.thy Library/Code_Char.thy \
Library/Code_Char_chr.thy Library/Code_Integer.thy \
Library/Code_Message.thy \
--- a/src/HOL/ex/Eval_Examples.thy Mon Sep 15 20:51:58 2008 +0200
+++ b/src/HOL/ex/Eval_Examples.thy Tue Sep 16 09:21:22 2008 +0200
@@ -5,7 +5,7 @@
header {* Small examples for evaluation mechanisms *}
theory Eval_Examples
-imports Eval "~~/src/HOL/Real/Rational"
+imports Code_Eval "~~/src/HOL/Real/Rational"
begin
text {* evaluation oracle *}
@@ -35,44 +35,44 @@
text {* term evaluation *}
value "(Suc 2 + 1) * 4"
-value (code) "(Suc 2 + 1) * 4"
-value (SML) "(Suc 2 + 1) * 4"
-value ("normal_form") "(Suc 2 + 1) * 4"
+value [code] "(Suc 2 + 1) * 4"
+value [SML] "(Suc 2 + 1) * 4"
+value [nbe] "(Suc 2 + 1) * 4"
value "(Suc 2 + Suc 0) * Suc 3"
-value (code) "(Suc 2 + Suc 0) * Suc 3"
-value (SML) "(Suc 2 + Suc 0) * Suc 3"
-value ("normal_form") "(Suc 2 + Suc 0) * Suc 3"
+value [code] "(Suc 2 + Suc 0) * Suc 3"
+value [SML] "(Suc 2 + Suc 0) * Suc 3"
+value [nbe] "(Suc 2 + Suc 0) * Suc 3"
value "nat 100"
-value (code) "nat 100"
-value (SML) "nat 100"
-value ("normal_form") "nat 100"
+value [code] "nat 100"
+value [SML] "nat 100"
+value [nbe] "nat 100"
value "(10\<Colon>int) \<le> 12"
-value (code) "(10\<Colon>int) \<le> 12"
-value (SML) "(10\<Colon>int) \<le> 12"
-value ("normal_form") "(10\<Colon>int) \<le> 12"
+value [code] "(10\<Colon>int) \<le> 12"
+value [SML] "(10\<Colon>int) \<le> 12"
+value [nbe] "(10\<Colon>int) \<le> 12"
value "max (2::int) 4"
-value (code) "max (2::int) 4"
-value (SML) "max (2::int) 4"
-value ("normal_form") "max (2::int) 4"
+value [code] "max (2::int) 4"
+value [SML] "max (2::int) 4"
+value [nbe] "max (2::int) 4"
value "of_int 2 / of_int 4 * (1::rat)"
-value (code) "of_int 2 / of_int 4 * (1::rat)"
-value (SML) "of_int 2 / of_int 4 * (1::rat)"
-value ("normal_form") "of_int 2 / of_int 4 * (1::rat)"
+value [code] "of_int 2 / of_int 4 * (1::rat)"
+value [SML] "of_int 2 / of_int 4 * (1::rat)"
+value [nbe] "of_int 2 / of_int 4 * (1::rat)"
value "[]::nat list"
-value (code) "[]::nat list"
-value (SML) "[]::nat list"
-value ("normal_form") "[]::nat list"
+value [code] "[]::nat list"
+value [SML] "[]::nat list"
+value [nbe] "[]::nat list"
value "[(nat 100, ())]"
-value (code) "[(nat 100, ())]"
-value (SML) "[(nat 100, ())]"
-value ("normal_form") "[(nat 100, ())]"
+value [code] "[(nat 100, ())]"
+value [SML] "[(nat 100, ())]"
+value [nbe] "[(nat 100, ())]"
text {* a fancy datatype *}
@@ -85,8 +85,8 @@
Cair 'a 'b
value "Shift (Cair (4::nat) [Suc 0])"
-value (code) "Shift (Cair (4::nat) [Suc 0])"
-value (SML) "Shift (Cair (4::nat) [Suc 0])"
-value ("normal_form") "Shift (Cair (4::nat) [Suc 0])"
+value [code] "Shift (Cair (4::nat) [Suc 0])"
+value [SML] "Shift (Cair (4::nat) [Suc 0])"
+value [nbe] "Shift (Cair (4::nat) [Suc 0])"
end
--- a/src/Pure/IsaMakefile Mon Sep 15 20:51:58 2008 +0200
+++ b/src/Pure/IsaMakefile Tue Sep 16 09:21:22 2008 +0200
@@ -72,7 +72,7 @@
Syntax/syn_trans.ML Syntax/syntax.ML Syntax/type_ext.ML Thy/html.ML \
Thy/latex.ML Thy/present.ML Thy/term_style.ML Thy/thm_deps.ML \
Thy/thy_edit.ML Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML \
- Thy/thy_output.ML Tools/ROOT.ML Tools/invoke.ML \
+ Thy/thy_output.ML Tools/ROOT.ML Tools/invoke.ML Tools/value.ML \
Tools/isabelle_process.ML Tools/named_thms.ML Tools/xml_syntax.ML \
assumption.ML axclass.ML codegen.ML config.ML conjunction.ML \
consts.ML context.ML conv.ML defs.ML display.ML drule.ML envir.ML \
--- a/src/Pure/Tools/ROOT.ML Mon Sep 15 20:51:58 2008 +0200
+++ b/src/Pure/Tools/ROOT.ML Tue Sep 16 09:21:22 2008 +0200
@@ -4,6 +4,7 @@
Miscellaneous tools and packages for Pure Isabelle.
*)
+use "value.ML";
use "named_thms.ML";
use "isabelle_process.ML";
@@ -12,4 +13,3 @@
(*derived theory and proof elements*)
use "invoke.ML";
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/value.ML Tue Sep 16 09:21:22 2008 +0200
@@ -0,0 +1,67 @@
+(* Title: Pure/Tools/value.ML
+ ID: $Id$
+ Author: Florian Haftmann, TU Muenchen
+
+Value command for different 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
+end;
+
+structure Value : VALUE =
+struct
+
+structure Evaluator = TheoryDataFun(
+ type T = (string * (Proof.context -> term -> term)) list;
+ val empty = [];
+ val copy = I;
+ val extend = I;
+ fun merge pp = AList.merge (op =) (K true);
+)
+
+val add_evaluator = Evaluator.map o AList.update (op =);
+
+fun value_select name ctxt =
+ case AList.lookup (op =) (Evaluator.get (ProofContext.theory_of ctxt)) name
+ of NONE => error ("No such evaluator: " ^ name)
+ | SOME f => f ctxt;
+
+fun value ctxt t = let val evaluators = Evaluator.get (ProofContext.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_cmd some_name modes raw_t state =
+ let
+ val ctxt = Toplevel.context_of state;
+ val t = Syntax.read_term ctxt raw_t;
+ val t' = case some_name
+ of NONE => value ctxt t
+ | SOME name => value_select name ctxt t;
+ val ty' = Term.type_of t';
+ val ctxt' = Variable.auto_fixes t ctxt;
+ val p = PrintMode.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;
+
+local structure P = OuterParse and K = OuterKeyword in
+
+val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
+
+val _ = OuterSyntax.improper_command "value" "evaluate and print term" K.diag
+ (Scan.option (P.$$$ "[" |-- P.xname --| P.$$$ "]") -- opt_modes -- P.term
+ >> (fn ((some_name, modes), t) => Toplevel.no_timing o Toplevel.keep
+ (value_cmd some_name modes t)));
+
+end; (*local*)
+
+end;
--- a/src/Pure/codegen.ML Mon Sep 15 20:51:58 2008 +0200
+++ b/src/Pure/codegen.ML Tue Sep 16 09:21:22 2008 +0200
@@ -96,6 +96,8 @@
val del_nodes: string list -> codegr -> codegr
val map_node: string -> (node -> node) -> codegr -> codegr
val new_node: string * node -> codegr -> codegr
+
+ val setup: theory -> theory
end;
structure Codegen : CODEGEN =
@@ -154,7 +156,7 @@
type nametab = (string * string) Symtab.table * unit Symtab.table;
-fun merge_nametabs ((tab, used), (tab', used')) =
+fun merge_nametabs ((tab, used) : nametab, (tab', used')) =
(Symtab.merge op = (tab, tab'), Symtab.merge op = (used, used'));
type node =
@@ -232,7 +234,7 @@
fun merge _
({codegens = codegens1, tycodegens = tycodegens1,
consts = consts1, types = types1,
- preprocs = preprocs1, modules = modules1, test_params = test_params1},
+ preprocs = preprocs1, modules = modules1, test_params = test_params1} : T,
{codegens = codegens2, tycodegens = tycodegens2,
consts = consts2, types = types2,
preprocs = preprocs2, modules = modules2, test_params = test_params2}) =
@@ -347,14 +349,6 @@
end)
in add_preprocessor prep end;
-val _ = Context.>>
- (let
- fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
- in
- Context.map_theory (Code.add_attribute ("unfold", Scan.succeed (mk_attribute
- (fn thm => add_unfold thm #> Code.add_inline thm))))
- end);
-
(**** associate constants with target language code ****)
@@ -784,11 +778,6 @@
(add_edge (node_id, dep) gr'', p module''))
end);
-val _ = Context.>> (Context.map_theory
- (add_codegen "default" default_codegen #>
- add_tycodegen "default" default_tycodegen));
-
-
fun mk_tuple [p] = p
| mk_tuple ps = Pretty.block (str "(" ::
List.concat (separate [str ",", Pretty.brk 1] (map single ps)) @
@@ -804,7 +793,7 @@
fun mk_struct name s = "structure " ^ name ^ " =\nstruct\n\n" ^ s ^ "end;\n";
-fun add_to_module name s = AList.map_entry (op =) name (suffix s);
+fun add_to_module name s = AList.map_entry (op =) (name : string) (suffix s);
fun output_code gr module xs =
let
@@ -1023,8 +1012,6 @@
else state
end;
-val _ = Context.>> (Specification.add_theorem_hook test_goal');
-
(**** Evaluator for terms ****)
@@ -1053,18 +1040,6 @@
in !eval_result end;
in e () end;
-fun print_evaluated_term s = Toplevel.keep (fn state =>
- let
- val ctxt = Toplevel.context_of state;
- val thy = ProofContext.theory_of ctxt;
- val t = eval_term thy (Syntax.read_term ctxt s);
- val T = Term.type_of t;
- in
- Pretty.writeln
- (Pretty.block [Pretty.quote (Syntax.pretty_term ctxt t), Pretty.fbrk,
- Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt T)])
- end);
-
exception Evaluation of term;
fun evaluation_oracle (thy, Evaluation t) =
@@ -1072,10 +1047,7 @@
fun evaluation_conv ct =
let val thy = Thm.theory_of_cterm ct
- in Thm.invoke_oracle_i thy "Pure.evaluation" (thy, Evaluation (Thm.term_of ct)) end;
-
-val _ = Context.>> (Context.map_theory
- (Theory.add_oracle ("evaluation", evaluation_oracle)));
+ in Thm.invoke_oracle_i thy "HOL.evaluation" (thy, Evaluation (Thm.term_of ct)) end;
(**** Interface ****)
@@ -1156,6 +1128,15 @@
else map_modules (Symtab.update (module, gr)) thy)
end));
+val setup = add_codegen "default" default_codegen
+ #> add_tycodegen "default" default_tycodegen
+ #> Theory.add_oracle ("evaluation", evaluation_oracle)
+ #> Value.add_evaluator ("SML", eval_term o ProofContext.theory_of)
+ #> Code.add_attribute ("unfold", Scan.succeed (Thm.declaration_attribute
+ (fn thm => Context.mapping (add_unfold thm #> Code.add_inline thm) I)));
+
+val _ = Context.>> (Specification.add_theorem_hook test_goal');
+
val _ =
OuterSyntax.command "code_library"
"generates code for terms (one structure for each theory)" K.thy_decl
@@ -1195,10 +1176,6 @@
(get_test_params (Toplevel.theory_of st), [])) g [] |>
pretty_counterex (Toplevel.context_of st) |> Pretty.writeln)));
-val _ =
- OuterSyntax.improper_command "value" "read, evaluate and print term" K.diag
- (P.term >> (Toplevel.no_timing oo print_evaluated_term));
-
end;
val auto_quickcheck = Codegen.auto_quickcheck;
--- a/src/Tools/nbe.ML Mon Sep 15 20:51:58 2008 +0200
+++ b/src/Tools/nbe.ML Tue Sep 16 09:21:22 2008 +0200
@@ -454,7 +454,8 @@
let val ctxt = Toplevel.context_of state
in norm_print_term ctxt modes (Syntax.read_term ctxt s) end;
-val setup = Theory.add_oracle ("norm", norm_oracle);
+val setup = Theory.add_oracle ("norm", norm_oracle)
+ #> Value.add_evaluator ("nbe", norm_term o ProofContext.theory_of);
local structure P = OuterParse and K = OuterKeyword in
@@ -462,7 +463,7 @@
val _ =
OuterSyntax.improper_command "normal_form" "normalize term by evaluation" K.diag
- (opt_modes -- P.typ >> (Toplevel.keep o norm_print_term_cmd));
+ (opt_modes -- P.term >> (Toplevel.keep o norm_print_term_cmd));
end;