src/ZF/Tools/twos_compl.ML
author wenzelm
Thu May 31 12:06:31 2007 +0200 (2007-05-31)
changeset 23146 0bc590051d95
child 24584 01e83ffa6c54
permissions -rw-r--r--
moved Integ files to canonical place;
     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 Bin
     7 
     8    The sign Pls stands for an infinite string of leading 0s.
     9    The sign Min stands for an infinite string of leading 1s.
    10 
    11 See int_of_binary for the numerical interpretation.  A number can have
    12 multiple representations, namely leading 0s with sign Pls and leading 1s with
    13 sign Min.  A number is in NORMAL FORM if it has no such extra bits.
    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 = Pls | Min | $$ of bin * int;
    28 
    29 (** Conversions between bin and int **)
    30 
    31 fun int_of_binary Pls = 0
    32   | int_of_binary Min = ~1
    33   | int_of_binary (w$$b) = 2 * int_of_binary w + b;
    34 
    35 fun binary_of_int 0 = Pls
    36   | binary_of_int ~1 = Min
    37   | binary_of_int n = binary_of_int (n div 2) $$ (n mod 2);
    38 
    39 (*** Addition ***)
    40 
    41 (*Attach a bit while preserving the normal form.  Cases left as default
    42   are Pls$$$1 and Min$$$0. *)
    43 fun  Pls $$$ 0 = Pls
    44   | Min $$$ 1 = Min
    45   |     v $$$ x = v$$x;
    46 
    47 (*Successor of an integer, assumed to be in normal form.
    48   If w$$1 is normal then w is not Min, so bin_succ(w) $$ 0 is normal.
    49   But Min$$0 is normal while Min$$1 is not.*)
    50 fun bin_succ Pls = Pls$$1
    51   | bin_succ Min = Pls
    52   | bin_succ (w$$1) = bin_succ(w) $$ 0
    53   | bin_succ (w$$0) = w $$$ 1;
    54 
    55 (*Predecessor of an integer, assumed to be in normal form.
    56   If w$$0 is normal then w is not Pls, so bin_pred(w) $$ 1 is normal.
    57   But Pls$$1 is normal while Pls$$0 is not.*)
    58 fun bin_pred Pls = Min
    59   | bin_pred Min = Min$$0
    60   | bin_pred (w$$1) = w $$$ 0
    61   | bin_pred (w$$0) = bin_pred(w) $$ 1;
    62 
    63 (*Sum of two binary integers in normal form.  
    64   Ensure last $$ preserves normal form! *)
    65 fun bin_add (Pls, w) = w
    66   | bin_add (Min, w) = bin_pred w
    67   | bin_add (v$$x, Pls) = v$$x
    68   | bin_add (v$$x, Min) = bin_pred (v$$x)
    69   | bin_add (v$$x, w$$y) = 
    70       bin_add(v, if x+y=2 then bin_succ w else w) $$$ ((x+y) mod 2);
    71 
    72 (*** Subtraction ***)
    73 
    74 (*Unary minus*)
    75 fun bin_minus Pls = Pls
    76   | bin_minus Min = Pls$$1
    77   | bin_minus (w$$1) = bin_pred (bin_minus(w) $$$ 0)
    78   | bin_minus (w$$0) = bin_minus(w) $$ 0;
    79 
    80 (*** Multiplication ***)
    81 
    82 (*product of two bins; a factor of 0 might cause leading 0s in result*)
    83 fun bin_mult (Pls, _) = Pls
    84   | bin_mult (Min, v) = bin_minus v
    85   | bin_mult (w$$1, v) = bin_add(bin_mult(w,v) $$$ 0,  v)
    86   | bin_mult (w$$0, v) = bin_mult(w,v) $$$ 0;
    87 
    88 (*** Testing ***)
    89 
    90 (*tests addition*)
    91 fun checksum m n =
    92     let val wm = binary_of_int m
    93         and wn = binary_of_int n
    94         val wsum = bin_add(wm,wn)
    95     in  if m+n = int_of_binary wsum then (wm, wn, wsum, m+n)
    96         else raise Match
    97     end;
    98 
    99 fun bfact n = if n=0 then  Pls$$1  
   100               else  bin_mult(binary_of_int n, bfact(n-1));
   101 
   102 (*Examples...
   103 bfact 5;
   104 int_of_binary it;
   105 bfact 69;
   106 int_of_binary it;
   107 
   108 (*For {HOL,ZF}/ex/BinEx.ML*)
   109 bin_add(binary_of_int 13, binary_of_int 19);
   110 bin_add(binary_of_int 1234, binary_of_int 5678);
   111 bin_add(binary_of_int 1359, binary_of_int ~2468);
   112 bin_add(binary_of_int 93746, binary_of_int ~46375);
   113 bin_minus(binary_of_int 65745);
   114 bin_minus(binary_of_int ~54321);
   115 bin_mult(binary_of_int 13, binary_of_int 19);
   116 bin_mult(binary_of_int ~84, binary_of_int 51);
   117 bin_mult(binary_of_int 255, binary_of_int 255);
   118 bin_mult(binary_of_int 1359, binary_of_int ~2468);
   119 
   120 
   121 (*leading zeros??*)
   122 bin_add(binary_of_int 1234, binary_of_int ~1234);
   123 bin_mult(binary_of_int 1234, Pls);
   124 
   125 (*leading ones??*)
   126 bin_add(binary_of_int 1, binary_of_int ~2);
   127 bin_add(binary_of_int 1234, binary_of_int ~1235);
   128 *)