author | haftmann |
Tue, 15 Jan 2008 16:19:23 +0100 | |
changeset 25919 | 8b1c0d434824 |
parent 25767 | 852bce03412a |
child 25928 | 042e877d9841 |
permissions | -rw-r--r-- |
24999 | 1 |
(* Title: HOL/Library/Code_Integer.thy |
2 |
ID: $Id$ |
|
3 |
Author: Florian Haftmann, TU Muenchen |
|
4 |
*) |
|
5 |
||
6 |
header {* Pretty integer literals for code generation *} |
|
7 |
||
8 |
theory Code_Integer |
|
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25767
diff
changeset
|
9 |
imports Int |
24999 | 10 |
begin |
11 |
||
12 |
text {* |
|
13 |
HOL numeral expressions are mapped to integer literals |
|
14 |
in target languages, using predefined target language |
|
15 |
operations for abstract integer operations. |
|
16 |
*} |
|
17 |
||
18 |
code_type int |
|
19 |
(SML "IntInf.int") |
|
20 |
(OCaml "Big'_int.big'_int") |
|
21 |
(Haskell "Integer") |
|
22 |
||
23 |
code_instance int :: eq |
|
24 |
(Haskell -) |
|
25 |
||
26 |
setup {* |
|
27 |
fold (fn target => CodeTarget.add_pretty_numeral target true |
|
28 |
@{const_name number_int_inst.number_of_int} |
|
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25767
diff
changeset
|
29 |
@{const_name Int.B0} @{const_name Int.B1} |
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25767
diff
changeset
|
30 |
@{const_name Int.Pls} @{const_name Int.Min} |
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25767
diff
changeset
|
31 |
@{const_name Int.Bit} |
24999 | 32 |
) ["SML", "OCaml", "Haskell"] |
33 |
*} |
|
34 |
||
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25767
diff
changeset
|
35 |
code_const "Int.Pls" and "Int.Min" and "Int.Bit" |
24999 | 36 |
(SML "raise/ Fail/ \"Pls\"" |
37 |
and "raise/ Fail/ \"Min\"" |
|
38 |
and "!((_);/ (_);/ raise/ Fail/ \"Bit\")") |
|
39 |
(OCaml "failwith/ \"Pls\"" |
|
40 |
and "failwith/ \"Min\"" |
|
41 |
and "!((_);/ (_);/ failwith/ \"Bit\")") |
|
42 |
(Haskell "error/ \"Pls\"" |
|
43 |
and "error/ \"Min\"" |
|
44 |
and "error/ \"Bit\"") |
|
45 |
||
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25767
diff
changeset
|
46 |
code_const Int.pred |
24999 | 47 |
(SML "IntInf.- ((_), 1)") |
48 |
(OCaml "Big'_int.pred'_big'_int") |
|
49 |
(Haskell "!(_/ -/ 1)") |
|
50 |
||
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25767
diff
changeset
|
51 |
code_const Int.succ |
24999 | 52 |
(SML "IntInf.+ ((_), 1)") |
53 |
(OCaml "Big'_int.succ'_big'_int") |
|
54 |
(Haskell "!(_/ +/ 1)") |
|
55 |
||
56 |
code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int" |
|
57 |
(SML "IntInf.+ ((_), (_))") |
|
58 |
(OCaml "Big'_int.add'_big'_int") |
|
59 |
(Haskell infixl 6 "+") |
|
60 |
||
61 |
code_const "uminus \<Colon> int \<Rightarrow> int" |
|
62 |
(SML "IntInf.~") |
|
63 |
(OCaml "Big'_int.minus'_big'_int") |
|
64 |
(Haskell "negate") |
|
65 |
||
66 |
code_const "op - \<Colon> int \<Rightarrow> int \<Rightarrow> int" |
|
67 |
(SML "IntInf.- ((_), (_))") |
|
68 |
(OCaml "Big'_int.sub'_big'_int") |
|
69 |
(Haskell infixl 6 "-") |
|
70 |
||
71 |
code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int" |
|
72 |
(SML "IntInf.* ((_), (_))") |
|
73 |
(OCaml "Big'_int.mult'_big'_int") |
|
74 |
(Haskell infixl 7 "*") |
|
75 |
||
76 |
code_const "op = \<Colon> int \<Rightarrow> int \<Rightarrow> bool" |
|
77 |
(SML "!((_ : IntInf.int) = _)") |
|
78 |
(OCaml "Big'_int.eq'_big'_int") |
|
79 |
(Haskell infixl 4 "==") |
|
80 |
||
81 |
code_const "op \<le> \<Colon> int \<Rightarrow> int \<Rightarrow> bool" |
|
82 |
(SML "IntInf.<= ((_), (_))") |
|
83 |
(OCaml "Big'_int.le'_big'_int") |
|
84 |
(Haskell infix 4 "<=") |
|
85 |
||
86 |
code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool" |
|
87 |
(SML "IntInf.< ((_), (_))") |
|
88 |
(OCaml "Big'_int.lt'_big'_int") |
|
89 |
(Haskell infix 4 "<") |
|
90 |
||
91 |
code_reserved SML IntInf |
|
92 |
code_reserved OCaml Big_int |
|
93 |
||
94 |
end |