author | blanchet |
Tue, 07 Jun 2011 11:13:52 +0200 | |
changeset 43236 | a1a0dcbeb785 |
parent 42842 | 6ef538f6a8ab |
child 43317 | f9283eb3a4bf |
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 |
|
37745
6315b6426200
checking generated code for various target languages
haftmann
parents:
37695
diff
changeset
|
13 |
subsection {* Check whether generated code compiles *} |
6315b6426200
checking generated code for various target languages
haftmann
parents:
37695
diff
changeset
|
14 |
|
6315b6426200
checking generated code for various target languages
haftmann
parents:
37695
diff
changeset
|
15 |
text {* |
37824 | 16 |
If any of the checks fails, inspect the code generated |
17 |
by a corresponding @{text export_code} command. |
|
37745
6315b6426200
checking generated code for various target languages
haftmann
parents:
37695
diff
changeset
|
18 |
*} |
6315b6426200
checking generated code for various target languages
haftmann
parents:
37695
diff
changeset
|
19 |
|
40711
81bc73585eec
globbing constant expressions use more idiomatic underscore rather than star
haftmann
parents:
37825
diff
changeset
|
20 |
export_code _ checking SML OCaml? Haskell? Scala? |
25616 | 21 |
|
24195 | 22 |
end |