author lcp Mon, 27 Feb 1995 17:51:12 +0100 changeset 912 ed9e0c70a5da parent 911 55754d6d399c child 913 8aaa8c5a567e
Redefined functions to suppress redundant leading 0s and 1s
 src/ZF/ex/twos_compl.ML file | annotate | diff | comparison | revisions
```--- a/src/ZF/ex/twos_compl.ML	Mon Feb 27 17:47:57 1995 +0100
+++ b/src/ZF/ex/twos_compl.ML	Mon Feb 27 17:51:12 1995 +0100
@@ -3,14 +3,14 @@
Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory

-ML code for Arithmetic on binary integers; the model for theory BinFn
+ML code for Arithmetic on binary integers; the model for theory Bin

-   The sign Plus stands for an infinite string of leading 0's.
-   The sign Minus stands for an infinite string of leading 1's.
+   The sign Plus stands for an infinite string of leading 0s.
+   The sign Minus stands for an infinite string of leading 1s.

-A number can have multiple representations, namely leading 0's with sign
-Plus and leading 1's with sign Minus.  See int_of_binary for the numerical
-interpretation.
+See int_of_binary for the numerical interpretation.  A number can have
+multiple representations, namely leading 0s with sign Plus and leading 1s with
+sign Minus.  A number is in NORMAL FORM if it has no such extra bits.

The representation expects that (m mod 2) is 0 or 1, even if m is negative;
For instance, ~5 div 2 = ~3 and ~5 mod 2 = 1; thus ~5 = (~3)*2 + 1
@@ -21,7 +21,7 @@
System.Control.Print.printDepth := 350;
*)

-infix 5 \$\$
+infix 5 \$\$ \$\$\$

(*Recursive datatype of binary integers*)
datatype bin = Plus | Minus | op \$\$ of bin * int;
@@ -38,25 +38,36 @@

+(*Attach a bit while preserving the normal form.  Cases left as default
+  are Plus\$\$\$1 and Minus\$\$\$0. *)
+fun  Plus \$\$\$ 0 = Plus
+  | Minus \$\$\$ 1 = Minus
+  |     v \$\$\$ x = v\$\$x;
+
+(*Successor of an integer, assumed to be in normal form.
+  If w\$\$1 is normal then w is not Minus, so bin_succ(w) \$\$ 0 is normal.
+  But Minus\$\$0 is normal while Minus\$\$1 is not.*)
fun bin_succ Plus = Plus\$\$1
| bin_succ Minus = Plus
| bin_succ (w\$\$1) = bin_succ(w) \$\$ 0
-  | bin_succ (w\$\$0) = w\$\$1;
+  | bin_succ (w\$\$0) = w \$\$\$ 1;

-(*Subtracing one from a number*)
+(*Predecessor of an integer, assumed to be in normal form.
+  If w\$\$0 is normal then w is not Plus, so bin_pred(w) \$\$ 1 is normal.
+  But Plus\$\$1 is normal while Plus\$\$0 is not.*)
fun bin_pred Plus = Minus
| bin_pred Minus = Minus\$\$0
-  | bin_pred (w\$\$1) = w\$\$0
+  | bin_pred (w\$\$1) = w \$\$\$ 0
| bin_pred (w\$\$0) = bin_pred(w) \$\$ 1;

-(*sum of two binary integers*)
+(*Sum of two binary integers in normal form.
+  Ensure last \$\$ preserves normal form! *)
fun bin_add (Plus, w) = w
| bin_add (Minus, w) = bin_pred w
| bin_add (v\$\$x, Plus) = v\$\$x
| bin_add (v\$\$x, Minus) = bin_pred (v\$\$x)
-  | bin_add (v\$\$x, w\$\$y) = bin_add(v, if x+y=2 then bin_succ w else w) \$\$
-                           ((x+y) mod 2);
+  | bin_add (v\$\$x, w\$\$y) =
+      bin_add(v, if x+y=2 then bin_succ w else w) \$\$\$ ((x+y) mod 2);

(*** Subtraction ***)

@@ -68,11 +79,11 @@

(*** Multiplication ***)

-(*product of two bins*)
+(*product of two bins; a factor of 0 might cause leading 0s in result*)
fun bin_mult (Plus, _) = Plus
| bin_mult (Minus, v) = bin_minus v
-  | bin_mult (w\$\$1, v) = bin_add(bin_mult(w,v) \$\$ 0,  v)
-  | bin_mult (w\$\$0, v) = bin_mult(w,v) \$\$ 0;
+  | bin_mult (w\$\$1, v) = bin_add(bin_mult(w,v) \$\$\$ 0,  v)
+  | bin_mult (w\$\$0, v) = bin_mult(w,v) \$\$\$ 0;

(*** Testing ***)

@@ -94,10 +105,11 @@
bfact 69;
int_of_binary it;

bin_mult(binary_of_int 1234, Plus);