# HG changeset patch # User haftmann # Date 1187161059 -7200 # Node ID c9867bdf24247969cb94ae23804dbdc893912d90 # Parent 165648d5679feafb6653de3ff58d7df08daab925 updated code generator setup diff -r 165648d5679f -r c9867bdf2424 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Wed Aug 15 08:57:38 2007 +0200 +++ b/src/HOL/HOL.thy Wed Aug 15 08:57:39 2007 +0200 @@ -24,7 +24,12 @@ "~~/src/Provers/eqsubst.ML" "~~/src/Provers/quantifier1.ML" ("simpdata.ML") - ("~~/src/HOL/Tools/recfun_codegen.ML") + "~~/src/Pure/codegen.ML" + "~~/src/Tools/code/code_name.ML" + "~~/src/Tools/code/code_funcgr.ML" + "~~/src/Tools/code/code_thingol.ML" + "~~/src/Tools/code/code_target.ML" + "~~/src/Tools/code/code_package.ML" "~~/src/Tools/nbe.ML" begin @@ -1636,204 +1641,43 @@ *} -subsection {* Code generator setup *} - -subsubsection {* SML code generator setup *} - -use "~~/src/HOL/Tools/recfun_codegen.ML" - -types_code - "bool" ("bool") -attach (term_of) {* -fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const; -*} -attach (test) {* -fun gen_bool i = one_of [false, true]; -*} - "prop" ("bool") -attach (term_of) {* -fun term_of_prop b = - HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const); -*} - -consts_code - "Trueprop" ("(_)") - "True" ("true") - "False" ("false") - "Not" ("Bool.not") - "op |" ("(_ orelse/ _)") - "op &" ("(_ andalso/ _)") - "If" ("(if _/ then _/ else _)") - -setup {* -let +subsection {* Code generator basic setup -- see further @{text Code_Setup.thy} *} -fun eq_codegen thy defs gr dep thyname b t = - (case strip_comb t of - (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE - | (Const ("op =", _), [t, u]) => - let - val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t); - val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u); - val (gr''', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr'', HOLogic.boolT) - in - SOME (gr''', Codegen.parens - (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu])) - end - | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen - thy defs dep thyname b (gr, Codegen.eta_expand t ts 2)) - | _ => NONE); - -in - -Codegen.add_codegen "eq_codegen" eq_codegen -#> RecfunCodegen.setup - -end -*} - -text {* Evaluation *} - -method_setup evaluation = {* - Method.no_args (Method.SIMPLE_METHOD' (CONVERSION Codegen.evaluation_conv THEN' rtac TrueI)) -*} "solve goal by evaluation" - - -subsubsection {* Generic code generator setup *} - -setup "CodeName.setup #> CodeTarget.setup" - -text {* operational equality for code generation *} +setup "CodeName.setup #> CodeTarget.setup #> Codegen.setup" class eq (attach "op =") = type - -text {* using built-in Haskell equality *} - -code_class eq - (Haskell "Eq" where "op =" \ "(==)") - -code_const "op =" - (Haskell infixl 4 "==") - - -text {* type bool *} - code_datatype True False lemma [code func]: - shows "(False \ x) = False" - and "(True \ x) = x" - and "(x \ False) = False" - and "(x \ True) = x" by simp_all + shows "False \ x \ False" + and "True \ x \ x" + and "x \ False \ False" + and "x \ True \ x" by simp_all lemma [code func]: - shows "(False \ x) = x" - and "(True \ x) = True" - and "(x \ False) = x" - and "(x \ True) = True" by simp_all + shows "False \ x \ x" + and "True \ x \ True" + and "x \ False \ x" + and "x \ True \ True" by simp_all lemma [code func]: - shows "(\ True) = False" - and "(\ False) = True" by (rule HOL.simp_thms)+ - -lemmas [code] = imp_conv_disj + shows "\ True \ False" + and "\ False \ True" by (rule HOL.simp_thms)+ instance bool :: eq .. lemma [code func]: - shows "True = P \ P" - and "False = P \ \ P" - and "P = True \ P" - and "P = False \ \ P" by simp_all - -code_type bool - (SML "bool") - (OCaml "bool") - (Haskell "Bool") - -code_instance bool :: eq - (Haskell -) - -code_const "op = \ bool \ bool \ bool" - (Haskell infixl 4 "==") - -code_const True and False and Not and "op &" and "op |" and If - (SML "true" and "false" and "not" - and infixl 1 "andalso" and infixl 0 "orelse" - and "!(if (_)/ then (_)/ else (_))") - (OCaml "true" and "false" and "not" - and infixl 4 "&&" and infixl 2 "||" - and "!(if (_)/ then (_)/ else (_))") - (Haskell "True" and "False" and "not" - and infixl 3 "&&" and infixl 2 "||" - and "!(if (_)/ then (_)/ else (_))") - -code_reserved SML - bool true false not - -code_reserved OCaml - bool not - - -text {* type prop *} + shows "False = P \ \ P" + and "True = P \ P" + and "P = False \ \ P" + and "P = True \ P" by simp_all code_datatype Trueprop "prop" - -text {* type itself *} - code_datatype "TYPE('a)" -text {* code generation for undefined as exception *} - -code_const undefined - (SML "raise/ Fail/ \"undefined\"") - (OCaml "failwith/ \"undefined\"") - (Haskell "error/ \"undefined\"") - - -text {* Let and If *} - -lemmas [code func] = Let_def if_True if_False - -setup {* - CodePackage.add_appconst (@{const_name Let}, CodePackage.appgen_let) - #> CodePackage.add_appconst (@{const_name If}, CodePackage.appgen_if) -*} - - -subsubsection {* Evaluation oracle *} - -oracle eval_oracle ("term") = {* fn thy => fn t => - if CodePackage.satisfies thy (HOLogic.dest_Trueprop t) [] - then t - else HOLogic.Trueprop $ HOLogic.true_const (*dummy*) -*} - -method_setup eval = {* -let - fun eval_tac thy = - SUBGOAL (fn (t, i) => rtac (eval_oracle thy t) i) -in - Method.ctxt_args (fn ctxt => - Method.SIMPLE_METHOD' (eval_tac (ProofContext.theory_of ctxt))) -end -*} "solve goal by evaluation" - - -subsubsection {* Normalization by evaluation *} - -setup Nbe.setup - -method_setup normalization = {* - Method.no_args (Method.SIMPLE_METHOD' - (CONVERSION (ObjectLogic.judgment_conv Nbe.normalization_conv) - THEN' resolve_tac [TrueI, refl])) -*} "solve goal by normalization" - - subsection {* Legacy tactics and ML bindings *} ML {* diff -r 165648d5679f -r c9867bdf2424 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Aug 15 08:57:38 2007 +0200 +++ b/src/HOL/IsaMakefile Wed Aug 15 08:57:39 2007 +0200 @@ -82,8 +82,12 @@ $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML \ $(SRC)/Provers/quasi.ML $(SRC)/Provers/splitter.ML \ $(SRC)/Provers/trancl.ML $(SRC)/Tools/integer.ML $(SRC)/Tools/Metis/metis.ML\ + $(SRC)/Pure/codegen.ML \ + $(SRC)/Tools/code/code_funcgr.ML \ + $(SRC)/Tools/code/code_name.ML $(SRC)/Tools/code/code_package.ML \ + $(SRC)/Tools/code/code_target.ML $(SRC)/Tools/code/code_thingol.ML \ $(SRC)/Tools/nbe.ML $(SRC)/Tools/rat.ML Tools/TFL/casesplit.ML ATP_Linkup.thy \ - Accessible_Part.thy Arith_Tools.thy Datatype.thy \ + Accessible_Part.thy Arith_Tools.thy Code_Setup.thy Datatype.thy \ Dense_Linear_Order.thy Divides.thy Equiv_Relations.thy Extraction.thy \ Finite_Set.thy FixedPoint.thy Fun.thy FunDef.thy HOL.thy \ Hilbert_Choice.thy Inductive.thy IntArith.thy IntDef.thy IntDiv.thy \ @@ -222,7 +226,7 @@ Library/SCT_Interpretation.thy \ Library/SCT_Implementation.thy Library/Size_Change_Termination.thy \ Library/SCT_Examples.thy Library/sct.ML \ - Library/Pure_term.thy Library/Eval.thy Library/Pretty_Int.thy \ + Library/Pure_term.thy Library/Eval.thy Library/Eval_Witness.thy Library/Pretty_Int.thy \ Library/Pretty_Char.thy Library/Pretty_Char_chr.thy Library/Abstract_Rat.thy @cd Library; $(ISATOOL) usedir $(OUT)/HOL Library diff -r 165648d5679f -r c9867bdf2424 src/HOL/Library/Eval.thy --- a/src/HOL/Library/Eval.thy Wed Aug 15 08:57:38 2007 +0200 +++ b/src/HOL/Library/Eval.thy Wed Aug 15 08:57:39 2007 +0200 @@ -6,7 +6,7 @@ header {* A simple term evaluation mechanism *} theory Eval -imports Pure_term +imports Main Pure_term begin subsection {* @{text typ_of} class *} @@ -154,31 +154,67 @@ signature EVAL = sig val eval_ref: term option ref - val eval_term: theory -> term -> term - val print: (theory -> term -> term) -> string - -> Toplevel.transition -> Toplevel.transition + val eval_conv: cterm -> thm + val eval_print: (cterm -> thm) -> Proof.context -> term -> unit + val eval_print_cmd: (cterm -> thm) -> string -> Toplevel.state -> unit end; -structure Eval : EVAL = +structure Eval = struct val eval_ref = ref (NONE : term option); -fun eval_term thy t = - CodePackage.eval_term - thy (("Eval.eval_ref", eval_ref), TermOf.mk_term_of t); +end; +*} + +oracle eval_oracle ("term * CodeThingol.code * CodeThingol.iterm * CodeThingol.itype * cterm") = {* fn thy => fn (t0, code, t, ty, ct) => +let + val _ = (Term.map_types o Term.map_atyps) (fn _ => + error ("Term " ^ Sign.string_of_term thy t0 ^ " contains polymorphic type")) + t0; +in Logic.mk_equals (t0, CodeTarget.eval_term thy ("Eval.eval_ref", Eval.eval_ref) code (t, ty) []) end; +*} + +ML {* +structure Eval : EVAL = +struct + +open Eval; + +fun eval_invoke thy t0 code (t, ty) _ ct = eval_oracle thy (t0, code, t, ty, ct); -fun print eval s = Toplevel.keep (fn state => +fun eval_conv ct = + let + val thy = Thm.theory_of_cterm ct; + val ct' = (Thm.cterm_of thy o TermOf.mk_term_of o Thm.term_of) ct; + in + CodePackage.eval_term thy + (eval_invoke thy (Thm.term_of ct)) ct' + end; + +fun eval_print conv ctxt t = + let + val thy = ProofContext.theory_of ctxt; + val ct = Thm.cterm_of thy t; + val (_, t') = (Logic.dest_equals o Thm.prop_of o conv) ct; + val ty = Term.type_of t'; + val p = + Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t'), Pretty.fbrk, + Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt ty)]; + in Pretty.writeln p end; + +fun eval_print_cmd conv raw_t state = let val ctxt = Toplevel.context_of state; + val t = ProofContext.read_term ctxt raw_t; val thy = ProofContext.theory_of ctxt; - val t = eval thy (ProofContext.read_term ctxt s); - val T = Term.type_of t; - in - writeln (Pretty.string_of - (Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t), Pretty.fbrk, - Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt T)])) - end); + val ct = Thm.cterm_of thy t; + val (_, t') = (Logic.dest_equals o Thm.prop_of o conv) ct; + val ty = Term.type_of t'; + val p = + Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t'), Pretty.fbrk, + Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt ty)]; + in Pretty.writeln p end; end; *} @@ -187,8 +223,8 @@ val valueP = OuterSyntax.improper_command "value" "read, evaluate and print term" OuterKeyword.diag ((OuterParse.opt_keyword "overloaded" -- OuterParse.term) - >> (fn (b, t) => (Toplevel.no_timing o Eval.print - (if b then Eval.eval_term else Codegen.eval_term) t))); + >> (fn (b, t) => Toplevel.no_timing o Toplevel.keep + (Eval.eval_print_cmd (if b then Eval.eval_conv else Codegen.evaluation_conv) t))); val _ = OuterSyntax.add_parsers [valueP]; *} diff -r 165648d5679f -r c9867bdf2424 src/HOL/Set.thy --- a/src/HOL/Set.thy Wed Aug 15 08:57:38 2007 +0200 +++ b/src/HOL/Set.thy Wed Aug 15 08:57:39 2007 +0200 @@ -6,7 +6,7 @@ header {* Set theory for higher-order logic *} theory Set -imports HOL +imports Code_Setup begin text {* A set in HOL is simply a predicate. *} diff -r 165648d5679f -r c9867bdf2424 src/HOL/ex/Eval_Examples.thy --- a/src/HOL/ex/Eval_Examples.thy Wed Aug 15 08:57:38 2007 +0200 +++ b/src/HOL/ex/Eval_Examples.thy Wed Aug 15 08:57:39 2007 +0200 @@ -12,17 +12,19 @@ lemma "True \ False" by eval lemma "\ (Suc 0 = Suc 1)" by eval +lemma "[] = ([]\ int list)" by eval +lemma "[()] = [()]" by eval text {* term evaluation *} value (overloaded) "(Suc 2 + 1) * 4" value (overloaded) "(Suc 2 + 1) * 4" value (overloaded) "(Suc 2 + Suc 0) * Suc 3" +value (overloaded) "nat 100" +value (overloaded) "(10\int) \ 12" +value (overloaded) "[(nat 100, ())]" value (overloaded) "[]::nat list" value (overloaded) "fst ([]::nat list, Suc 0) = []" -value (overloaded) "nat 100" -value (overloaded) "[(nat 100, ())]" -value (overloaded) "int 10 \ 12" text {* a fancy datatype *} diff -r 165648d5679f -r c9867bdf2424 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Wed Aug 15 08:57:38 2007 +0200 +++ b/src/Pure/IsaMakefile Wed Aug 15 08:57:39 2007 +0200 @@ -23,9 +23,7 @@ Pure: $(OUT)/Pure$(ML_SUFFIX) -$(OUT)/Pure$(ML_SUFFIX): $(SRC)/Tools/code/code_funcgr.ML \ - $(SRC)/Tools/code/code_name.ML $(SRC)/Tools/code/code_package.ML \ - $(SRC)/Tools/code/code_target.ML $(SRC)/Tools/code/code_thingol.ML \ +$(OUT)/Pure$(ML_SUFFIX): \ CPure.thy General/ROOT.ML General/alist.ML General/balanced_tree.ML \ General/basics.ML General/buffer.ML General/file.ML General/graph.ML \ General/heap.ML General/history.ML General/markup.ML \ @@ -68,7 +66,7 @@ Thy/present.ML Thy/term_style.ML Thy/thm_database.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 Tools/named_thms.ML \ - Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML \ + Tools/xml_syntax.ML assumption.ML axclass.ML \ compress.ML config.ML conjunction.ML consts.ML context.ML \ context_position.ML conv.ML defs.ML display.ML drule.ML envir.ML \ fact_index.ML goal.ML library.ML logic.ML meta_simplifier.ML \ diff -r 165648d5679f -r c9867bdf2424 src/Pure/Tools/ROOT.ML --- a/src/Pure/Tools/ROOT.ML Wed Aug 15 08:57:38 2007 +0200 +++ b/src/Pure/Tools/ROOT.ML Wed Aug 15 08:57:39 2007 +0200 @@ -11,11 +11,3 @@ (*derived theory and proof elements*) use "invoke.ML"; - -(*code generator*) -use "../codegen.ML"; -use "../../Tools/code/code_name.ML"; -use "../../Tools/code/code_funcgr.ML"; -use "../../Tools/code/code_thingol.ML"; -use "../../Tools/code/code_target.ML"; -use "../../Tools/code/code_package.ML"; diff -r 165648d5679f -r c9867bdf2424 src/Pure/codegen.ML --- a/src/Pure/codegen.ML Wed Aug 15 08:57:38 2007 +0200 +++ b/src/Pure/codegen.ML Wed Aug 15 08:57:39 2007 +0200 @@ -85,6 +85,8 @@ val mk_deftab: theory -> deftab val add_unfold: thm -> theory -> theory + val setup: theory -> theory + val get_node: codegr -> string -> node val add_edge: string * string -> codegr -> codegr val add_edge_acyclic: string * string -> codegr -> codegr @@ -336,13 +338,6 @@ end) in add_preprocessor prep end; -val _ = Context.add_setup - (let - fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I); - in - Code.add_attribute ("unfold", Scan.succeed (mk_attribute - (fn thm => add_unfold thm #> Code.add_inline thm))) - end); (**** associate constants with target language code ****) @@ -798,11 +793,6 @@ (add_edge (node_id, dep) gr'', p module'')) end); -val _ = Context.add_setup - (add_codegen "default" default_codegen #> - add_tycodegen "default" default_tycodegen); - - 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); @@ -1034,10 +1024,8 @@ fun evaluation_conv ct = let val {thy, t, ...} = rep_cterm ct - in Thm.invoke_oracle_i thy "Pure.evaluation" (thy, Evaluation t) end; + in Thm.invoke_oracle_i thy "Code_Setup.evaluation" (thy, Evaluation t) end; -val _ = Context.add_setup - (Theory.add_oracle ("evaluation", evaluation_oracle)); (**** Interface ****) @@ -1061,21 +1049,6 @@ (p, []) => p | _ => error ("Malformed annotation: " ^ quote s)); -val _ = Context.add_setup - (fold assoc_type [("fun", (parse_mixfix (K dummyT) "(_ ->/ _)", - [("term_of", - "fun term_of_fun_type _ T _ U _ = Free (\"\", T --> U);\n"), - ("test", - "fun gen_fun_type _ G i =\n\ - \ let\n\ - \ val f = ref (fn x => raise Match);\n\ - \ val _ = (f := (fn x =>\n\ - \ let\n\ - \ val y = G i;\n\ - \ val f' = !f\n\ - \ in (f := (fn x' => if x = x' then y else f' x'); y) end))\n\ - \ in (fn x => !f x) end;\n")]))]); - structure P = OuterParse and K = OuterKeyword; @@ -1180,4 +1153,28 @@ val _ = OuterSyntax.add_parsers [assoc_typeP, assoc_constP, code_libraryP, code_moduleP, test_paramsP, testP, valueP]; +val setup = + let + fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I); + in + Code.add_attribute ("unfold", Scan.succeed (mk_attribute + (fn thm => add_unfold thm #> Code.add_inline thm))) + #> add_codegen "default" default_codegen + #> add_tycodegen "default" default_tycodegen + #> Theory.add_oracle ("evaluation", evaluation_oracle) + #> fold assoc_type [("fun", (parse_mixfix (K dummyT) "(_ ->/ _)", + [("term_of", + "fun term_of_fun_type _ T _ U _ = Free (\"\", T --> U);\n"), + ("test", + "fun gen_fun_type _ G i =\n\ + \ let\n\ + \ val f = ref (fn x => raise Match);\n\ + \ val _ = (f := (fn x =>\n\ + \ let\n\ + \ val y = G i;\n\ + \ val f' = !f\n\ + \ in (f := (fn x' => if x = x' then y else f' x'); y) end))\n\ + \ in (fn x => !f x) end;\n")]))] + end; + end;