author  haftmann 
Thu, 29 Oct 2009 22:16:40 +0100  
changeset 33343  2eb0b672ab40 
parent 32657  5f13912245ff 
child 33364  2bd12592c5e8 
permissions  rwrr 
23854  1 
(* Title: HOL/Library/Efficient_Nat.thy 
25931  2 
Author: Stefan Berghofer, Florian Haftmann, TU Muenchen 
23854  3 
*) 
4 

25931  5 
header {* Implementation of natural numbers by targetlanguage integers *} 
23854  6 

7 
theory Efficient_Nat 

31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31128
diff
changeset

8 
imports Code_Integer Main 
23854  9 
begin 
10 

11 
text {* 

25931  12 
When generating code for functions on natural numbers, the 
13 
canonical representation using @{term "0::nat"} and 

14 
@{term "Suc"} is unsuitable for computations involving large 

15 
numbers. The efficiency of the generated code can be improved 

16 
drastically by implementing natural numbers by targetlanguage 

17 
integers. To do this, just include this theory. 

23854  18 
*} 
19 

25931  20 
subsection {* Basic arithmetic *} 
23854  21 

22 
text {* 

23 
Most standard arithmetic functions on natural numbers are implemented 

24 
using their counterparts on the integers: 

25 
*} 

26 

25931  27 
code_datatype number_nat_inst.number_of_nat 
24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

28 

32069
6d28bbd33e2c
prefer code_inline over code_unfold; use code_unfold_post where appropriate
haftmann
parents:
31998
diff
changeset

29 
lemma zero_nat_code [code, code_unfold_post]: 
25931  30 
"0 = (Numeral0 :: nat)" 
31 
by simp 

24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

32 

32069
6d28bbd33e2c
prefer code_inline over code_unfold; use code_unfold_post where appropriate
haftmann
parents:
31998
diff
changeset

33 
lemma one_nat_code [code, code_unfold_post]: 
25931  34 
"1 = (Numeral1 :: nat)" 
35 
by simp 

24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

36 

25931  37 
lemma Suc_code [code]: 
38 
"Suc n = n + 1" 

39 
by simp 

24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

40 

25931  41 
lemma plus_nat_code [code]: 
42 
"n + m = nat (of_nat n + of_nat m)" 

43 
by simp 

24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

44 

25931  45 
lemma minus_nat_code [code]: 
46 
"n  m = nat (of_nat n  of_nat m)" 

47 
by simp 

24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

48 

25931  49 
lemma times_nat_code [code]: 
50 
"n * m = nat (of_nat n * of_nat m)" 

51 
unfolding of_nat_mult [symmetric] by simp 

24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

52 

26009  53 
text {* Specialized @{term "op div \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"} 
54 
and @{term "op mod \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"} operations. *} 

55 

28694  56 
definition divmod_aux :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where 
33343  57 
[code del]: "divmod_aux = divmod_nat" 
24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

58 

28522  59 
lemma [code]: 
33343  60 
"divmod_nat n m = (if m = 0 then (0, n) else divmod_aux n m)" 
61 
unfolding divmod_aux_def divmod_nat_div_mod by simp 

26009  62 

26100
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26009
diff
changeset

63 
lemma divmod_aux_code [code]: 
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26009
diff
changeset

64 
"divmod_aux n m = (nat (of_nat n div of_nat m), nat (of_nat n mod of_nat m))" 
33343  65 
unfolding divmod_aux_def divmod_nat_div_mod zdiv_int [symmetric] zmod_int [symmetric] by simp 
24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

66 

25931  67 
lemma eq_nat_code [code]: 
28351  68 
"eq_class.eq n m \<longleftrightarrow> eq_class.eq (of_nat n \<Colon> int) (of_nat m)" 
69 
by (simp add: eq) 

70 

71 
lemma eq_nat_refl [code nbe]: 

72 
"eq_class.eq (n::nat) n \<longleftrightarrow> True" 

73 
by (rule HOL.eq_refl) 

24715
f96d86cdbe5a
Efficient_Nat and Pretty_Int integrated with ML_Int
haftmann
parents:
24630
diff
changeset

74 

25931  75 
lemma less_eq_nat_code [code]: 
76 
"n \<le> m \<longleftrightarrow> (of_nat n \<Colon> int) \<le> of_nat m" 

77 
by simp 

23854  78 

25931  79 
lemma less_nat_code [code]: 
80 
"n < m \<longleftrightarrow> (of_nat n \<Colon> int) < of_nat m" 

81 
by simp 

23854  82 

25931  83 
subsection {* Case analysis *} 
23854  84 

