src/ZF/ex/twos-compl.ML
 changeset 0 a5a9c433f639
```     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/ZF/ex/twos-compl.ML	Thu Sep 16 12:20:38 1993 +0200
1.3 @@ -0,0 +1,103 @@
1.4 +(*  Title: 	ZF/ex/twos-compl.ML
1.5 +    ID:         \$Id\$
1.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
1.7 +    Copyright   1993  University of Cambridge
1.8 +
1.9 +ML code for Arithmetic on binary integers; the model for theory BinFn
1.10 +
1.11 +   The sign Plus stands for an infinite string of leading 0's.
1.12 +   The sign Minus stands for an infinite string of leading 1's.
1.13 +
1.14 +A number can have multiple representations, namely leading 0's with sign
1.15 +Plus and leading 1's with sign Minus.  See int_of_binary for the numerical
1.16 +interpretation.
1.17 +
1.18 +The representation expects that (m mod 2) is 0 or 1, even if m is negative;
1.19 +For instance, ~5 div 2 = ~3 and ~5 mod 2 = 1; thus ~5 = (~3)*2 + 1
1.20 +
1.21 +Still needs division!
1.22 +
1.23 +print_depth 40;
1.24 +System.Control.Print.printDepth := 350;
1.25 +*)
1.26 +
1.27 +infix 5 \$\$
1.28 +
1.29 +(*Recursive datatype of binary integers*)
1.30 +datatype bin = Plus | Minus | op \$\$ of bin * int;
1.31 +
1.32 +(** Conversions between bin and int **)
1.33 +
1.34 +fun int_of_binary Plus = 0
1.35 +  | int_of_binary Minus = ~1
1.36 +  | int_of_binary (w\$\$b) = 2 * int_of_binary w + b;
1.37 +
1.38 +fun binary_of_int 0 = Plus
1.39 +  | binary_of_int ~1 = Minus
1.40 +  | binary_of_int n = binary_of_int (n div 2) \$\$ (n mod 2);
1.41 +
1.43 +
1.44 +(*Adding one to a number*)
1.45 +fun bin_succ Plus = Plus\$\$1
1.46 +  | bin_succ Minus = Plus
1.47 +  | bin_succ (w\$\$1) = bin_succ(w) \$\$ 0
1.48 +  | bin_succ (w\$\$0) = w\$\$1;
1.49 +
1.50 +(*Subtracing one from a number*)
1.51 +fun bin_pred Plus = Minus
1.52 +  | bin_pred Minus = Minus\$\$0
1.53 +  | bin_pred (w\$\$1) = w\$\$0
1.54 +  | bin_pred (w\$\$0) = bin_pred(w) \$\$ 1;
1.55 +
1.56 +(*sum of two binary integers*)
1.57 +fun bin_add (Plus, w) = w
1.58 +  | bin_add (Minus, w) = bin_pred w
1.59 +  | bin_add (v\$\$x, Plus) = v\$\$x
1.60 +  | bin_add (v\$\$x, Minus) = bin_pred (v\$\$x)
1.61 +  | bin_add (v\$\$x, w\$\$y) = bin_add(v, if x+y=2 then bin_succ w else w) \$\$
1.62 +                           ((x+y) mod 2);
1.63 +
1.64 +(*** Subtraction ***)
1.65 +
1.66 +(*Unary minus*)
1.67 +fun bin_minus Plus = Plus
1.68 +  | bin_minus Minus = Plus\$\$1
1.69 +  | bin_minus (w\$\$1) = bin_pred (bin_minus(w) \$\$ 0)
1.70 +  | bin_minus (w\$\$0) = bin_minus(w) \$\$ 0;
1.71 +
1.72 +(*** Multiplication ***)
1.73 +
1.74 +(*product of two bins*)
1.75 +fun bin_mult (Plus, _) = Plus
1.76 +  | bin_mult (Minus, v) = bin_minus v
1.77 +  | bin_mult (w\$\$1, v) = bin_add(bin_mult(w,v) \$\$ 0,  v)
1.78 +  | bin_mult (w\$\$0, v) = bin_mult(w,v) \$\$ 0;
1.79 +
1.80 +(*** Testing ***)
1.81 +
1.83 +fun checksum m n =
1.84 +    let val wm = binary_of_int m
1.85 +        and wn = binary_of_int n
1.86 +        val wsum = bin_add(wm,wn)
1.87 +    in  if m+n = int_of_binary wsum then (wm, wn, wsum, m+n)
1.88 +        else raise Match
1.89 +    end;
1.90 +
1.91 +fun bfact n = if n=0 then  Plus\$\$1
1.92 +              else  bin_mult(binary_of_int n, bfact(n-1));
1.93 +
1.94 +(*Examples...
1.95 +bfact 5;
1.96 +int_of_binary it;
1.97 +bfact 69;
1.98 +int_of_binary it;
1.99 +