haftmann@31378: 
haftmann@31378: (* Author: Florian Haftmann, TU Muenchen *)
haftmann@24195: 
haftmann@31378: header {* Pervasive test of code generator using pretty literals *}
haftmann@24195: 
haftmann@37695: theory Generate_Pretty
haftmann@37695: imports Candidates_Pretty
haftmann@24195: begin
haftmann@24195: 
haftmann@37695: lemma [code, code del]: "nat_of_char = nat_of_char" ..
haftmann@37695: lemma [code, code del]: "char_of_nat = char_of_nat" ..
haftmann@37695: 
huffman@47108: declare Quickcheck_Narrowing.one_code_int_code [code del]
huffman@47108: declare Quickcheck_Narrowing.int_of_code [code del]
bulwahn@43317: 
haftmann@37745: subsection {* Check whether generated code compiles *}
haftmann@37745: 
haftmann@37745: text {*
haftmann@37824:   If any of the checks fails, inspect the code generated
haftmann@37824:   by a corresponding @{text export_code} command.
haftmann@37745: *}
haftmann@37745: 
haftmann@40711: export_code _ checking SML OCaml? Haskell? Scala?
haftmann@25616: 
haftmann@24195: end