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;
23 fun gen_bool i = one_of [false, true];
28 HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const);
36 "op |" ("(_ orelse/ _)")
37 "op &" ("(_ andalso/ _)")
38 "If" ("(if _/ then _/ else _)")
43 fun eq_codegen thy defs gr dep thyname b t =
45 (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
46 | (Const ("op =", _), [t, u]) =>
48 val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t);
49 val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u);
50 val (gr''', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr'', HOLogic.boolT)
52 SOME (gr''', Codegen.parens
53 (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu]))
55 | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
56 thy defs dep thyname b (gr, Codegen.eta_expand t ts 2))
60 Codegen.add_codegen "eq_codegen" eq_codegen
66 method_setup evaluation = {*
67 Method.no_args (Method.SIMPLE_METHOD' (CONVERSION Codegen.evaluation_conv THEN' rtac TrueI))
68 *} "solve goal by evaluation"
71 subsection {* Generic code generator setup *}
74 text {* using built-in Haskell equality *}
77 (Haskell "Eq" where "op =" \<equiv> "(==)")
80 (Haskell infixl 4 "==")
85 lemmas [code] = imp_conv_disj
92 code_instance bool :: eq
95 code_const "op = \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
96 (Haskell infixl 4 "==")
98 code_const True and False and Not and "op &" and "op |" and If
99 (SML "true" and "false" and "not"
100 and infixl 1 "andalso" and infixl 0 "orelse"
101 and "!(if (_)/ then (_)/ else (_))")
102 (OCaml "true" and "false" and "not"
103 and infixl 4 "&&" and infixl 2 "||"
104 and "!(if (_)/ then (_)/ else (_))")
105 (Haskell "True" and "False" and "not"
106 and infixl 3 "&&" and infixl 2 "||"
107 and "!(if (_)/ then (_)/ else (_))")
116 text {* code generation for undefined as exception *}
119 (SML "raise/ Fail/ \"undefined\"")
120 (OCaml "failwith/ \"undefined\"")
121 (Haskell "error/ \"undefined\"")
124 text {* Let and If *}
126 lemmas [code func] = Let_def if_True if_False
129 CodePackage.add_appconst (@{const_name Let}, CodePackage.appgen_let)
130 #> CodePackage.add_appconst (@{const_name If}, CodePackage.appgen_if)
134 subsection {* Evaluation oracle *}
136 oracle eval_oracle ("term") = {* fn thy => fn t =>
137 if CodePackage.satisfies thy (Thm.cterm_of thy (HOLogic.dest_Trueprop t)) []
139 else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
142 method_setup eval = {*
145 SUBGOAL (fn (t, i) => rtac (eval_oracle thy t) i)
147 Method.ctxt_args (fn ctxt =>
148 Method.SIMPLE_METHOD' (eval_tac (ProofContext.theory_of ctxt)))
150 *} "solve goal by evaluation"
153 subsection {* Normalization by evaluation *}
155 method_setup normalization = {*
156 Method.no_args (Method.SIMPLE_METHOD'
157 (CONVERSION (ObjectLogic.judgment_conv Nbe.normalization_conv)
158 THEN' resolve_tac [TrueI, refl]))
159 *} "solve goal by normalization"