(* Author: Carsten Schuermann *)
(* An adder for arbitrary many bits *)


(* ha x y = Cs

   Invariant:
   Cs = [c, z] where c, z are two circuits that
   form a halfadder and that
   compute the carry c and the sum z of x+y
*)
fun ha x y =
  [ANDGate (x, y),			(* Carry *)
   XORGate (x, y)]			(* Bitwise Addition *)
  
(* fa x y b = Cs

   Invariant:
   Cs = [c, z] where c, z are two circuits that
   form a halfadder and that
   compute the carry c and the sum of z = x+y+b
*)
fun fa x y b =
  [ORGate (ORGate (ANDGate (x, y),	(* Carry *)
		   ANDGate (y, b)),
	   ANDGate (x, b)),
   XORGate (XORGate (x, y), b)]		(* Bitwise Addition *)

(* fourbitadder x3 x2 x1 x0 y3 y2 y1 y0 b = Cs

   Invariant:
   Cs = [c, z3, z2, z1, z0] where c, z3, z2, z1 are circuits that
   compute the carry c and the sum of z3z2z1z0 = x3x2x1x0+y3y2y1y0
*)
fun fourbitadder x3 x2 x1 x0 y3 y2 y1 y0 =
    let 
      val [c0, z0] = ha x0 y0
      val [c1, z1] = fa x1 y1 c0
      val [c2, z2] = fa x2 y2 c1
      val [c3, z3] = fa x3 y3 c2
    in
      [c3,z3,z2,z1,z0]
    end

(* nbitadder xs ys = Cs

   Invariant:
   Cs = c :: zs where c, zs are circuits that
   compute the carry c and the sum of zs = xs + ys
*)
fun nbitadder [x]       [y]       = 
    ha x y
  | nbitadder (x :: xs) (y :: ys) = 
    let
      val c :: zs = nbitadder xs ys
      val [c', z] = fa x y c
    in
      c' :: z :: zs
    end




fun intToCircuit b n = intToCircuit' b n []
and intToCircuit' 0 0 a = a
  | intToCircuit' b 0 a = intToCircuit' (b-1) 0 (SIGNAL O :: a) 
  | intToCircuit' b n a = 
    if n mod 2 = 0 then intToCircuit' (b-1) (n div 2) (SIGNAL O :: a)
    else intToCircuit' (b-1) (n div 2) (SIGNAL I :: a)

 
fun circuitToInt C =
    let 
      val (_, n) = circuitToInt' C
    in
      n
    end
and circuitToInt' [] = (1, 0)
  | circuitToInt' (SIGNAL O :: cs) =
    let 
      val (f, n) = circuitToInt' cs
    in
      (2*f, n)
    end
  | circuitToInt' (SIGNAL I :: cs) =
    let 
      val (f, n) = circuitToInt' cs
    in
      (2*f, n + f)
    end



fun test b x y = 
    let
      val c1 = intToCircuit b x
      val c2 = intToCircuit b y
      val c3 = nbitadder c1 c2
      val c4 = simulateList c3
    in
      circuitToInt c4
    end