haftmann@24999
|
1 |
(* Title: HOL/Library/Code_Integer.thy
|
haftmann@24999
|
2 |
Author: Florian Haftmann, TU Muenchen
|
haftmann@24999
|
3 |
*)
|
haftmann@24999
|
4 |
|
haftmann@24999
|
5 |
header {* Pretty integer literals for code generation *}
|
haftmann@24999
|
6 |
|
haftmann@24999
|
7 |
theory Code_Integer
|
haftmann@38205
|
8 |
imports Main Code_Natural
|
haftmann@24999
|
9 |
begin
|
haftmann@24999
|
10 |
|
haftmann@24999
|
11 |
text {*
|
huffman@47978
|
12 |
Representation-ignorant code equations for conversions.
|
huffman@47978
|
13 |
*}
|
huffman@47978
|
14 |
|
huffman@47978
|
15 |
lemma nat_code [code]:
|
huffman@47978
|
16 |
"nat k = (if k \<le> 0 then 0 else
|
huffman@47978
|
17 |
let
|
huffman@47978
|
18 |
(l, j) = divmod_int k 2;
|
huffman@47995
|
19 |
n = nat l;
|
huffman@47995
|
20 |
l' = n + n
|
huffman@47978
|
21 |
in if j = 0 then l' else Suc l')"
|
huffman@47978
|
22 |
proof -
|
huffman@47978
|
23 |
have "2 = nat 2" by simp
|
huffman@47978
|
24 |
show ?thesis
|
huffman@48088
|
25 |
apply (subst mult_2 [symmetric])
|
huffman@47978
|
26 |
apply (auto simp add: Let_def divmod_int_mod_div not_le
|
huffman@47978
|
27 |
nat_div_distrib nat_mult_distrib mult_div_cancel mod_2_not_eq_zero_eq_one_int)
|
huffman@47978
|
28 |
apply (unfold `2 = nat 2`)
|
huffman@47978
|
29 |
apply (subst nat_mod_distrib [symmetric])
|
huffman@47978
|
30 |
apply simp_all
|
huffman@47978
|
31 |
done
|
huffman@47978
|
32 |
qed
|
huffman@47978
|
33 |
|
huffman@47978
|
34 |
lemma (in ring_1) of_int_code:
|
huffman@47978
|
35 |
"of_int k = (if k = 0 then 0
|
huffman@47978
|
36 |
else if k < 0 then - of_int (- k)
|
huffman@47978
|
37 |
else let
|
huffman@47978
|
38 |
(l, j) = divmod_int k 2;
|
huffman@47978
|
39 |
l' = 2 * of_int l
|
huffman@47978
|
40 |
in if j = 0 then l' else l' + 1)"
|
huffman@47978
|
41 |
proof -
|
huffman@47978
|
42 |
from mod_div_equality have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
|
huffman@47978
|
43 |
show ?thesis
|
huffman@47978
|
44 |
by (simp add: Let_def divmod_int_mod_div mod_2_not_eq_zero_eq_one_int
|
huffman@47978
|
45 |
of_int_add [symmetric]) (simp add: * mult_commute)
|
huffman@47978
|
46 |
qed
|
huffman@47978
|
47 |
|
huffman@47978
|
48 |
declare of_int_code [code]
|
huffman@47978
|
49 |
|
huffman@47978
|
50 |
text {*
|
haftmann@24999
|
51 |
HOL numeral expressions are mapped to integer literals
|
haftmann@24999
|
52 |
in target languages, using predefined target language
|
haftmann@24999
|
53 |
operations for abstract integer operations.
|
haftmann@24999
|
54 |
*}
|
haftmann@24999
|
55 |
|
haftmann@24999
|
56 |
code_type int
|
haftmann@24999
|
57 |
(SML "IntInf.int")
|
haftmann@24999
|
58 |
(OCaml "Big'_int.big'_int")
|
haftmann@24999
|
59 |
(Haskell "Integer")
|
haftmann@34899
|
60 |
(Scala "BigInt")
|
haftmann@38299
|
61 |
(Eval "int")
|
haftmann@24999
|
62 |
|
haftmann@39086
|
63 |
code_instance int :: equal
|
haftmann@24999
|
64 |
(Haskell -)
|
haftmann@24999
|
65 |
|
huffman@47978
|
66 |
code_const "0::int"
|
huffman@47978
|
67 |
(SML "0")
|
huffman@47978
|
68 |
(OCaml "Big'_int.zero'_big'_int")
|
huffman@47978
|
69 |
(Haskell "0")
|
huffman@47978
|
70 |
(Scala "BigInt(0)")
|
huffman@47978
|
71 |
|
haftmann@24999
|
72 |
setup {*
|
huffman@47978
|
73 |
fold (Numeral.add_code @{const_name Int.Pos}
|
huffman@47978
|
74 |
false Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"]
|
huffman@47978
|
75 |
*}
|
huffman@47978
|
76 |
|
huffman@47978
|
77 |
setup {*
|
huffman@47978
|
78 |
fold (Numeral.add_code @{const_name Int.Neg}
|
haftmann@34931
|
79 |
true Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"]
|
haftmann@24999
|
80 |
*}
|
haftmann@24999
|
81 |
|
haftmann@24999
|
82 |
code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
|
haftmann@24999
|
83 |
(SML "IntInf.+ ((_), (_))")
|
haftmann@24999
|
84 |
(OCaml "Big'_int.add'_big'_int")
|
haftmann@24999
|
85 |
(Haskell infixl 6 "+")
|
haftmann@34899
|
86 |
(Scala infixl 7 "+")
|
haftmann@38195
|
87 |
(Eval infixl 8 "+")
|
haftmann@24999
|
88 |
|
haftmann@24999
|
89 |
code_const "uminus \<Colon> int \<Rightarrow> int"
|
haftmann@24999
|
90 |
(SML "IntInf.~")
|
haftmann@24999
|
91 |
(OCaml "Big'_int.minus'_big'_int")
|
haftmann@24999
|
92 |
(Haskell "negate")
|
haftmann@34899
|
93 |
(Scala "!(- _)")
|
haftmann@38195
|
94 |
(Eval "~/ _")
|
haftmann@24999
|
95 |
|
haftmann@24999
|
96 |
code_const "op - \<Colon> int \<Rightarrow> int \<Rightarrow> int"
|
haftmann@24999
|
97 |
(SML "IntInf.- ((_), (_))")
|
haftmann@24999
|
98 |
(OCaml "Big'_int.sub'_big'_int")
|
haftmann@24999
|
99 |
(Haskell infixl 6 "-")
|
haftmann@34899
|
100 |
(Scala infixl 7 "-")
|
haftmann@38195
|
101 |
(Eval infixl 8 "-")
|
haftmann@24999
|
102 |
|
huffman@47978
|
103 |
code_const Int.dup
|
huffman@47978
|
104 |
(SML "IntInf.*/ (2,/ (_))")
|
huffman@47978
|
105 |
(OCaml "Big'_int.mult'_big'_int/ 2")
|
huffman@47978
|
106 |
(Haskell "!(2 * _)")
|
huffman@47978
|
107 |
(Scala "!(2 * _)")
|
huffman@47978
|
108 |
(Eval "!(2 * _)")
|
huffman@47978
|
109 |
|
huffman@47978
|
110 |
code_const Int.sub
|
huffman@47978
|
111 |
(SML "!(raise/ Fail/ \"sub\")")
|
huffman@47978
|
112 |
(OCaml "failwith/ \"sub\"")
|
huffman@47978
|
113 |
(Haskell "error/ \"sub\"")
|
haftmann@49088
|
114 |
(Scala "!sys.error(\"sub\")")
|
huffman@47978
|
115 |
|
haftmann@24999
|
116 |
code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"
|
haftmann@24999
|
117 |
(SML "IntInf.* ((_), (_))")
|
haftmann@24999
|
118 |
(OCaml "Big'_int.mult'_big'_int")
|
haftmann@24999
|
119 |
(Haskell infixl 7 "*")
|
haftmann@34899
|
120 |
(Scala infixl 8 "*")
|
haftmann@38195
|
121 |
(Eval infixl 9 "*")
|
haftmann@24999
|
122 |
|
haftmann@29873
|
123 |
code_const pdivmod
|
haftmann@34899
|
124 |
(SML "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)")
|
haftmann@34899
|
125 |
(OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)")
|
haftmann@34931
|
126 |
(Haskell "divMod/ (abs _)/ (abs _)")
|
haftmann@38195
|
127 |
(Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
|
haftmann@38195
|
128 |
(Eval "Integer.div'_mod/ (abs _)/ (abs _)")
|
haftmann@29873
|
129 |
|
haftmann@39086
|
130 |
code_const "HOL.equal \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
|
haftmann@24999
|
131 |
(SML "!((_ : IntInf.int) = _)")
|
haftmann@24999
|
132 |
(OCaml "Big'_int.eq'_big'_int")
|
haftmann@39499
|
133 |
(Haskell infix 4 "==")
|
haftmann@34899
|
134 |
(Scala infixl 5 "==")
|
haftmann@38195
|
135 |
(Eval infixl 6 "=")
|
haftmann@24999
|
136 |
|
haftmann@24999
|
137 |
code_const "op \<le> \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
|
haftmann@24999
|
138 |
(SML "IntInf.<= ((_), (_))")
|
haftmann@24999
|
139 |
(OCaml "Big'_int.le'_big'_int")
|
haftmann@24999
|
140 |
(Haskell infix 4 "<=")
|
haftmann@34899
|
141 |
(Scala infixl 4 "<=")
|
haftmann@38195
|
142 |
(Eval infixl 6 "<=")
|
haftmann@24999
|
143 |
|
haftmann@24999
|
144 |
code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
|
haftmann@24999
|
145 |
(SML "IntInf.< ((_), (_))")
|
haftmann@24999
|
146 |
(OCaml "Big'_int.lt'_big'_int")
|
haftmann@24999
|
147 |
(Haskell infix 4 "<")
|
haftmann@38195
|
148 |
(Scala infixl 4 "<")
|
haftmann@38195
|
149 |
(Eval infixl 6 "<")
|
haftmann@24999
|
150 |
|
haftmann@31205
|
151 |
code_const Code_Numeral.int_of
|
haftmann@31192
|
152 |
(SML "IntInf.fromInt")
|
haftmann@31377
|
153 |
(OCaml "_")
|
haftmann@49446
|
154 |
(Haskell "Prelude.toInteger")
|
haftmann@38195
|
155 |
(Scala "!_.as'_BigInt")
|
haftmann@38195
|
156 |
(Eval "_")
|
haftmann@24999
|
157 |
|
haftmann@32657
|
158 |
code_const "Code_Evaluation.term_of \<Colon> int \<Rightarrow> term"
|
haftmann@31192
|
159 |
(Eval "HOLogic.mk'_number/ HOLogic.intT")
|
haftmann@28228
|
160 |
|
huffman@47978
|
161 |
end
|