author | haftmann |
Mon, 21 Jan 2008 08:43:27 +0100 | |
changeset 25928 | 042e877d9841 |
parent 25919 | 8b1c0d434824 |
child 26009 | b6a64fe38634 |
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 {* |
|
25928 | 27 |
fold (Numeral.add_code @{const_name number_int_inst.number_of_int} |
28 |
true true) ["SML", "OCaml", "Haskell"] |
|
24999 | 29 |
*} |
30 |
||
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25767
diff
changeset
|
31 |
code_const "Int.Pls" and "Int.Min" and "Int.Bit" |
24999 | 32 |
(SML "raise/ Fail/ \"Pls\"" |
33 |
and "raise/ Fail/ \"Min\"" |
|
34 |
and "!((_);/ (_);/ raise/ Fail/ \"Bit\")") |
|
35 |
(OCaml "failwith/ \"Pls\"" |
|
36 |
and "failwith/ \"Min\"" |
|
37 |
and "!((_);/ (_);/ failwith/ \"Bit\")") |
|
38 |
(Haskell "error/ \"Pls\"" |
|
39 |
and "error/ \"Min\"" |
|
40 |
and "error/ \"Bit\"") |
|
41 |
||
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25767
diff
changeset
|
42 |
code_const Int.pred |
24999 | 43 |
(SML "IntInf.- ((_), 1)") |
44 |
(OCaml "Big'_int.pred'_big'_int") |
|
45 |
(Haskell "!(_/ -/ 1)") |
|
46 |
||
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25767
diff
changeset
|
47 |
code_const Int.succ |
24999 | 48 |
(SML "IntInf.+ ((_), 1)") |
49 |
(OCaml "Big'_int.succ'_big'_int") |
|
50 |
(Haskell "!(_/ +/ 1)") |
|
51 |
||
52 |
code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int" |
|
53 |
(SML "IntInf.+ ((_), (_))") |
|
54 |
(OCaml "Big'_int.add'_big'_int") |
|
55 |
(Haskell infixl 6 "+") |
|
56 |
||
57 |
code_const "uminus \<Colon> int \<Rightarrow> int" |
|
58 |
(SML "IntInf.~") |
|
59 |
(OCaml "Big'_int.minus'_big'_int") |
|
60 |
(Haskell "negate") |
|
61 |
||
62 |
code_const "op - \<Colon> int \<Rightarrow> int \<Rightarrow> int" |
|
63 |
(SML "IntInf.- ((_), (_))") |
|
64 |
(OCaml "Big'_int.sub'_big'_int") |
|
65 |
(Haskell infixl 6 "-") |
|
66 |
||
67 |
code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int" |
|
68 |
(SML "IntInf.* ((_), (_))") |
|
69 |
(OCaml "Big'_int.mult'_big'_int") |
|
70 |
(Haskell infixl 7 "*") |
|
71 |
||
72 |
code_const "op = \<Colon> int \<Rightarrow> int \<Rightarrow> bool" |
|
73 |
(SML "!((_ : IntInf.int) = _)") |
|
74 |
(OCaml "Big'_int.eq'_big'_int") |
|
75 |
(Haskell infixl 4 "==") |
|
76 |
||
77 |
code_const "op \<le> \<Colon> int \<Rightarrow> int \<Rightarrow> bool" |
|
78 |
(SML "IntInf.<= ((_), (_))") |
|
79 |
(OCaml "Big'_int.le'_big'_int") |
|
80 |
(Haskell infix 4 "<=") |
|
81 |
||
82 |
code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool" |
|
83 |
(SML "IntInf.< ((_), (_))") |
|
84 |
(OCaml "Big'_int.lt'_big'_int") |
|
85 |
(Haskell infix 4 "<") |
|
86 |
||
87 |
code_reserved SML IntInf |
|
88 |
code_reserved OCaml Big_int |
|
89 |
||
90 |
end |