85 
text {* 

25931  86 
Case analysis on natural numbers is rephrased using a conditional 
87 
expression: 

23854  88 
*} 
89 

31998
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31954
diff
changeset

90 
lemma [code, code_unfold]: 
25931  91 
"nat_case = (\<lambda>f g n. if n = 0 then f else g (n  1))" 
92 
by (auto simp add: expand_fun_eq dest!: gr0_implies_Suc) 

25615  93 

23854  94 

95 
subsection {* Preprocessors *} 

96 

97 
text {* 

98 
In contrast to @{term "Suc n"}, the term @{term "n + (1::nat)"} is no longer 

99 
a constructor term. Therefore, all occurrences of this term in a position 

100 
where a pattern is expected (i.e.\ on the lefthand side of a recursion 

101 
equation or in the arguments of an inductive relation in an introduction 

102 
rule) must be eliminated. 

103 
This can be accomplished by applying the following transformation rules: 

104 
*} 

105 

29937  106 
lemma Suc_if_eq: "(\<And>n. f (Suc n) \<equiv> h n) \<Longrightarrow> f 0 \<equiv> g \<Longrightarrow> 
107 
f n \<equiv> if n = 0 then g else h (n  1)" 

31954
8db19c99b00a
Stefan Berghofer's code generator uses Pure equality instead of HOL equality now
haftmann
parents:
31377
diff
changeset

108 
by (rule eq_reflection) (cases n, simp_all) 
29937  109 

25931  110 
lemma Suc_clause: "(\<And>n. P n (Suc n)) \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> P (n  1) n" 
29932
a2594b5c945a
dropped clause_suc_preproc for generic code generator
haftmann
parents:
29815
diff
changeset

111 
by (cases n) simp_all 
23854  112 

113 
text {* 

114 
The rules above are built into a preprocessor that is plugged into 

115 
the code generator. Since the preprocessor for introduction rules 

116 
does not know anything about modes, some of the modes that worked 

117 
for the canonical representation of natural numbers may no longer work. 

118 
*} 

119 

120 
(*<*) 

27609  121 
setup {* 
122 
let 

23854  123 

31954
8db19c99b00a
Stefan Berghofer's code generator uses Pure equality instead of HOL equality now
haftmann
parents:
31377
diff
changeset

124 
fun remove_suc thy thms = 
23854  125 
let 
126 
val vname = Name.variant (map fst 

29937  127 
(fold (Term.add_var_names o Thm.full_prop_of) thms [])) "n"; 
23854  128 
val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT)); 
129 
fun lhs_of th = snd (Thm.dest_comb 

31954
8db19c99b00a
Stefan Berghofer's code generator uses Pure equality instead of HOL equality now
haftmann
parents:
31377
diff
changeset

130 
(fst (Thm.dest_comb (cprop_of th)))); 
8db19c99b00a
Stefan Berghofer's code generator uses Pure equality instead of HOL equality now
haftmann
parents:
31377
diff
changeset

131 
fun rhs_of th = snd (Thm.dest_comb (cprop_of th)); 
23854  132 
fun find_vars ct = (case term_of ct of 
29932
a2594b5c945a
dropped clause_suc_preproc for generic code generator
haftmann
parents:
29815
diff
changeset

133 
(Const (@{const_name Suc}, _) $ Var _) => [(cv, snd (Thm.dest_comb ct))] 
23854  134 
 _ $ _ => 
135 
let val (ct1, ct2) = Thm.dest_comb ct 

136 
in 

137 
map (apfst (fn ct => Thm.capply ct ct2)) (find_vars ct1) @ 

138 
map (apfst (Thm.capply ct1)) (find_vars ct2) 

139 
end 

140 
 _ => []); 

141 
val eqs = maps 

142 
(fn th => map (pair th) (find_vars (lhs_of th))) thms; 

