src/HOL/Codegenerator_Test/Generate_Pretty.thy
author huffman
Sun Mar 25 20:15:39 2012 +0200 (2012-03-25 ago)
changeset 47108 2a1953f0d20d
parent 43317 f9283eb3a4bf
child 50629 264ece81df93
permissions -rw-r--r--
merged fork with new numeral representation (see NEWS)
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