src/ZF/ex/twos_compl.ML
changeset 0 a5a9c433f639
child 912 ed9e0c70a5da
     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.42 +(*** Addition ***)
    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.82 +(*tests addition*)
    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 +
   1.100 +(*leading zeros!*)
   1.101 +bin_add(binary_of_int 1234, binary_of_int ~1234);
   1.102 +bin_mult(binary_of_int 1234, Plus);
   1.103 +
   1.104 +(*leading ones!*)
   1.105 +bin_add(binary_of_int 1234, binary_of_int ~1235);
   1.106 +*)