author | bulwahn |
Fri, 18 Mar 2011 18:19:42 +0100 (2011-03-18) | |
changeset 42031 | 2de57cda5b24 |
parent 40711 | 81bc73585eec |
child 50629 | 264ece81df93 |
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 |
|
40711
81bc73585eec
globbing constant expressions use more idiomatic underscore rather than star
haftmann
parents:
37825
diff
changeset
|
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 |