src/ZF/ex/twos_compl.ML
 author clasohm Thu Sep 16 12:20:38 1993 +0200 (1993-09-16) changeset 0 a5a9c433f639 child 912 ed9e0c70a5da permissions -rw-r--r--
Initial revision
```     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 *)
```