|
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 |
|
9 imports IntArith Code_Index |
|
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} |
|
29 @{const_name Numeral.B0} @{const_name Numeral.B1} |
|
30 @{const_name Numeral.Pls} @{const_name Numeral.Min} |
|
31 @{const_name Numeral.Bit} |
|
32 ) ["SML", "OCaml", "Haskell"] |
|
33 *} |
|
34 |
|
35 code_const "Numeral.Pls" and "Numeral.Min" and "Numeral.Bit" |
|
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 |
|
46 code_const Numeral.pred |
|
47 (SML "IntInf.- ((_), 1)") |
|
48 (OCaml "Big'_int.pred'_big'_int") |
|
49 (Haskell "!(_/ -/ 1)") |
|
50 |
|
51 code_const Numeral.succ |
|
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_const index_of_int and int_of_index |
|
92 (SML "IntInf.toInt" and "IntInf.fromInt") |
|
93 (OCaml "Big'_int.int'_of'_big'_int" and "Big'_int.big'_int'_of'_int") |
|
94 (Haskell "_" and "_") |
|
95 |
|
96 code_reserved SML IntInf |
|
97 code_reserved OCaml Big_int |
|
98 |
|
99 end |