haftmann@23854
|
1 |
(* Title: HOL/Library/Efficient_Nat.thy
|
haftmann@25931
|
2 |
Author: Stefan Berghofer, Florian Haftmann, TU Muenchen
|
haftmann@23854
|
3 |
*)
|
haftmann@23854
|
4 |
|
haftmann@25931
|
5 |
header {* Implementation of natural numbers by target-language integers *}
|
haftmann@23854
|
6 |
|
haftmann@23854
|
7 |
theory Efficient_Nat
|
huffman@47978
|
8 |
imports Code_Nat Code_Integer Main
|
haftmann@23854
|
9 |
begin
|
haftmann@23854
|
10 |
|
haftmann@23854
|
11 |
text {*
|
huffman@47978
|
12 |
The efficiency of the generated code for natural numbers can be improved
|
haftmann@25931
|
13 |
drastically by implementing natural numbers by target-language
|
haftmann@25931
|
14 |
integers. To do this, just include this theory.
|
haftmann@23854
|
15 |
*}
|
haftmann@23854
|
16 |
|
huffman@47978
|
17 |
subsection {* Target language fundamentals *}
|
haftmann@25931
|
18 |
|
haftmann@25931
|
19 |
text {*
|
haftmann@25967
|
20 |
For ML, we map @{typ nat} to target language integers, where we
|
haftmann@34899
|
21 |
ensure that values are always non-negative.
|
haftmann@25931
|
22 |
*}
|
haftmann@25931
|
23 |
|
haftmann@25931
|
24 |
code_type nat
|
haftmann@27496
|
25 |
(SML "IntInf.int")
|
haftmann@25931
|
26 |
(OCaml "Big'_int.big'_int")
|
haftmann@38195
|
27 |
(Eval "int")
|
haftmann@25931
|
28 |
|
haftmann@25931
|
29 |
text {*
|
bulwahn@46056
|
30 |
For Haskell and Scala we define our own @{typ nat} type. The reason
|
haftmann@34899
|
31 |
is that we have to distinguish type class instances for @{typ nat}
|
haftmann@34899
|
32 |
and @{typ int}.
|
haftmann@25967
|
33 |
*}
|
haftmann@25967
|
34 |
|
haftmann@39007
|
35 |
code_include Haskell "Nat"
|
haftmann@39007
|
36 |
{*newtype Nat = Nat Integer deriving (Eq, Show, Read);
|
haftmann@25967
|
37 |
|
haftmann@25967
|
38 |
instance Num Nat where {
|
haftmann@25967
|
39 |
fromInteger k = Nat (if k >= 0 then k else 0);
|
haftmann@25967
|
40 |
Nat n + Nat m = Nat (n + m);
|
haftmann@25967
|
41 |
Nat n - Nat m = fromInteger (n - m);
|
haftmann@25967
|
42 |
Nat n * Nat m = Nat (n * m);
|
haftmann@25967
|
43 |
abs n = n;
|
haftmann@25967
|
44 |
signum _ = 1;
|
haftmann@25967
|
45 |
negate n = error "negate Nat";
|
haftmann@25967
|
46 |
};
|
haftmann@25967
|
47 |
|
haftmann@25967
|
48 |
instance Ord Nat where {
|
haftmann@25967
|
49 |
Nat n <= Nat m = n <= m;
|
haftmann@25967
|
50 |
Nat n < Nat m = n < m;
|
haftmann@25967
|
51 |
};
|
haftmann@25967
|
52 |
|
haftmann@25967
|
53 |
instance Real Nat where {
|
haftmann@25967
|
54 |
toRational (Nat n) = toRational n;
|
haftmann@25967
|
55 |
};
|
haftmann@25967
|
56 |
|
haftmann@25967
|
57 |
instance Enum Nat where {
|
haftmann@25967
|
58 |
toEnum k = fromInteger (toEnum k);
|
haftmann@25967
|
59 |
fromEnum (Nat n) = fromEnum n;
|
haftmann@25967
|
60 |
};
|
haftmann@25967
|
61 |
|
haftmann@25967
|
62 |
instance Integral Nat where {
|
haftmann@25967
|
63 |
toInteger (Nat n) = n;
|
haftmann@25967
|
64 |
divMod n m = quotRem n m;
|
haftmann@38195
|
65 |
quotRem (Nat n) (Nat m)
|
haftmann@38195
|
66 |
| (m == 0) = (0, Nat n)
|
haftmann@38195
|
67 |
| otherwise = (Nat k, Nat l) where (k, l) = quotRem n m;
|
haftmann@25967
|
68 |
};
|
haftmann@25967
|
69 |
*}
|
haftmann@25967
|
70 |
|
haftmann@25967
|
71 |
code_reserved Haskell Nat
|
haftmann@25967
|
72 |
|
haftmann@39007
|
73 |
code_include Scala "Nat"
|
haftmann@39194
|
74 |
{*object Nat {
|
haftmann@34899
|
75 |
|
haftmann@34899
|
76 |
def apply(numeral: BigInt): Nat = new Nat(numeral max 0)
|
haftmann@34899
|
77 |
def apply(numeral: Int): Nat = Nat(BigInt(numeral))
|
haftmann@34899
|
78 |
def apply(numeral: String): Nat = Nat(BigInt(numeral))
|
haftmann@34899
|
79 |
|
haftmann@34899
|
80 |
}
|
haftmann@34899
|
81 |
|
haftmann@34899
|
82 |
class Nat private(private val value: BigInt) {
|
haftmann@34899
|
83 |
|
haftmann@34899
|
84 |
override def hashCode(): Int = this.value.hashCode()
|
haftmann@34899
|
85 |
|
haftmann@34899
|
86 |
override def equals(that: Any): Boolean = that match {
|
haftmann@34899
|
87 |
case that: Nat => this equals that
|
haftmann@34899
|
88 |
case _ => false
|
haftmann@34899
|
89 |
}
|
haftmann@34899
|
90 |
|
haftmann@34899
|
91 |
override def toString(): String = this.value.toString
|
haftmann@34899
|
92 |
|
haftmann@34899
|
93 |
def equals(that: Nat): Boolean = this.value == that.value
|
haftmann@34899
|
94 |
|
haftmann@34899
|
95 |
def as_BigInt: BigInt = this.value
|
haftmann@40014
|
96 |
def as_Int: Int = if (this.value >= scala.Int.MinValue && this.value <= scala.Int.MaxValue)
|
haftmann@34931
|
97 |
this.value.intValue
|
haftmann@38206
|
98 |
else error("Int value out of range: " + this.value.toString)
|
haftmann@34899
|
99 |
|
haftmann@34899
|
100 |
def +(that: Nat): Nat = new Nat(this.value + that.value)
|
haftmann@37222
|
101 |
def -(that: Nat): Nat = Nat(this.value - that.value)
|
haftmann@34899
|
102 |
def *(that: Nat): Nat = new Nat(this.value * that.value)
|
haftmann@34899
|
103 |
|
haftmann@34899
|
104 |
def /%(that: Nat): (Nat, Nat) = if (that.value == 0) (new Nat(0), this)
|
haftmann@34899
|
105 |
else {
|
haftmann@34899
|
106 |
val (k, l) = this.value /% that.value
|
haftmann@34899
|
107 |
(new Nat(k), new Nat(l))
|
haftmann@34899
|
108 |
}
|
haftmann@34899
|
109 |
|
haftmann@34899
|
110 |
def <=(that: Nat): Boolean = this.value <= that.value
|
haftmann@34899
|
111 |
|
haftmann@34899
|
112 |
def <(that: Nat): Boolean = this.value < that.value
|
haftmann@34899
|
113 |
|
haftmann@34899
|
114 |
}
|
haftmann@34899
|
115 |
*}
|
haftmann@34899
|
116 |
|
haftmann@34899
|
117 |
code_reserved Scala Nat
|
haftmann@34899
|
118 |
|
haftmann@25967
|
119 |
code_type nat
|
haftmann@29730
|
120 |
(Haskell "Nat.Nat")
|
haftmann@39194
|
121 |
(Scala "Nat")
|
haftmann@25967
|
122 |
|
haftmann@39086
|
123 |
code_instance nat :: equal
|
haftmann@25967
|
124 |
(Haskell -)
|
haftmann@25967
|
125 |
|
haftmann@25931
|
126 |
setup {*
|
huffman@47978
|
127 |
fold (Numeral.add_code @{const_name nat_of_num}
|
haftmann@38195
|
128 |
false Code_Printer.literal_positive_numeral) ["SML", "OCaml", "Haskell", "Scala"]
|
haftmann@25931
|
129 |
*}
|
haftmann@25931
|
130 |
|
huffman@47978
|
131 |
code_const "0::nat"
|
huffman@47978
|
132 |
(SML "0")
|
huffman@47978
|
133 |
(OCaml "Big'_int.zero'_big'_int")
|
huffman@47978
|
134 |
(Haskell "0")
|
huffman@47978
|
135 |
(Scala "Nat(0)")
|
huffman@47978
|
136 |
|
huffman@47978
|
137 |
|
huffman@47978
|
138 |
subsection {* Conversions *}
|
huffman@47978
|
139 |
|
haftmann@25931
|
140 |
text {*
|
haftmann@25931
|
141 |
Since natural numbers are implemented
|
huffman@47978
|
142 |
using integers in ML, the coercion function @{term "int"} of type
|
haftmann@25931
|
143 |
@{typ "nat \<Rightarrow> int"} is simply implemented by the identity function.
|
haftmann@37363
|
144 |
For the @{const nat} function for converting an integer to a natural
|
huffman@47978
|
145 |
number, we give a specific implementation using an ML expression that
|
haftmann@25931
|
146 |
returns its input value, provided that it is non-negative, and otherwise
|
haftmann@25931
|
147 |
returns @{text "0"}.
|
haftmann@25931
|
148 |
*}
|
haftmann@25931
|
149 |
|
haftmann@32065
|
150 |
definition int :: "nat \<Rightarrow> int" where
|
huffman@47978
|
151 |
[code_abbrev]: "int = of_nat"
|
haftmann@32065
|
152 |
|
haftmann@25931
|
153 |
code_const int
|
haftmann@25931
|
154 |
(SML "_")
|
haftmann@25931
|
155 |
(OCaml "_")
|
haftmann@25931
|
156 |
|
haftmann@25967
|
157 |
code_const nat
|
haftmann@44511
|
158 |
(SML "IntInf.max/ (0,/ _)")
|
haftmann@25967
|
159 |
(OCaml "Big'_int.max'_big'_int/ Big'_int.zero'_big'_int")
|
huffman@47978
|
160 |
(Eval "Integer.max/ 0")
|
haftmann@25967
|
161 |
|
haftmann@35689
|
162 |
text {* For Haskell and Scala, things are slightly different again. *}
|
haftmann@25967
|
163 |
|
haftmann@25967
|
164 |
code_const int and nat
|
haftmann@49446
|
165 |
(Haskell "Prelude.toInteger" and "Prelude.fromInteger")
|
haftmann@39194
|
166 |
(Scala "!_.as'_BigInt" and "Nat")
|
haftmann@25931
|
167 |
|
huffman@47978
|
168 |
text {* Alternativ implementation for @{const of_nat} *}
|
huffman@47978
|
169 |
|
huffman@47978
|
170 |
lemma [code]:
|
huffman@47978
|
171 |
"of_nat n = (if n = 0 then 0 else
|
huffman@47978
|
172 |
let
|
huffman@47978
|
173 |
(q, m) = divmod_nat n 2;
|
huffman@47978
|
174 |
q' = 2 * of_nat q
|
huffman@47978
|
175 |
in if m = 0 then q' else q' + 1)"
|
huffman@47978
|
176 |
proof -
|
huffman@47978
|
177 |
from mod_div_equality have *: "of_nat n = of_nat (n div 2 * 2 + n mod 2)" by simp
|
huffman@47978
|
178 |
show ?thesis
|
huffman@47978
|
179 |
apply (simp add: Let_def divmod_nat_div_mod mod_2_not_eq_zero_eq_one_nat
|
huffman@47978
|
180 |
of_nat_mult
|
huffman@47978
|
181 |
of_nat_add [symmetric])
|
huffman@47978
|
182 |
apply (auto simp add: of_nat_mult)
|
huffman@47978
|
183 |
apply (simp add: * of_nat_mult add_commute mult_commute)
|
huffman@47978
|
184 |
done
|
huffman@47978
|
185 |
qed
|
huffman@47978
|
186 |
|
huffman@47978
|
187 |
text {* Conversion from and to code numerals *}
|
haftmann@25931
|
188 |
|
haftmann@31205
|
189 |
code_const Code_Numeral.of_nat
|
haftmann@25967
|
190 |
(SML "IntInf.toInt")
|
haftmann@31377
|
191 |
(OCaml "_")
|
haftmann@49446
|
192 |
(Haskell "!(Prelude.fromInteger/ ./ Prelude.toInteger)")
|
haftmann@39194
|
193 |
(Scala "!Natural(_.as'_BigInt)")
|
haftmann@38195
|
194 |
(Eval "_")
|
haftmann@25967
|
195 |
|
haftmann@31205
|
196 |
code_const Code_Numeral.nat_of
|
haftmann@25931
|
197 |
(SML "IntInf.fromInt")
|
haftmann@31377
|
198 |
(OCaml "_")
|
haftmann@49446
|
199 |
(Haskell "!(Prelude.fromInteger/ ./ Prelude.toInteger)")
|
haftmann@39194
|
200 |
(Scala "!Nat(_.as'_BigInt)")
|
haftmann@38195
|
201 |
(Eval "_")
|
haftmann@25931
|
202 |
|
haftmann@25931
|
203 |
|
huffman@47978
|
204 |
subsection {* Target language arithmetic *}
|
huffman@47978
|
205 |
|
huffman@47978
|
206 |
code_const "plus \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
|
huffman@47978
|
207 |
(SML "IntInf.+/ ((_),/ (_))")
|
haftmann@25931
|
208 |
(OCaml "Big'_int.add'_big'_int")
|
haftmann@25931
|
209 |
(Haskell infixl 6 "+")
|
haftmann@34899
|
210 |
(Scala infixl 7 "+")
|
haftmann@38195
|
211 |
(Eval infixl 8 "+")
|
haftmann@34899
|
212 |
|
huffman@47978
|
213 |
code_const "minus \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
|
huffman@47978
|
214 |
(SML "IntInf.max/ (0, IntInf.-/ ((_),/ (_)))")
|
huffman@47978
|
215 |
(OCaml "Big'_int.max'_big'_int/ Big'_int.zero'_big'_int/ (Big'_int.sub'_big'_int/ _/ _)")
|
haftmann@34899
|
216 |
(Haskell infixl 6 "-")
|
haftmann@34899
|
217 |
(Scala infixl 7 "-")
|
huffman@47978
|
218 |
(Eval "Integer.max/ 0/ (_ -/ _)")
|
haftmann@25931
|
219 |
|
huffman@47978
|
220 |
code_const Code_Nat.dup
|
huffman@47978
|
221 |
(SML "IntInf.*/ (2,/ (_))")
|
huffman@47978
|
222 |
(OCaml "Big'_int.mult'_big'_int/ 2")
|
huffman@47978
|
223 |
(Haskell "!(2 * _)")
|
huffman@47978
|
224 |
(Scala "!(2 * _)")
|
huffman@47978
|
225 |
(Eval "!(2 * _)")
|
huffman@47978
|
226 |
|
huffman@47978
|
227 |
code_const Code_Nat.sub
|
huffman@47978
|
228 |
(SML "!(raise/ Fail/ \"sub\")")
|
huffman@47978
|
229 |
(OCaml "failwith/ \"sub\"")
|
huffman@47978
|
230 |
(Haskell "error/ \"sub\"")
|
haftmann@49088
|
231 |
(Scala "!sys.error(\"sub\")")
|
huffman@47978
|
232 |
|
huffman@47978
|
233 |
code_const "times \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
|
huffman@47978
|
234 |
(SML "IntInf.*/ ((_),/ (_))")
|
haftmann@25931
|
235 |
(OCaml "Big'_int.mult'_big'_int")
|
haftmann@25931
|
236 |
(Haskell infixl 7 "*")
|
haftmann@34899
|
237 |
(Scala infixl 8 "*")
|
haftmann@38195
|
238 |
(Eval infixl 9 "*")
|
haftmann@25931
|
239 |
|
haftmann@38195
|
240 |
code_const divmod_nat
|
haftmann@26009
|
241 |
(SML "IntInf.divMod/ ((_),/ (_))")
|
haftmann@26009
|
242 |
(OCaml "Big'_int.quomod'_big'_int")
|
haftmann@26009
|
243 |
(Haskell "divMod")
|
haftmann@34899
|
244 |
(Scala infixl 8 "/%")
|
haftmann@38195
|
245 |
(Eval "Integer.div'_mod")
|
haftmann@25931
|
246 |
|
haftmann@39086
|
247 |
code_const "HOL.equal \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
|
haftmann@25931
|
248 |
(SML "!((_ : IntInf.int) = _)")
|
haftmann@25931
|
249 |
(OCaml "Big'_int.eq'_big'_int")
|
haftmann@39499
|
250 |
(Haskell infix 4 "==")
|
haftmann@34899
|
251 |
(Scala infixl 5 "==")
|
haftmann@38195
|
252 |
(Eval infixl 6 "=")
|
haftmann@25931
|
253 |
|
huffman@47978
|
254 |
code_const "less_eq \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
|
huffman@47978
|
255 |
(SML "IntInf.<=/ ((_),/ (_))")
|
haftmann@25931
|
256 |
(OCaml "Big'_int.le'_big'_int")
|
haftmann@25931
|
257 |
(Haskell infix 4 "<=")
|
haftmann@34899
|
258 |
(Scala infixl 4 "<=")
|
haftmann@38195
|
259 |
(Eval infixl 6 "<=")
|
haftmann@25931
|
260 |
|
huffman@47978
|
261 |
code_const "less \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
|
huffman@47978
|
262 |
(SML "IntInf.</ ((_),/ (_))")
|
haftmann@25931
|
263 |
(OCaml "Big'_int.lt'_big'_int")
|
haftmann@25931
|
264 |
(Haskell infix 4 "<")
|
haftmann@34899
|
265 |
(Scala infixl 4 "<")
|
haftmann@38195
|
266 |
(Eval infixl 6 "<")
|
haftmann@25931
|
267 |
|
huffman@47978
|
268 |
code_const Num.num_of_nat
|
huffman@47978
|
269 |
(SML "!(raise/ Fail/ \"num'_of'_nat\")")
|
huffman@47978
|
270 |
(OCaml "failwith/ \"num'_of'_nat\"")
|
huffman@47978
|
271 |
(Haskell "error/ \"num'_of'_nat\"")
|
haftmann@49088
|
272 |
(Scala "!sys.error(\"num'_of'_nat\")")
|
haftmann@25931
|
273 |
|
huffman@47978
|
274 |
|
huffman@47978
|
275 |
subsection {* Evaluation *}
|
haftmann@28228
|
276 |
|
haftmann@28562
|
277 |
lemma [code, code del]:
|
haftmann@32657
|
278 |
"(Code_Evaluation.term_of \<Colon> nat \<Rightarrow> term) = Code_Evaluation.term_of" ..
|
haftmann@28228
|
279 |
|
haftmann@32657
|
280 |
code_const "Code_Evaluation.term_of \<Colon> nat \<Rightarrow> term"
|
haftmann@28228
|
281 |
(SML "HOLogic.mk'_number/ HOLogic.natT")
|
haftmann@28228
|
282 |
|
huffman@47978
|
283 |
text {*
|
huffman@47978
|
284 |
FIXME -- Evaluation with @{text "Quickcheck_Narrowing"} does not work, as
|
bulwahn@46664
|
285 |
@{text "code_module"} is very aggressive leading to bad Haskell code.
|
bulwahn@46664
|
286 |
Therefore, we simply deactivate the narrowing-based quickcheck from here on.
|
bulwahn@46664
|
287 |
*}
|
bulwahn@46664
|
288 |
|
bulwahn@46664
|
289 |
declare [[quickcheck_narrowing_active = false]]
|
haftmann@28228
|
290 |
|
haftmann@23854
|
291 |
|
haftmann@23854
|
292 |
code_modulename SML
|
haftmann@33364
|
293 |
Efficient_Nat Arith
|
haftmann@23854
|
294 |
|
haftmann@23854
|
295 |
code_modulename OCaml
|
haftmann@33364
|
296 |
Efficient_Nat Arith
|
haftmann@23854
|
297 |
|
haftmann@23854
|
298 |
code_modulename Haskell
|
haftmann@33364
|
299 |
Efficient_Nat Arith
|
haftmann@23854
|
300 |
|
huffman@47978
|
301 |
hide_const (open) int
|
haftmann@23854
|
302 |
|
haftmann@23854
|
303 |
end
|