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 Bin |
|
7 |
|
8 The sign Pls stands for an infinite string of leading 0s. |
|
9 The sign Min stands for an infinite string of leading 1s. |
|
10 |
|
11 See int_of_binary for the numerical interpretation. A number can have |
|
12 multiple representations, namely leading 0s with sign Pls and leading 1s with |
|
13 sign Min. A number is in NORMAL FORM if it has no such extra bits. |
|
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 = Pls | Min | $$ of bin * int; |
|
28 |
|
29 (** Conversions between bin and int **) |
|
30 |
|
31 fun int_of_binary Pls = 0 |
|
32 | int_of_binary Min = ~1 |
|
33 | int_of_binary (w$$b) = 2 * int_of_binary w + b; |
|
34 |
|
35 fun binary_of_int 0 = Pls |
|
36 | binary_of_int ~1 = Min |
|
37 | binary_of_int n = binary_of_int (n div 2) $$ (n mod 2); |
|
38 |
|
39 (*** Addition ***) |
|
40 |
|
41 (*Attach a bit while preserving the normal form. Cases left as default |
|
42 are Pls$$$1 and Min$$$0. *) |
|
43 fun Pls $$$ 0 = Pls |
|
44 | Min $$$ 1 = Min |
|
45 | v $$$ x = v$$x; |
|
46 |
|
47 (*Successor of an integer, assumed to be in normal form. |
|
48 If w$$1 is normal then w is not Min, so bin_succ(w) $$ 0 is normal. |
|
49 But Min$$0 is normal while Min$$1 is not.*) |
|
50 fun bin_succ Pls = Pls$$1 |
|
51 | bin_succ Min = Pls |
|
52 | bin_succ (w$$1) = bin_succ(w) $$ 0 |
|
53 | bin_succ (w$$0) = w $$$ 1; |
|
54 |
|
55 (*Predecessor of an integer, assumed to be in normal form. |
|
56 If w$$0 is normal then w is not Pls, so bin_pred(w) $$ 1 is normal. |
|
57 But Pls$$1 is normal while Pls$$0 is not.*) |
|
58 fun bin_pred Pls = Min |
|
59 | bin_pred Min = Min$$0 |
|
60 | bin_pred (w$$1) = w $$$ 0 |
|
61 | bin_pred (w$$0) = bin_pred(w) $$ 1; |
|
62 |
|
63 (*Sum of two binary integers in normal form. |
|
64 Ensure last $$ preserves normal form! *) |
|
65 fun bin_add (Pls, w) = w |
|
66 | bin_add (Min, w) = bin_pred w |
|
67 | bin_add (v$$x, Pls) = v$$x |
|
68 | bin_add (v$$x, Min) = bin_pred (v$$x) |
|
69 | bin_add (v$$x, w$$y) = |
|
70 bin_add(v, if x+y=2 then bin_succ w else w) $$$ ((x+y) mod 2); |
|
71 |
|
72 (*** Subtraction ***) |
|
73 |
|
74 (*Unary minus*) |
|
75 fun bin_minus Pls = Pls |
|
76 | bin_minus Min = Pls$$1 |
|
77 | bin_minus (w$$1) = bin_pred (bin_minus(w) $$$ 0) |
|
78 | bin_minus (w$$0) = bin_minus(w) $$ 0; |
|
79 |
|
80 (*** Multiplication ***) |
|
81 |
|
82 (*product of two bins; a factor of 0 might cause leading 0s in result*) |
|
83 fun bin_mult (Pls, _) = Pls |
|
84 | bin_mult (Min, v) = bin_minus v |
|
85 | bin_mult (w$$1, v) = bin_add(bin_mult(w,v) $$$ 0, v) |
|
86 | bin_mult (w$$0, v) = bin_mult(w,v) $$$ 0; |
|
87 |
|
88 (*** Testing ***) |
|
89 |
|
90 (*tests addition*) |
|
91 fun checksum m n = |
|
92 let val wm = binary_of_int m |
|
93 and wn = binary_of_int n |
|
94 val wsum = bin_add(wm,wn) |
|
95 in if m+n = int_of_binary wsum then (wm, wn, wsum, m+n) |
|
96 else raise Match |
|
97 end; |
|
98 |
|
99 fun bfact n = if n=0 then Pls$$1 |
|
100 else bin_mult(binary_of_int n, bfact(n-1)); |
|
101 |
|
102 (*Examples... |
|
103 bfact 5; |
|
104 int_of_binary it; |
|
105 bfact 69; |
|
106 int_of_binary it; |
|
107 |
|
108 (*For {HOL,ZF}/ex/BinEx.ML*) |
|
109 bin_add(binary_of_int 13, binary_of_int 19); |
|
110 bin_add(binary_of_int 1234, binary_of_int 5678); |
|
111 bin_add(binary_of_int 1359, binary_of_int ~2468); |
|
112 bin_add(binary_of_int 93746, binary_of_int ~46375); |
|
113 bin_minus(binary_of_int 65745); |
|
114 bin_minus(binary_of_int ~54321); |
|
115 bin_mult(binary_of_int 13, binary_of_int 19); |
|
116 bin_mult(binary_of_int ~84, binary_of_int 51); |
|
117 bin_mult(binary_of_int 255, binary_of_int 255); |
|
118 bin_mult(binary_of_int 1359, binary_of_int ~2468); |
|
119 |
|
120 |
|
121 (*leading zeros??*) |
|
122 bin_add(binary_of_int 1234, binary_of_int ~1234); |
|
123 bin_mult(binary_of_int 1234, Pls); |
|
124 |
|
125 (*leading ones??*) |
|
126 bin_add(binary_of_int 1, binary_of_int ~2); |
|
127 bin_add(binary_of_int 1234, binary_of_int ~1235); |
|
128 *) |
|