author | haftmann |
Sat, 05 Jul 2014 11:01:53 +0200 | |
changeset 57514 | bdc2c6b40bf2 |
parent 54228 | 229282d53781 |
child 58678 | 398e05aa84d4 |
permissions | -rw-r--r-- |
31378 | 1 |
|
2 |
(* Author: Florian Haftmann, TU Muenchen *) |
|
24195 | 3 |
|
51161
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51143
diff
changeset
|
4 |
header {* Pervasive test of code generator *} |
24195 | 5 |
|
51161
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51143
diff
changeset
|
6 |
theory Generate_Binary_Nat |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51143
diff
changeset
|
7 |
imports |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51143
diff
changeset
|
8 |
Candidates |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51143
diff
changeset
|
9 |
"~~/src/HOL/Library/AList_Mapping" |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51143
diff
changeset
|
10 |
"~~/src/HOL/Library/Finite_Lattice" |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51143
diff
changeset
|
11 |
"~~/src/HOL/Library/Code_Binary_Nat" |
24195 | 12 |
begin |
13 |
||
37745
6315b6426200
checking generated code for various target languages
haftmann
parents:
37695
diff
changeset
|
14 |
text {* |
37824 | 15 |
If any of the checks fails, inspect the code generated |
16 |
by a corresponding @{text export_code} command. |
|
37745
6315b6426200
checking generated code for various target languages
haftmann
parents:
37695
diff
changeset
|
17 |
*} |
6315b6426200
checking generated code for various target languages
haftmann
parents:
37695
diff
changeset
|
18 |
|
54228 | 19 |
text {* Formal joining of hierarchy of implicit definitions in Scala *} |
20 |
||
21 |
class semiring_numeral_even_odd = semiring_numeral_div + even_odd |
|
22 |
||
23 |
instance nat :: semiring_numeral_even_odd .. |
|
24 |
||
25 |
definition semiring_numeral_even_odd :: "'a itself \<Rightarrow> 'a::semiring_numeral_even_odd" |
|
26 |
where |
|
27 |
"semiring_numeral_even_odd TYPE('a) = undefined" |
|
28 |
||
29 |
definition semiring_numeral_even_odd_nat :: "nat itself \<Rightarrow> nat" |
|
30 |
where |
|
31 |
"semiring_numeral_even_odd_nat = semiring_numeral_even_odd" |
|
32 |
||
33 |
export_code _ checking SML OCaml? Haskell? Scala |
|
25616 | 34 |
|
24195 | 35 |
end |