author | haftmann |
Wed, 14 Jul 2010 15:49:29 +0200 | |
changeset 37824 | 365e37fe93f3 |
parent 37819 | 000049335247 |
child 37825 | adc1143bc1a8 |
permissions | -rw-r--r-- |
31378 | 1 |
|
2 |
(* Author: Florian Haftmann, TU Muenchen *) |
|
24195 | 3 |
|
31378 | 4 |
header {* Pervasive test of code generator using pretty literals *} |
24195 | 5 |
|
37695
71e84a203c19
introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37475
diff
changeset
|
6 |
theory Generate_Pretty |
71e84a203c19
introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37475
diff
changeset
|
7 |
imports Candidates_Pretty |
24195 | 8 |
begin |
9 |
||
37695
71e84a203c19
introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37475
diff
changeset
|
10 |
lemma [code, code del]: "nat_of_char = nat_of_char" .. |
71e84a203c19
introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37475
diff
changeset
|
11 |
lemma [code, code del]: "char_of_nat = char_of_nat" .. |
71e84a203c19
introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37475
diff
changeset
|
12 |
lemma [code, code del]: "(less_eq :: char \<Rightarrow> _) = less_eq" .. |
71e84a203c19
introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37475
diff
changeset
|
13 |
lemma [code, code del]: "(less :: char \<Rightarrow> _) = less" .. |
71e84a203c19
introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37475
diff
changeset
|
14 |
|
37745
6315b6426200
checking generated code for various target languages
haftmann
parents:
37695
diff
changeset
|
15 |
subsection {* Check whether generated code compiles *} |
6315b6426200
checking generated code for various target languages
haftmann
parents:
37695
diff
changeset
|
16 |
|
6315b6426200
checking generated code for various target languages
haftmann
parents:
37695
diff
changeset
|
17 |
text {* |
37824 | 18 |
If any of the checks fails, inspect the code generated |
19 |
by a corresponding @{text export_code} command. |
|
37745
6315b6426200
checking generated code for various target languages
haftmann
parents:
37695
diff
changeset
|
20 |
*} |
6315b6426200
checking generated code for various target languages
haftmann
parents:
37695
diff
changeset
|
21 |
|
37824 | 22 |
export_code "*" checking SML OCaml Haskell Scala |
25616 | 23 |
|
24195 | 24 |
end |