src/HOL/Codegenerator_Test/Generate_Pretty.thy
author Christian Sternagel
Thu Aug 30 15:44:03 2012 +0900 (2012-08-30)
changeset 49093 fdc301f592c4
parent 47108 2a1953f0d20d
child 50629 264ece81df93
permissions -rw-r--r--
forgot to add lemmas
haftmann@31378
     1
haftmann@31378
     2
(* Author: Florian Haftmann, TU Muenchen *)
haftmann@24195
     3
haftmann@31378
     4
header {* Pervasive test of code generator using pretty literals *}
haftmann@24195
     5
haftmann@37695
     6
theory Generate_Pretty
haftmann@37695
     7
imports Candidates_Pretty
haftmann@24195
     8
begin
haftmann@24195
     9
haftmann@37695
    10
lemma [code, code del]: "nat_of_char = nat_of_char" ..
haftmann@37695
    11
lemma [code, code del]: "char_of_nat = char_of_nat" ..
haftmann@37695
    12
huffman@47108
    13
declare Quickcheck_Narrowing.one_code_int_code [code del]
huffman@47108
    14
declare Quickcheck_Narrowing.int_of_code [code del]
bulwahn@43317
    15
haftmann@37745
    16
subsection {* Check whether generated code compiles *}
haftmann@37745
    17
haftmann@37745
    18
text {*
haftmann@37824
    19
  If any of the checks fails, inspect the code generated
haftmann@37824
    20
  by a corresponding @{text export_code} command.
haftmann@37745
    21
*}
haftmann@37745
    22
haftmann@40711
    23
export_code _ checking SML OCaml? Haskell? Scala?
haftmann@25616
    24
haftmann@24195
    25
end