curry := f -> x -> y -> f (x, y); #from stdlib

#
# Implementation of binary numbers.
#

inc := 
	Nil		=> (One, Nil)
|	(Zero, s)	=> (One, s)
|	(One, s)	=> (Zero, inc s)
;

dec := 
	(Zero, s)	=> (One, dec s)
|	(One, s)	=> (Zero, s)
;

add := curry( 
	(Nil, x)			=> x
|	(x, Nil)			=> x
|	((Zero, l), (Zero, r))		=> (Zero, add l r)
|	((Zero, l), (One, r))		=> (One, add l r)
|	((One, l), (Zero, r))		=> (One, add l r)
|	((One, l), (One, r))		=> (Zero, inc (add l r))
);

nativize := 
	Nil		=> 0
|	(Zero, r)	=> 2 * (nativize r)
|	(One, r)	=> 1 + 2 * (nativize r)
;

digit := 
	0	=> Zero
|	1	=> One
;

convert := 
	0	=> Nil
|	n	=> (digit (n % 2), convert (n / 2))
;