Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
set print_mode and margin appropriately.
1 (* Title: HOL/Code_Setup.thy
3 Author: Florian Haftmann
6 header {* Setup of code generators and derived tools *}
10 uses "~~/src/HOL/Tools/recfun_codegen.ML"
13 subsection {* SML code generator setup *}
15 setup RecfunCodegen.setup
20 fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
24 let val b = one_of [false, true]
25 in (b, fn () => term_of_bool b) end;
30 HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const);
38 "op |" ("(_ orelse/ _)")
39 "op &" ("(_ andalso/ _)")
40 "If" ("(if _/ then _/ else _)")
45 fun eq_codegen thy defs gr dep thyname b t =
47 (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
48 | (Const ("op =", _), [t, u]) =>
50 val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t);
51 val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u);
52 val (gr''', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr'', HOLogic.boolT)
54 SOME (gr''', Codegen.parens
55 (Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]))
57 | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
58 thy defs dep thyname b (gr, Codegen.eta_expand t ts 2))
62 Codegen.add_codegen "eq_codegen" eq_codegen
66 quickcheck_params [size = 5, iterations = 50]
70 method_setup evaluation = {*
71 Method.no_args (Method.SIMPLE_METHOD' (CONVERSION Codegen.evaluation_conv THEN' rtac TrueI))
72 *} "solve goal by evaluation"
75 subsection {* Generic code generator setup *}
78 text {* using built-in Haskell equality *}
81 (Haskell "Eq" where "op =" \<equiv> "(==)")
84 (Haskell infixl 4 "==")
89 lemmas [code func, code unfold, code post] = imp_conv_disj
96 code_const True and False and Not and "op &" and "op |" and If
97 (SML "true" and "false" and "not"
98 and infixl 1 "andalso" and infixl 0 "orelse"
99 and "!(if (_)/ then (_)/ else (_))")
100 (OCaml "true" and "false" and "not"
101 and infixl 4 "&&" and infixl 2 "||"
102 and "!(if (_)/ then (_)/ else (_))")
103 (Haskell "True" and "False" and "not"
104 and infixl 3 "&&" and infixl 2 "||"
105 and "!(if (_)/ then (_)/ else (_))")
114 text {* code generation for undefined as exception *}
117 (SML "raise/ Fail/ \"undefined\"")
118 (OCaml "failwith/ \"undefined\"")
119 (Haskell "error/ \"undefined\"")
122 text {* Let and If *}
124 lemmas [code func] = Let_def if_True if_False
127 subsection {* Evaluation oracle *}
129 oracle eval_oracle ("term") = {* fn thy => fn t =>
130 if CodePackage.satisfies thy (HOLogic.dest_Trueprop t) []
132 else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
135 method_setup eval = {*
138 SUBGOAL (fn (t, i) => rtac (eval_oracle thy t) i)
140 Method.ctxt_args (fn ctxt =>
141 Method.SIMPLE_METHOD' (eval_tac (ProofContext.theory_of ctxt)))
143 *} "solve goal by evaluation"
146 subsection {* Normalization by evaluation *}
148 method_setup normalization = {*
149 Method.no_args (Method.SIMPLE_METHOD'
150 (CONVERSION (ObjectLogic.judgment_conv Nbe.norm_conv)
151 THEN' (fn k => TRY (rtac TrueI k))
153 *} "solve goal by normalization"