# HG changeset patch # User haftmann # Date 1221549682 -7200 # Node ID 77221ee0f7b97ca253225e9b53a810904ae9945a # Parent 97c530dc8aca9d4897b9fec302511859fa52fd1b generic value command diff -r 97c530dc8aca -r 77221ee0f7b9 NEWS --- 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. diff -r 97c530dc8aca -r 77221ee0f7b9 src/HOL/HOL.thy --- 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]: diff -r 97c530dc8aca -r 77221ee0f7b9 src/HOL/IsaMakefile --- 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 \ diff -r 97c530dc8aca -r 77221ee0f7b9 src/HOL/ex/Eval_Examples.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\int) \ 12" -value (code) "(10\int) \ 12" -value (SML) "(10\int) \ 12" -value ("normal_form") "(10\int) \ 12" +value [code] "(10\int) \ 12" +value [SML] "(10\int) \ 12" +value [nbe] "(10\int) \ 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 diff -r 97c530dc8aca -r 77221ee0f7b9 src/Pure/IsaMakefile --- 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 \ diff -r 97c530dc8aca -r 77221ee0f7b9 src/Pure/Tools/ROOT.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"; - diff -r 97c530dc8aca -r 77221ee0f7b9 src/Pure/Tools/value.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; diff -r 97c530dc8aca -r 77221ee0f7b9 src/Pure/codegen.ML --- 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; diff -r 97c530dc8aca -r 77221ee0f7b9 src/Tools/nbe.ML --- 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;