author | haftmann |
Wed, 14 Jul 2010 15:49:29 +0200 | |
changeset 37824 | 365e37fe93f3 |
parent 37819 | 000049335247 |
child 37825 | adc1143bc1a8 |
permissions | -rw-r--r-- |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
1 |
|
31378 | 2 |
(* Author: Florian Haftmann, TU Muenchen *) |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
3 |
|
31378 | 4 |
header {* Pervasive test of code generator *} |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
5 |
|
37695
71e84a203c19
introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
34306
diff
changeset
|
6 |
theory Generate |
71e84a203c19
introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
34306
diff
changeset
|
7 |
imports Candidates |
31378 | 8 |
begin |
24430 | 9 |
|
37745
6315b6426200
checking generated code for various target languages
haftmann
parents:
37695
diff
changeset
|
10 |
subsection {* Check whether generated code compiles *} |
6315b6426200
checking generated code for various target languages
haftmann
parents:
37695
diff
changeset
|
11 |
|
6315b6426200
checking generated code for various target languages
haftmann
parents:
37695
diff
changeset
|
12 |
text {* |
37824 | 13 |
If any of the checks fails, inspect the code generated |
14 |
by a corresponding @{text export_code} command. |
|
37745
6315b6426200
checking generated code for various target languages
haftmann
parents:
37695
diff
changeset
|
15 |
*} |
6315b6426200
checking generated code for various target languages
haftmann
parents:
37695
diff
changeset
|
16 |
|
37824 | 17 |
export_code "*" checking SML OCaml Haskell Scala |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
18 |
|
23266 | 19 |
end |