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;
wenzelm@23146
     1
(*  Title:      ZF/ex/twos-compl.ML
wenzelm@23146
     2
    ID:         $Id$
wenzelm@23146
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
wenzelm@23146
     4
    Copyright   1993  University of Cambridge
wenzelm@23146
     5
wenzelm@23146
     6
ML code for Arithmetic on binary integers; the model for theory Bin
wenzelm@23146
     7
wenzelm@23146
     8
   The sign Pls stands for an infinite string of leading 0s.
wenzelm@23146
     9
   The sign Min stands for an infinite string of leading 1s.
wenzelm@23146
    10
wenzelm@23146
    11
See int_of_binary for the numerical interpretation.  A number can have
wenzelm@23146
    12
multiple representations, namely leading 0s with sign Pls and leading 1s with
wenzelm@23146
    13
sign Min.  A number is in NORMAL FORM if it has no such extra bits.
wenzelm@23146
    14
wenzelm@23146
    15
The representation expects that (m mod 2) is 0 or 1, even if m is negative;
wenzelm@23146
    16
For instance, ~5 div 2 = ~3 and ~5 mod 2 = 1; thus ~5 = (~3)*2 + 1
wenzelm@23146
    17
wenzelm@23146
    18
Still needs division!
wenzelm@23146
    19
wenzelm@23146
    20
print_depth 40;
wenzelm@23146
    21
System.Control.Print.printDepth := 350; 
wenzelm@23146
    22
*)
wenzelm@23146
    23
wenzelm@23146
    24
infix 5 $$ $$$
wenzelm@23146
    25
wenzelm@23146
    26
(*Recursive datatype of binary integers*)
wenzelm@23146
    27
datatype bin = Pls | Min | $$ of bin * int;
wenzelm@23146
    28
wenzelm@23146
    29
(** Conversions between bin and int **)
wenzelm@23146
    30
wenzelm@23146
    31
fun int_of_binary Pls = 0
wenzelm@23146
    32
  | int_of_binary Min = ~1
wenzelm@23146
    33
  | int_of_binary (w$$b) = 2 * int_of_binary w + b;
wenzelm@23146
    34
wenzelm@23146
    35
fun binary_of_int 0 = Pls
wenzelm@23146
    36
  | binary_of_int ~1 = Min
wenzelm@23146
    37
  | binary_of_int n = binary_of_int (n div 2) $$ (n mod 2);
wenzelm@23146
    38
wenzelm@23146
    39
(*** Addition ***)
wenzelm@23146
    40
wenzelm@23146
    41
(*Attach a bit while preserving the normal form.  Cases left as default
wenzelm@23146
    42
  are Pls$$$1 and Min$$$0. *)
wenzelm@23146
    43
fun  Pls $$$ 0 = Pls
wenzelm@23146
    44
  | Min $$$ 1 = Min
wenzelm@23146
    45
  |     v $$$ x = v$$x;
wenzelm@23146
    46
wenzelm@23146
    47
(*Successor of an integer, assumed to be in normal form.
wenzelm@23146
    48
  If w$$1 is normal then w is not Min, so bin_succ(w) $$ 0 is normal.
wenzelm@23146
    49
  But Min$$0 is normal while Min$$1 is not.*)
wenzelm@23146
    50
fun bin_succ Pls = Pls$$1
wenzelm@23146
    51
  | bin_succ Min = Pls
wenzelm@23146
    52
  | bin_succ (w$$1) = bin_succ(w) $$ 0
wenzelm@23146
    53
  | bin_succ (w$$0) = w $$$ 1;
wenzelm@23146
    54
wenzelm@23146
    55
(*Predecessor of an integer, assumed to be in normal form.
wenzelm@23146
    56
  If w$$0 is normal then w is not Pls, so bin_pred(w) $$ 1 is normal.
wenzelm@23146
    57
  But Pls$$1 is normal while Pls$$0 is not.*)
wenzelm@23146
    58
fun bin_pred Pls = Min
wenzelm@23146
    59
  | bin_pred Min = Min$$0
wenzelm@23146
    60
  | bin_pred (w$$1) = w $$$ 0
wenzelm@23146
    61
  | bin_pred (w$$0) = bin_pred(w) $$ 1;
wenzelm@23146
    62
wenzelm@23146
    63
(*Sum of two binary integers in normal form.  
wenzelm@23146
    64
  Ensure last $$ preserves normal form! *)
wenzelm@23146
    65
