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` ```*) ```