--- 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 =" \<equiv> "(==)")
-
-code_const "op ="
- (Haskell infixl 4 "==")
-
-
-text {* type bool *}
-
code_datatype True False
lemma [code func]:
- shows "(False \<and> x) = False"
- and "(True \<and> x) = x"
- and "(x \<and> False) = False"
- and "(x \<and> True) = x" by simp_all
+ shows "False \<and> x \<longleftrightarrow> False"
+ and "True \<and> x \<longleftrightarrow> x"
+ and "x \<and> False \<longleftrightarrow> False"
+ and "x \<and> True \<longleftrightarrow> x" by simp_all
lemma [code func]:
- shows "(False \<or> x) = x"
- and "(True \<or> x) = True"
- and "(x \<or> False) = x"
- and "(x \<or> True) = True" by simp_all
+ shows "False \<or> x \<longleftrightarrow> x"
+ and "True \<or> x \<longleftrightarrow> True"
+ and "x \<or> False \<longleftrightarrow> x"
+ and "x \<or> True \<longleftrightarrow> True" by simp_all
lemma [code func]:
- shows "(\<not> True) = False"
- and "(\<not> False) = True" by (rule HOL.simp_thms)+
-
-lemmas [code] = imp_conv_disj
+ shows "\<not> True \<longleftrightarrow> False"
+ and "\<not> False \<longleftrightarrow> True" by (rule HOL.simp_thms)+
instance bool :: eq ..
lemma [code func]:
- shows "True = P \<longleftrightarrow> P"
- and "False = P \<longleftrightarrow> \<not> P"
- and "P = True \<longleftrightarrow> P"
- and "P = False \<longleftrightarrow> \<not> P" by simp_all
-
-code_type bool
- (SML "bool")
- (OCaml "bool")
- (Haskell "Bool")
-
-code_instance bool :: eq
- (Haskell -)
-
-code_const "op = \<Colon> bool \<Rightarrow> bool \<Rightarrow> 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 \<longleftrightarrow> \<not> P"
+ and "True = P \<longleftrightarrow> P"
+ and "P = False \<longleftrightarrow> \<not> P"
+ and "P = True \<longleftrightarrow> 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 {*
--- 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
--- 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];
*}
--- 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. *}
--- 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 \<or> False" by eval
lemma "\<not> (Suc 0 = Suc 1)" by eval
+lemma "[] = ([]\<Colon> 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\<Colon>int) \<le> 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 \<le> 12"
text {* a fancy datatype *}
--- 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 \
--- 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";
--- 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 (\"<function>\", 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 (\"<function>\", 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;