author | haftmann |
Fri, 25 Jan 2008 14:53:56 +0100 | |
changeset 25963 | 07e08dad8a77 |
parent 24810 | 862b71696efe |
child 28335 | 25326092cf9a |
permissions | -rw-r--r-- |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
1 |
(* ID: $Id$ |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
2 |
Author: Florian Haftmann, TU Muenchen |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
3 |
*) |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
4 |
|
21877
e871f57b1adb
now testing executable content of nearly all HOL
haftmann
parents:
21545
diff
changeset
|
5 |
header {* Tests and examples for code generator *} |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
6 |
|
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
7 |
theory Codegenerator |
21911
e29bcab0c81c
added OCaml code generation (without dictionaries)
haftmann
parents:
21898
diff
changeset
|
8 |
imports ExecutableContent |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
9 |
begin |
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
10 |
|
24432 | 11 |
ML {* (*FIXME get rid of this*) |
24430 | 12 |
nonfix union; |
13 |
nonfix inter; |
|
24718 | 14 |
nonfix upto; |
24430 | 15 |
*} |
16 |
||
24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24348
diff
changeset
|
17 |
export_code * in SML module_name CodegenTest |
24810 | 18 |
in OCaml module_name CodegenTest file - |
23811 | 19 |
in Haskell file - |
19281
b411f25fff25
added example for operational classes and code generator
haftmann
parents:
diff
changeset
|
20 |
|
24432 | 21 |
ML {* |
22 |
infix union; |
|
23 |
infix inter; |
|
24718 | 24 |
infix 4 upto; |
24432 | 25 |
*} |
26 |
||
23266 | 27 |
end |