143 
fun mk_thms (th, (ct, cv')) = 

144 
let 

145 
val th' = 

146 
Thm.implies_elim 

147 
(Conv.fconv_rule (Thm.beta_conversion true) 

148 
(Drule.instantiate' 

149 
[SOME (ctyp_of_term ct)] [SOME (Thm.cabs cv ct), 

150 
SOME (Thm.cabs cv' (rhs_of th)), NONE, SOME cv'] 

31954
8db19c99b00a
Stefan Berghofer's code generator uses Pure equality instead of HOL equality now
haftmann
parents:
31377
diff
changeset

151 
@{thm Suc_if_eq})) (Thm.forall_intr cv' th) 
23854  152 
in 
153 
case map_filter (fn th'' => 

154 
SOME (th'', singleton 

155 
(Variable.trade (K (fn [th'''] => [th''' RS th'])) (Variable.thm_context th'')) th'') 

156 
handle THM _ => NONE) thms of 

157 
[] => NONE 

158 
 thps => 

159 
let val (ths1, ths2) = split_list thps 

160 
in SOME (subtract Thm.eq_thm (th :: ths1) thms @ ths2) end 

161 
end 

29937  162 
in get_first mk_thms eqs end; 
163 

31954
8db19c99b00a
Stefan Berghofer's code generator uses Pure equality instead of HOL equality now
haftmann
parents:
31377
diff
changeset

164 
fun eqn_suc_preproc thy thms = 
29937  165 
let 
31954
8db19c99b00a
Stefan Berghofer's code generator uses Pure equality instead of HOL equality now
haftmann
parents:
31377
diff
changeset

166 
val dest = fst o Logic.dest_equals o prop_of; 
29937  167 
val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc}); 
168 
in 

169 
if forall (can dest) thms andalso exists (contains_suc o dest) thms 

32348  170 
then thms > perhaps_loop (remove_suc thy) > (Option.map o map) Drule.zero_var_indexes 
29937  171 
else NONE 
23854  172 
end; 
173 

31954
8db19c99b00a
Stefan Berghofer's code generator uses Pure equality instead of HOL equality now
haftmann
parents:
31377
diff
changeset

174 
val eqn_suc_preproc1 = Code_Preproc.simple_functrans eqn_suc_preproc; 
29937  175 

31954
8db19c99b00a
Stefan Berghofer's code generator uses Pure equality instead of HOL equality now
haftmann
parents:
31377
diff
changeset

176 
fun eqn_suc_preproc2 thy thms = eqn_suc_preproc thy thms 
29937  177 
> the_default thms; 
23854  178 

179 
fun remove_suc_clause thy thms = 

180 
let 

181 
val vname = Name.variant (map fst 

29258  182 
(fold (Term.add_var_names o Thm.full_prop_of) thms [])) "x"; 
24222  183 
fun find_var (t as Const (@{const_name Suc}, _) $ (v as Var _)) = SOME (t, v) 
23854  184 
 find_var (t $ u) = (case find_var t of NONE => find_var u  x => x) 
185 
 find_var _ = NONE; 

186 
fun find_thm th = 

187 
let val th' = Conv.fconv_rule ObjectLogic.atomize th 

188 
in Option.map (pair (th, th')) (find_var (prop_of th')) end 

189 
in 

190 
case get_first find_thm thms of 

191 
NONE => thms 

192 
 SOME ((th, th'), (Sucv, v)) => 

193 
let 

194 
val cert = cterm_of (Thm.theory_of_thm th); 

195 
val th'' = ObjectLogic.rulify (Thm.implies_elim 

196 
(Conv.fconv_rule (Thm.beta_conversion true) 

197 
(Drule.instantiate' [] 

198 
[SOME (cert (lambda v (Abs ("x", HOLogic.natT, 

199 
abstract_over (Sucv, 

200 
HOLogic.dest_Trueprop (prop_of th')))))), 

24222  201 
SOME (cert v)] @{thm Suc_clause})) 
23854  202 
(Thm.forall_intr (cert v) th')) 
203 
in 

204 
remove_suc_clause thy (map (fn th''' => 

205 
if (op = o pairself prop_of) (th''', th) then th'' else th''') thms) 

206 
end 

207 
end; 

208 

209 
fun clause_suc_preproc thy ths = 

210 
let 

211 
val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop 

212 
in 

213 
if forall (can (dest o concl_of)) ths andalso 

29287  214 
exists (fn th => exists (exists_Const (fn (c, _) => c = @{const_name Suc})) 
215 
(map_filter (try dest) (concl_of th :: prems_of th))) ths 

23854  216 
then remove_suc_clause thy ths else ths 
217 
end; 

27609  218 
in 
219 

31954
8db19c99b00a
Stefan Berghofer's code generator uses Pure equality instead of HOL equality now
haftmann
parents:
31377
diff
changeset

220 
Codegen.add_preprocessor eqn_suc_preproc2 
23854  221 
#> Codegen.add_preprocessor clause_suc_preproc 
31954
8db19c99b00a
Stefan Berghofer's code generator uses Pure equality instead of HOL equality now
haftmann
parents:
31377
diff
changeset

222 
#> Code_Preproc.add_functrans ("eqn_Suc", eqn_suc_preproc1) 
27609  223 

224 
end; 

23854  225 
*} 
226 
(*>*) 

227 

27609  228 

25931  229 
subsection {* Target language setup *} 
230 

231 
text {* 

25967  232 
For ML, we map @{typ nat} to target language integers, where we 
25931  233 
assert that values are always nonnegative. 
234 
*} 

235 

236 
code_type nat 

27496  237 
(SML "IntInf.int") 
25931  238 
(OCaml "Big'_int.big'_int") 
239 

240 
types_code 

241 
nat ("int") 

242 
attach (term_of) {* 

243 
val term_of_nat = HOLogic.mk_number HOLogic.natT; 

244 
*} 

245 
attach (test) {* 

246 
fun gen_nat i = 

247 
let val n = random_range 0 i 

248 
in (n, fn () => term_of_nat n) end; 

249 
*} 

250 

251 
text {* 

25967  252 
For Haskell we define our own @{typ nat} type. The reason 
253 
is that we have to distinguish type class instances 

254 
for @{typ nat} and @{typ int}. 

255 
*} 

256 

257 
code_include Haskell "Nat" {* 

258 
newtype Nat = Nat Integer deriving (Show, Eq); 

259 

260 
instance Num Nat where { 

261 
fromInteger k = Nat (if k >= 0 then k else 0); 

262 
Nat n + Nat m = Nat (n + m); 

263 
Nat n  Nat m = fromInteger (n  m); 

264 
Nat n * Nat m = Nat (n * m); 

265 
abs n = n; 

266 
signum _ = 1; 

267 
negate n = error "negate Nat"; 

268 
}; 

269 

270 
instance Ord Nat where { 

271 
Nat n <= Nat m = n <= m; 

272 
Nat n < Nat m = n < m; 

273 
}; 

274 

275 
instance Real Nat where { 

276 
toRational (Nat n) = toRational n; 

277 
}; 

278 

279 
instance Enum Nat where { 

280 
toEnum k = fromInteger (toEnum k); 

281 
fromEnum (Nat n) = fromEnum n; 

282 
}; 

283 

284 
instance Integral Nat where { 

285 
toInteger (Nat n) = n; 

286 
divMod n m = quotRem n m; 

287 
quotRem (Nat n) (Nat m) = (Nat k, Nat l) where (k, l) = quotRem n m; 

288 
}; 

289 
*} 

290 

291 
code_reserved Haskell Nat 

292 

293 
code_type nat 

29793  294 
(Haskell "Nat.Nat") 
25967  295 

296 
code_instance nat :: eq 

297 
(Haskell ) 

298 

299 
text {* 

25931  300 
Natural numerals. 
301 
*} 

302 

32069
6d28bbd33e2c
prefer code_inline over code_unfold; use code_unfold_post where appropriate
haftmann
parents:
31998
diff
changeset

303 
lemma [code_unfold_post]: 
25931  304 
"nat (number_of i) = number_nat_inst.number_of_nat i" 
305 
 {* this interacts as desired with @{thm nat_number_of_def} *} 

306 
by (simp add: number_nat_inst.number_of_nat) 

307 

308 
setup {* 

309 
fold (Numeral.add_code @{const_name number_nat_inst.number_of_nat} 

31295  310 
false true) ["SML", "OCaml", "Haskell"] 
25931  311 
*} 
312 

313 
text {* 

314 
Since natural numbers are implemented 

25967  315 
using integers in ML, the coercion function @{const "of_nat"} of type 
25931  316 
@{typ "nat \<Rightarrow> int"} is simply implemented by the identity function. 
317 
For the @{const "nat"} function for converting an integer to a natural 

318 
number, we give a specific implementation using an ML function that 

319 
returns its input value, provided that it is nonnegative, and otherwise 

320 
returns @{text "0"}. 

321 
*} 

322 

32073  323 
definition int :: "nat \<Rightarrow> int" where 
28562  324 
[code del]: "int = of_nat" 
25931  325 

28562  326 
lemma int_code' [code]: 
25931  327 
"int (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)" 
328 
unfolding int_nat_number_of [folded int_def] .. 

329 

28562  330 
lemma nat_code' [code]: 
25931  331 
"nat (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)" 
28969  332 
unfolding nat_number_of_def number_of_is_id neg_def by simp 
25931  333 

32069
6d28bbd33e2c
prefer code_inline over code_unfold; use code_unfold_post where appropriate
haftmann
parents:
31998
diff
changeset

334 
lemma of_nat_int [code_unfold_post]: 
25931  335 
"of_nat = int" by (simp add: int_def) 
336 

32073  337 
lemma of_nat_aux_int [code_unfold]: 
338 
"of_nat_aux (\<lambda>i. i + 1) k 0 = int k" 

339 
by (simp add: int_def Nat.of_nat_code) 

340 

25931  341 
code_const int 
342 
(SML "_") 

343 
(OCaml "_") 

344 

345 
consts_code 

346 
int ("(_)") 

347 
nat ("\<module>nat") 

348 
attach {* 

349 
fun nat i = if i < 0 then 0 else i; 

350 
*} 

351 

25967  352 
code_const nat 
353 
(SML "IntInf.max/ (/0,/ _)") 

354 
(OCaml "Big'_int.max'_big'_int/ Big'_int.zero'_big'_int") 

355 

356 
text {* For Haskell, things are slightly different again. *} 

357 

358 
code_const int and nat 

359 
(Haskell "toInteger" and "fromInteger") 

25931  360 

361 
text {* Conversion from and to indices. *} 

362 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

363 
code_const Code_Numeral.of_nat 
25967  364 
(SML "IntInf.toInt") 
31377  365 
(OCaml "_") 
27673  366 
(Haskell "fromEnum") 
25967  367 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

368 
code_const Code_Numeral.nat_of 
25931  369 
(SML "IntInf.fromInt") 
31377  370 
(OCaml "_") 
27673  371 
(Haskell "toEnum") 
25931  372 

373 
text {* Using target language arithmetic operations whenever appropriate *} 

374 

375 
code_const "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" 

376 
(SML "IntInf.+ ((_), (_))") 

377 
(OCaml "Big'_int.add'_big'_int") 

378 
(Haskell infixl 6 "+") 

379 

380 
code_const "op * \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" 

381 
(SML "IntInf.* ((_), (_))") 

382 
(OCaml "Big'_int.mult'_big'_int") 

383 
(Haskell infixl 7 "*") 

384 

26100
fbc60cd02ae2
using only an relation predicate to construct div and mod
haftmann
parents:
26009
diff
changeset

385 
code_const divmod_aux 
26009  386 
(SML "IntInf.divMod/ ((_),/ (_))") 
387 
(OCaml "Big'_int.quomod'_big'_int") 

388 
(Haskell "divMod") 

25931  389 

28346
b8390cd56b8f
discontinued special treatment of op = vs. eq_class.eq
haftmann
parents:
28228
diff
changeset

390 
code_const "eq_class.eq \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool" 
25931  391 
(SML "!((_ : IntInf.int) = _)") 
392 
(OCaml "Big'_int.eq'_big'_int") 

393 
(Haskell infixl 4 "==") 

394 

395 
code_const "op \<le> \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool" 

396 
(SML "IntInf.<= ((_), (_))") 

397 
(OCaml "Big'_int.le'_big'_int") 

398 
(Haskell infix 4 "<=") 

399 

400 
code_const "op < \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool" 

401 
(SML "IntInf.< ((_), (_))") 

402 
(OCaml "Big'_int.lt'_big'_int") 

403 
(Haskell infix 4 "<") 

404 

405 
consts_code 

28522  406 
"0::nat" ("0") 
407 
"1::nat" ("1") 

25931  408 
Suc ("(_ +/ 1)") 
409 
"op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" ("(_ +/ _)") 

410 
"op * \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" ("(_ */ _)") 

411 
"op \<le> \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool" ("(_ <=/ _)") 

412 
"op < \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool" ("(_ </ _)") 

413 

414 

28228  415 
text {* Evaluation *} 
416 

28562  417 
lemma [code, code del]: 
32657  418 
"(Code_Evaluation.term_of \<Colon> nat \<Rightarrow> term) = Code_Evaluation.term_of" .. 
28228  419 

32657  420 
code_const "Code_Evaluation.term_of \<Colon> nat \<Rightarrow> term" 
28228  421 
(SML "HOLogic.mk'_number/ HOLogic.natT") 
422 

423 

25931  424 
text {* Module names *} 
23854  425 

426 
code_modulename SML 

427 
Nat Integer 

428 
Divides Integer 

28683
59c01ec6cb8d
more clever module name aliasses for code generation
haftmann
parents:
28562
diff
changeset

429 
Ring_and_Field Integer 
23854  430 
Efficient_Nat Integer 
431 

432 
code_modulename OCaml 

433 
Nat Integer 

434 
Divides Integer 

28683
59c01ec6cb8d
more clever module name aliasses for code generation
haftmann
parents:
28562
diff
changeset

435 
Ring_and_Field Integer 
23854  436 
Efficient_Nat Integer 
437 

438 
code_modulename Haskell 

439 
Nat Integer 

24195  440 
Divides Integer 
28683
59c01ec6cb8d
more clever module name aliasses for code generation
haftmann
parents:
28562
diff
changeset

441 
Ring_and_Field Integer 
23854  442 
Efficient_Nat Integer 
443 

25931  444 
hide const int 
23854  445 

446 
end 