|
1 (* Title: ZF/ex/twos-compl.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 ML code for Arithmetic on binary integers; the model for theory BinFn |
|
7 |
|
8 The sign Plus stands for an infinite string of leading 0's. |
|
9 The sign Minus stands for an infinite string of leading 1's. |
|
10 |
|
11 A number can have multiple representations, namely leading 0's with sign |
|
12 Plus and leading 1's with sign Minus. See int_of_binary for the numerical |
|
13 interpretation. |
|
14 |
|
15 The representation expects that (m mod 2) is 0 or 1, even if m is negative; |
|
16 For instance, ~5 div 2 = ~3 and ~5 mod 2 = 1; thus ~5 = (~3)*2 + 1 |
|
17 |
|
18 Still needs division! |
|
19 |
|
20 print_depth 40; |
|
21 System.Control.Print.printDepth := 350; |
|
22 *) |
|
23 |
|
24 infix 5 $$ |
|
25 |
|
26 (*Recursive datatype of binary integers*) |
|
27 datatype bin = Plus | Minus | op $$ of bin * int; |
|
28 |
|
29 (** Conversions between bin and int **) |
|
30 |
|
31 fun int_of_binary Plus = 0 |
|
32 | int_of_binary Minus = ~1 |
|
33 | int_of_binary (w$$b) = 2 * int_of_binary w + b; |
|
34 |
|
35 fun binary_of_int 0 = Plus |
|
36 | binary_of_int ~1 = Minus |
|
37 | binary_of_int n = binary_of_int (n div 2) $$ (n mod 2); |
|
38 |
|
39 (*** Addition ***) |
|
40 |
|
41 (*Adding one to a number*) |
|
42 fun bin_succ Plus = Plus$$1 |
|
43 | bin_succ Minus = Plus |
|
44 | bin_succ (w$$1) = bin_succ(w) $$ 0 |
|
45 | bin_succ (w$$0) = w$$1; |
|
46 |
|
47 (*Subtracing one from a number*) |
|
48 fun bin_pred Plus = Minus |
|
49 | bin_pred Minus = Minus$$0 |
|
50 | bin_pred (w$$1) = w$$0 |
|
51 | bin_pred (w$$0) = bin_pred(w) $$ 1; |
|
52 |
|
53 (*sum of two binary integers*) |
|
54 fun bin_add (Plus, w) = w |
|
55 | bin_add (Minus, w) = bin_pred w |
|
56 | bin_add (v$$x, Plus) = v$$x |
|
57 | bin_add (v$$x, Minus) = bin_pred (v$$x) |
|
58 | bin_add (v$$x, w$$y) = bin_add(v, if x+y=2 then bin_succ w else w) $$ |
|
59 ((x+y) mod 2); |
|
60 |
|
61 (*** Subtraction ***) |
|
62 |
|
63 (*Unary minus*) |
|
64 fun bin_minus Plus = Plus |
|
65 | bin_minus Minus = Plus$$1 |
|
66 | bin_minus (w$$1) = bin_pred (bin_minus(w) $$ 0) |
|
67 | bin_minus (w$$0) = bin_minus(w) $$ 0; |
|
68 |
|
69 (*** Multiplication ***) |
|
70 |
|
71 (*product of two bins*) |
|
72 fun bin_mult (Plus, _) = Plus |
|
73 | bin_mult (Minus, v) = bin_minus v |
|
74 | bin_mult (w$$1, v) = bin_add(bin_mult(w,v) $$ 0, v) |
|
75 | bin_mult (w$$0, v) = bin_mult(w,v) $$ 0; |
|
76 |
|
77 (*** Testing ***) |
|
78 |
|
79 (*tests addition*) |
|
80 fun checksum m n = |
|
81 let val wm = binary_of_int m |
|
82 and wn = binary_of_int n |
|
83 val wsum = bin_add(wm,wn) |
|
84 in if m+n = int_of_binary wsum then (wm, wn, wsum, m+n) |
|
85 else raise Match |
|
86 end; |
|
87 |
|
88 fun bfact n = if n=0 then Plus$$1 |
|
89 else bin_mult(binary_of_int n, bfact(n-1)); |
|
90 |
|
91 (*Examples... |
|
92 bfact 5; |
|
93 int_of_binary it; |
|
94 bfact 69; |
|
95 int_of_binary it; |
|
96 |
|
97 (*leading zeros!*) |
|
98 bin_add(binary_of_int 1234, binary_of_int ~1234); |
|
99 bin_mult(binary_of_int 1234, Plus); |
|
100 |
|
101 (*leading ones!*) |
|
102 bin_add(binary_of_int 1234, binary_of_int ~1235); |
|
103 *) |