fun bin_add (Pls, w) = w
wenzelm@23146
    66
  | bin_add (Min, w) = bin_pred w
wenzelm@23146
    67
  | bin_add (v$$x, Pls) = v$$x
wenzelm@23146
    68
  | bin_add (v$$x, Min) = bin_pred (v$$x)
wenzelm@23146
    69
  | bin_add (v$$x, w$$y) = 
wenzelm@23146
    70
      bin_add(v, if x+y=2 then bin_succ w else w) $$$ ((x+y) mod 2);
wenzelm@23146
    71
wenzelm@23146
    72
(*** Subtraction ***)
wenzelm@23146
    73
wenzelm@23146
    74
(*Unary minus*)
wenzelm@23146
    75
fun bin_minus Pls = Pls
wenzelm@23146
    76
  | bin_minus Min = Pls$$1
wenzelm@23146
    77
  | bin_minus (w$$1) = bin_pred (bin_minus(w) $$$ 0)
wenzelm@23146
    78
  | bin_minus (w$$0) = bin_minus(w) $$ 0;
wenzelm@23146
    79
wenzelm@23146
    80
(*** Multiplication ***)
wenzelm@23146
    81
wenzelm@23146
    82
(*product of two bins; a factor of 0 might cause leading 0s in result*)
wenzelm@23146
    83
fun bin_mult (Pls, _) = Pls
wenzelm@23146
    84
  | bin_mult (Min, v) = bin_minus v
wenzelm@23146
    85
  | bin_mult (w$$1, v) = bin_add(bin_mult(w,v) $$$ 0,  v)
wenzelm@23146
    86
  | bin_mult (w$$0, v) = bin_mult(w,v) $$$ 0;
wenzelm@23146
    87
wenzelm@23146
    88
(*** Testing ***)
wenzelm@23146
    89
wenzelm@23146
    90
(*tests addition*)
wenzelm@23146
    91
fun checksum m n =
wenzelm@23146
    92
    let val wm = binary_of_int m
wenzelm@23146
    93
        and wn = binary_of_int n
wenzelm@23146
    94
        val wsum = bin_add(wm,wn)
wenzelm@23146
    95
    in  if m+n = int_of_binary wsum then (wm, wn, wsum, m+n)
wenzelm@23146
    96
        else raise Match
wenzelm@23146
    97
    end;
wenzelm@23146
    98
wenzelm@23146
    99
fun bfact n = if n=0 then  Pls$$1  
wenzelm@23146
   100
              else  bin_mult(binary_of_int n, bfact(n-1));
wenzelm@23146
   101
wenzelm@23146
   102
(*Examples...
wenzelm@23146
   103
bfact 5;
wenzelm@23146
   104
int_of_binary it;
wenzelm@23146
   105
bfact 69;
wenzelm@23146
   106
int_of_binary it;
wenzelm@23146
   107
wenzelm@23146
   108
(*For {HOL,ZF}/ex/BinEx.ML*)
wenzelm@23146
   109
bin_add(binary_of_int 13, binary_of_int 19);
wenzelm@23146
   110
bin_add(binary_of_int 1234, binary_of_int 5678);
wenzelm@23146
   111
bin_add(binary_of_int 1359, binary_of_int ~2468);
wenzelm@23146
   112
bin_add(binary_of_int 93746, binary_of_int ~46375);
wenzelm@23146
   113
bin_minus(binary_of_int 65745);
wenzelm@23146
   114
bin_minus(binary_of_int ~54321);
wenzelm@23146
   115
bin_mult(binary_of_int 13, binary_of_int 19);
wenzelm@23146
   116
bin_mult(binary_of_int ~84, binary_of_int 51);
wenzelm@23146
   117
bin_mult(binary_of_int 255, binary_of_int 255);
wenzelm@23146
   118
bin_mult(binary_of_int 1359, binary_of_int ~2468);
wenzelm@23146
   119
wenzelm@23146
   120
wenzelm@23146
   121
(*leading zeros??*)
wenzelm@23146
   122
bin_add(binary_of_int 1234, binary_of_int ~1234);
wenzelm@23146
   123
bin_mult(binary_of_int 1234, Pls);
wenzelm@23146
   124
wenzelm@23146
   125
(*leading ones??*)
wenzelm@23146
   126
bin_add(binary_of_int 1, binary_of_int ~2);
wenzelm@23146
   127
bin_add(binary_of_int 1234, binary_of_int ~1235);
wenzelm@23146
   128
*)