(* * * * * * * * * * *
* Resource Aware ML *
* * * * * * * * * * *
*
* File:
* bitvectors.raml
*
* Author:
* Jan Hoffmann (2010)
*
* Resource Bound:
* O(n^2)
*
* Description:
* A library for bit vectors.
*
* A bit vector is an integer list of 0's and 1's. The first value in
* the list is the least significant bit. For example [1,0] is 1 and
* [0,1] is 2. We interpret the empty list as zero., i.e., [] =
* [0].
*
* We a assume an arbitrary but fixed word length (e.g. 32 bit) for the
* vectors.
*
* The library contains the following functions.
*
* - add(b1,b2): addition b1+b2 of two bit vectors b1 b2. Can produce an
* overflow.
*
* - sub(b1,b2): subtraction of b2 from b1 (b1-b2). Returns [0,...,0] if the
* result is negative.
*
* - compare(b1,b2): -1 if b1 is less then b2, 0 if b1 is equal to b2,
and 1 if b1 is greater then b2.
*
* - leq(b1,b2): b1 < b2 ?
*
* - mult(b1,b2): multiplication of two bit vectors
*
* - Div(b1,b2): division of b1 by b2. The result is undefined in case
* of division by zero. (The function name is upper case
* since div is a RAML key word.)
*
*)
mult : (L(int),L(int)) -> L(int)
(* Multiplies two bit vectors. *)
mult (b1,b2) = let _=tick(1) in
match b1 with
| nil -> nil
| (x::xs) -> let zs = +0::mult(xs,b2) in
if x == 1 then add(b2,zs) else zs;
mult3 : (L(int),L(int),L(int)) -> L(int)
mult3 (b1,b2,b3) = let _=tick(1) in
mult(mult(b1,b2),b2);
(*
eq(mult3(A,B,C),1,[mult(A,B),mult(A,B)],[]).
eq(mult(B1,B2),1,[],[B1=0]).
eq(mult(B1,B2),1,[mult(B1s,B2)],[B1>=1,B1s = B1-1,Zs >=1+B1s]).
eq(mult(B1,B2),1,[mult(B1s,B2),add(B2,Zs)],[B1>=1,B1s = B1-1,Zs =< B1s+1]).
eq(out_mult(B1,B2),0,[],[B1=0]).
eq(out_mult(B1,B2),1,[out_mult(B1s,B2)],[B1>=1,B1s=B1-1]).
eq(out_mult(B1,B2),0,[out_mult(B1s,B2),outadd(B2,Zs)],[B1>=1,B1s=B1-1,Zs=<
B1s+1]).
*)
bitToInt : L(int) -> int
(* Converts a bit vector into an integer. *)
bitToInt b = let _=tick(1) in
bitToInt'(b,+1);
add : (L(int),L(int)) -> L(int)
(* Addition of two bit vectors.*)
add (b1,b2) = let _=tick(1) in
add' (b1,b2,+0);
(*
eq(add(B1,B2),1,[addp(B1,B2,I)],[I=0]).
eq(bitToInt(A),1,[bitToIntp(A,I)],[I=1]).
*)
bitToInt' : (L(int),int) -> int
(* Converts a bit vector into an integer. *)
bitToInt' (b,n) = let _=tick(1) in
match b with
| nil -> +0
| (x::xs) -> x*n + bitToInt'(xs,n*2);
(*
eq(bitToIntp(B,N),1,[],[B=0]).
eq(bitToIntp(B,N),1,[bitToIntp(Bs,M)],[B>=1,Bs=B-1,M=N*2]).
*)
add' : (L(int),L(int),int) -> L(int)
(* Helper function for the addition that takes care of the carryover. *)
add' (b1,b2,r) = let _=tick(1) in
match b1 with
| nil -> nil
| (x::xs) -> match b2 with
| nil -> nil
| (y::ys) -> let (z,r') = sum(x,y,r) in
z::add'(xs,ys,r');
(*
eq(addp(B1,B2,R),1,[],[B1=0]).
eq(addp(B1,B2,R),1,[],[B1>=1,B2=0]).
eq(addp(B1,B2,R),1,[sum(X,Y,R),addp(B1s,B2s,Rs)],[B1>=1,B2>=1,B1s=B1-1,B2s=B2-1]).
*)
sum : (int,int,int) -> (int,int)
(* Helper function for add' that computes the new bit and the new carryover. *)
sum (x,y,r) = let _=tick(1) in
let s = x + y + r in
if s == 0 then (+0,+0)
else if s == 1 then (+1,+0)
else if s == 2 then (+0,+1)
else (+1,+1);
(*
eq(sum(X,Y,R),1,[],[]).
*)
sub : (L(int),L(int)) -> L(int)
(* Subtraction of two bit vectors.
*)
sub (b1,b2) = let (b,_) = sub'(b1,b2,+0) in b;
sub' : (L(int),L(int),int) -> (L(int),int)
(* Helper function of sub that deals with the carryover.
*)
sub' (b1,b2,r) = let _=tick(1) in
match b1 with
| nil -> (nil,r)
| (x::xs) -> match b2 with
| nil -> (nil,r)
| (y::ys) -> let (z,r') = diff(x,y,r) in
let (zs,s) = sub'(xs,ys,r') in
(if s == 1 then +0::zs else z::zs,s);
(*
eq(subp(B1,B2,R),1,[],[B1=0]).
eq(subp(B1,B2,R),1,[],[B1>=1,B2=0]).
eq(subp(B1,B2,R),1,[diff(X,Y,R),subp(B1s,B2s,Rp)],[B1>=1,B2>=1,B1s=B1-1,B2s=B2-1]).
*)
diff : (int,int,int) -> (int,int)
(* Helper function for sub' that computes the new bit and the new carryover. *)
diff(x,y,r) = let _=tick(1) in
( x+y+r mod 2,if x - y - r < 0 then +1 else +0 );
(*
eq(diff(A,B,C),1,[],[]).
*)
leq : (L(int),L(int)) -> bool
leq (b1,b2) = (compare(b1,b2)) < 1;
(*
eq(leq(B1,B2),0,[compare(B1,B2)],[B1>=0,B2>=0]).
*)
compare : (L(int),L(int)) -> int
(* Returns 0 if both arguments are equal,
-1 if the first argument is smaller,
1 if the first argument is greater then the second
*)
compare (b1,b2) = let _=tick(1) in
match b1 with
| nil -> +0
| (x::xs) -> match b2 with
| nil -> +0
| (y::ys) -> let r = compare (xs,ys) in
if r == 0 then if xy then +1 else +0
else r;
(*
eq(compare(B1,B2),1,[],[B1=0]).
eq(compare(B1,B2),1,[],[B1>=1,B2=0]).
eq(compare(B1,B2),1,[compare(B1s,B2s)],[B1>=1,B2>=1,B1s=B1-1,B2s=B2-1]).
*)
main = ()