24285

1 
(* Title: HOL/Code_Setup.thy


2 
ID: $Id$


3 
Author: Florian Haftmann


4 
*)


5 


6 
header {* Setup of code generators and derived tools *}


7 


8 
theory Code_Setup


9 
imports HOL


10 
uses "~~/src/HOL/Tools/recfun_codegen.ML"


11 
begin


12 


13 
subsection {* SML code generator setup *}


14 


15 
setup RecfunCodegen.setup


16 


17 
types_code


18 
"bool" ("bool")


19 
attach (term_of) {*


20 
fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;


21 
*}


22 
attach (test) {*


23 
fun gen_bool i = one_of [false, true];


24 
*}


25 
"prop" ("bool")


26 
attach (term_of) {*


27 
fun term_of_prop b =


28 
HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const);


29 
*}


30 


31 
consts_code


32 
"Trueprop" ("(_)")


33 
"True" ("true")


34 
"False" ("false")


35 
"Not" ("Bool.not")


36 
"op " ("(_ orelse/ _)")


37 
"op &" ("(_ andalso/ _)")


38 
"If" ("(if _/ then _/ else _)")


39 


40 
setup {*


41 
let


42 


43 
fun eq_codegen thy defs gr dep thyname b t =


44 
(case strip_comb t of


45 
(Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE


46 
 (Const ("op =", _), [t, u]) =>


47 
let


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)


51 
in


52 
SOME (gr''', Codegen.parens


53 
(Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu]))


54 
end


55 
 (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen


56 
thy defs dep thyname b (gr, Codegen.eta_expand t ts 2))


57 
 _ => NONE);


58 


59 
in


60 
Codegen.add_codegen "eq_codegen" eq_codegen


61 
end


62 
*}


63 


64 
text {* Evaluation *}


65 


66 
method_setup evaluation = {*


67 
Method.no_args (Method.SIMPLE_METHOD' (CONVERSION Codegen.evaluation_conv THEN' rtac TrueI))


68 
*} "solve goal by evaluation"


69 


70 


71 
subsection {* Generic code generator setup *}


72 


73 


74 
text {* using builtin Haskell equality *}


75 


76 
code_class eq


77 
(Haskell "Eq" where "op =" \<equiv> "(==)")


78 


79 
code_const "op ="


80 
(Haskell infixl 4 "==")


81 


82 


83 
text {* type bool *}


84 


85 
lemmas [code] = imp_conv_disj


86 


87 
code_type bool


88 
(SML "bool")


89 
(OCaml "bool")


90 
(Haskell "Bool")


91 


92 
code_instance bool :: eq


93 
(Haskell )


94 


95 
code_const "op = \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"


96 
(Haskell infixl 4 "==")


97 


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 (_))")


108 


109 
code_reserved SML


110 
bool true false not


111 


112 
code_reserved OCaml


113 
bool not


114 


115 


116 
text {* code generation for undefined as exception *}


117 


118 
code_const undefined


119 
(SML "raise/ Fail/ \"undefined\"")


120 
(OCaml "failwith/ \"undefined\"")


121 
(Haskell "error/ \"undefined\"")


122 


123 


124 
text {* Let and If *}


125 


126 
lemmas [code func] = Let_def if_True if_False


127 


128 
setup {*


129 
CodePackage.add_appconst (@{const_name Let}, CodePackage.appgen_let)


130 
#> CodePackage.add_appconst (@{const_name If}, CodePackage.appgen_if)


131 
*}


132 


133 


134 
subsection {* Evaluation oracle *}


135 


136 
oracle eval_oracle ("term") = {* fn thy => fn t =>


137 
if CodePackage.satisfies thy (Thm.cterm_of thy (HOLogic.dest_Trueprop t)) []


138 
then t


139 
else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)


140 
*}


141 


142 
method_setup eval = {*


143 
let


144 
fun eval_tac thy =


145 
SUBGOAL (fn (t, i) => rtac (eval_oracle thy t) i)


146 
in


147 
Method.ctxt_args (fn ctxt =>


148 
Method.SIMPLE_METHOD' (eval_tac (ProofContext.theory_of ctxt)))


149 
end


150 
*} "solve goal by evaluation"


151 


152 


153 
subsection {* Normalization by evaluation *}


154 


155 
setup Nbe.setup


156 


157 
method_setup normalization = {*


158 
Method.no_args (Method.SIMPLE_METHOD'


159 
(CONVERSION (ObjectLogic.judgment_conv Nbe.normalization_conv)


160 
THEN' resolve_tac [TrueI, refl]))


161 
*} "solve goal by normalization"


162 


163 


164 
end
