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
clasohm@0
     1
(*  Title: 	ZF/ex/twos-compl.ML
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
clasohm@0
     6
ML code for Arithmetic on binary integers; the model for theory BinFn
clasohm@0
     7
clasohm@0
     8
   The sign Plus stands for an infinite string of leading 0's.
clasohm@0
     9
   The sign Minus stands for an infinite string of leading 1's.
clasohm@0
    10
clasohm@0
    11
A number can have multiple representations, namely leading 0's with sign
clasohm@0
    12
Plus and leading 1's with sign Minus.  See int_of_binary for the numerical
clasohm@0
    13
interpretation.
clasohm@0
    14
clasohm@0
    15
The representation expects that (m mod 2) is 0 or 1, even if m is negative;
clasohm@0
    16
For instance, ~5 div 2 = ~3 and ~5 mod 2 = 1; thus ~5 = (~3)*2 + 1
clasohm@0
    17
clasohm@0
    18
Still needs division!
clasohm@0
    19
clasohm@0
    20
print_depth 40;
clasohm@0
    21
System.Control.Print.printDepth := 350; 
clasohm@0
    22
*)
clasohm@0
    23
clasohm@0
    24
infix 5 $$ 
clasohm@0
    25
clasohm@0
    26
(*Recursive datatype of binary integers*)
clasohm@0
    27
datatype bin = Plus | Minus | op $$ of bin * int;
clasohm@0
    28
clasohm@0
    29
(** Conversions between bin and int **)
clasohm@0
    30
clasohm@0
    31
fun int_of_binary Plus = 0
clasohm@0
    32
  | int_of_binary Minus = ~1
clasohm@0
    33
  | int_of_binary (w$$b) = 2 * int_of_binary w + b;
clasohm@0
    34
clasohm@0
    35
fun binary_of_int 0 = Plus
clasohm@0
    36
  | binary_of_int ~1 = Minus
clasohm@0
    37
  | binary_of_int n = binary_of_int (n div 2) $$ (n mod 2);
clasohm@0
    38
clasohm@0
    39
(*** Addition ***)
clasohm@0
    40
clasohm@0
    41
(*Adding one to a number*)
clasohm@0
    42
fun bin_succ Plus = Plus$$1
clasohm@0
    43
  | bin_succ Minus = Plus
clasohm@0
    44
  | bin_succ (w$$1) = bin_succ(w) $$ 0
clasohm@0
    45
  | bin_succ (w$$0) = w$$1;
clasohm@0
    46
clasohm@0
    47
(*Subtracing one from a number*)
clasohm@0
    48
fun bin_pred Plus = Minus
clasohm@0
    49
  | bin_pred Minus = Minus$$0
clasohm@0
    50
  | bin_pred (w$$1) = w$$0
clasohm@0
    51
  | bin_pred (w$$0) = bin_pred(w) $$ 1;
clasohm@0
    52
clasohm@0
    53
(*sum of two binary integers*)
clasohm@0
    54
fun bin_add (Plus, w) = w
clasohm@0
    55
  | bin_add (Minus, w) = bin_pred w
clasohm@0
    56
  | bin_add (v$$x, Plus) = v$$x
clasohm@0
    57
  | bin_add (v$$x, Minus) = bin_pred (v$$x)
clasohm@0
    58
  | bin_add (v$$x, w$$y) = bin_add(v, if x+y=2 then bin_succ w else w) $$ 
clasohm@0
    59
                           ((x+y) mod 2);
clasohm@0
    60
clasohm@0
    61
(*** Subtraction ***)
clasohm@0
    62
clasohm@0
    63
(*Unary minus*)
clasohm@0
    64
fun bin_minus Plus = Plus
clasohm@0
    65
  | bin_minus Minus = Plus$$1
clasohm@0
    66
  | bin_minus (w$$1) = bin_pred (bin_minus(w) $$ 0)
clasohm@0
    67
  | bin_minus (w$$0) = bin_minus(w) $$ 0;
clasohm@0
    68
clasohm@0
    69
(*** Multiplication ***)
clasohm@0
    70
clasohm@0
    71
(*product of two bins*)
clasohm@0
    72
fun bin_mult (Plus, _) = Plus
clasohm@0
    73
  | bin_mult (Minus, v) = bin_minus v
clasohm@0
    74
  | bin_mult (w$$1, v) = bin_add(bin_mult(w,v) $$ 0,  v)
clasohm@0
    75
  | bin_mult (w$$0, v) = bin_mult(w,v) $$ 0;
clasohm@0
    76
clasohm@0
    77
(*** Testing ***)
clasohm@0
    78
clasohm@0
    79
(*tests addition*)
clasohm@0
    80
fun checksum m n =
clasohm@0
    81
    let val wm = binary_of_int m
clasohm@0
    82
        and wn = binary_of_int n
clasohm@0
    83
        val wsum = bin_add(wm,wn)
clasohm@0
    84
    in  if m+n = int_of_binary wsum then (wm, wn, wsum, m+n)
clasohm@0
    85
        else raise Match
clasohm@0
    86
    end;
clasohm@0
    87
clasohm@0
    88
fun bfact n = if n=0 then  Plus$$1  
clasohm@0
    89
              else  bin_mult(binary_of_int n, bfact(n-1));
clasohm@0
    90
clasohm@0
    91
(*Examples...
clasohm@0
    92
bfact 5;
clasohm@0
    93
int_of_binary it;
clasohm@0
    94
bfact 69;
clasohm@0
    95
int_of_binary it;
clasohm@0
    96
clasohm@0
    97
(*leading zeros!*)
clasohm@0
    98
bin_add(binary_of_int 1234, binary_of_int ~1234);
clasohm@0
    99
bin_mult(binary_of_int 1234, Plus);
clasohm@0
   100
clasohm@0
   101
(*leading ones!*)
clasohm@0
   102
bin_add(binary_of_int 1234, binary_of_int ~1235);
clasohm@0
   103
*)