author | haftmann |
Mon, 07 Jul 2008 08:47:17 +0200 | |
changeset 27487 | c8a6ce181805 |
parent 27368 | 9f90ac19e32b |
child 28228 | 7ebe8dc06cbb |
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 |
|
27487 | 9 |
imports Plain "~~/src/HOL/Presburger" |
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 |
||
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26009
diff
changeset
|
31 |
code_const "Int.Pls" and "Int.Min" and "Int.Bit0" and "Int.Bit1" |
24999 | 32 |
(SML "raise/ Fail/ \"Pls\"" |
33 |
and "raise/ Fail/ \"Min\"" |
|
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26009
diff
changeset
|
34 |
and "!((_);/ raise/ Fail/ \"Bit0\")" |
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26009
diff
changeset
|
35 |
and "!((_);/ raise/ Fail/ \"Bit1\")") |
24999 | 36 |
(OCaml "failwith/ \"Pls\"" |
37 |
and "failwith/ \"Min\"" |
|
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26009
diff
changeset
|
38 |
and "!((_);/ failwith/ \"Bit0\")" |
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26009
diff
changeset
|
39 |
and "!((_);/ failwith/ \"Bit1\")") |
24999 | 40 |
(Haskell "error/ \"Pls\"" |
41 |
and "error/ \"Min\"" |
|
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26009
diff
changeset
|
42 |
and "error/ \"Bit0\"" |
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26009
diff
changeset
|
43 |
and "error/ \"Bit1\"") |
24999 | 44 |
|
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25767
diff
changeset
|
45 |
code_const Int.pred |
24999 | 46 |
(SML "IntInf.- ((_), 1)") |
47 |
(OCaml "Big'_int.pred'_big'_int") |
|
48 |
(Haskell "!(_/ -/ 1)") |
|
49 |
||
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25767
diff
changeset
|
50 |
code_const Int.succ |
24999 | 51 |
(SML "IntInf.+ ((_), 1)") |
52 |
(OCaml "Big'_int.succ'_big'_int") |
|
53 |
(Haskell "!(_/ +/ 1)") |
|
54 |
||
55 |
code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int" |
|
56 |
(SML "IntInf.+ ((_), (_))") |
|
57 |
(OCaml "Big'_int.add'_big'_int") |
|
58 |
(Haskell infixl 6 "+") |
|
59 |
||
60 |
code_const "uminus \<Colon> int \<Rightarrow> int" |
|
61 |
(SML "IntInf.~") |
|
62 |
(OCaml "Big'_int.minus'_big'_int") |
|
63 |
(Haskell "negate") |
|
64 |
||
65 |
code_const "op - \<Colon> int \<Rightarrow> int \<Rightarrow> int" |
|
66 |
(SML "IntInf.- ((_), (_))") |
|
67 |
(OCaml "Big'_int.sub'_big'_int") |
|
68 |
(Haskell infixl 6 "-") |
|
69 |
||
70 |
code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int" |
|
71 |
(SML "IntInf.* ((_), (_))") |
|
72 |
(OCaml "Big'_int.mult'_big'_int") |
|
73 |
(Haskell infixl 7 "*") |
|
74 |
||
75 |
code_const "op = \<Colon> int \<Rightarrow> int \<Rightarrow> bool" |
|
76 |
(SML "!((_ : IntInf.int) = _)") |
|
77 |
(OCaml "Big'_int.eq'_big'_int") |
|
78 |
(Haskell infixl 4 "==") |
|
79 |
||
80 |
code_const "op \<le> \<Colon> int \<Rightarrow> int \<Rightarrow> bool" |
|
81 |
(SML "IntInf.<= ((_), (_))") |
|
82 |
(OCaml "Big'_int.le'_big'_int") |
|
83 |
(Haskell infix 4 "<=") |
|
84 |
||
85 |
code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool" |
|
86 |
(SML "IntInf.< ((_), (_))") |
|
87 |
(OCaml "Big'_int.lt'_big'_int") |
|
88 |
(Haskell infix 4 "<") |
|
89 |
||
90 |
code_reserved SML IntInf |
|
91 |
code_reserved OCaml Big_int |
|
92 |
||
93 |
end |