src/ZF/ex/twos-compl.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
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 *)