{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-}

{-
  Representation of binary numbers and arithmetic relations

  Representation
  B0  - 0
  B1  - 1
  U B1 B0  - 2
  U B1 B1  - 3
  U (U B1 B0) B0 - 4
  U (U B1 B1) B0 - 6
  U (U (U B1 B0) B1) B0 - 10

  If we disregard the parenthesis, we see the sequence of U followed by
  the number in the conventional binary notation.
  The number of leading Us is the binary logarithm (if we assume log2 0 = 0),
  or the number of digits in teh number minus 1.

  One could make U an infix operator. But: it would be longer than 1 character.
  When printing types, GHC will print it in prefix notation anyway.

-}


module BinaryNumber (
		     -- Representation
		     B0, B1, U,
		     -- Kind predicates
		     Nat0E, NatE, toInt,
		     -- sample Nat types and values
		     N0, N1, N2, N4, N8,
		     nat0, nat1, nat2, nat4, nat8,
		     -- Arithmetics
		     Succ, succ, pred, Add, add, sub,
		     BLT, BGT, BEQ, NCompare, cmp, NLessEq, NLess, assert_leq,
		     max,
		     Mul, mul, div,
		     Exp2, exp2,
		     GCD, gcd
		    ) where

import Prelude hiding (succ, pred, div, gcd, max, min)

data B0					-- bits
data B1

data U x y				-- the connective

-- The well-formedness condition, the kind predicate
class Nat0 a where toInt :: a -> Int
class Nat0 a => Nat a			-- (positive) naturals

-- To prevent the user from adding new instances to Nat0 and especially
-- to Nat (e.g., to prevent the user from adding the instance |Nat B0|)
-- we do NOT export Nat0 and Nat. Rather, we export the following proxies.
-- The proxies entail Nat and Nat0 and so can be used to add Nat and Nat0
-- constraints in the signatures. However, all the constraints below
-- are expressed in terms of Nat0 and Nat rather than proxies. Thus,
-- even if the user adds new instances to proxies, it would not matter.
-- Besides, because the following proxy instances are most general,
-- one may not add further instances without overlapping instance extension.
class    Nat0 n => Nat0E n
instance Nat0 n => Nat0E n
class    Nat n => NatE n
instance Nat n => NatE n


instance Nat0 B0 where toInt _ = 0
instance Nat0 B1 where toInt _ = 1
instance Nat x => Nat0 (U x B0) where 
    toInt n = 2*(toInt (h n))
      where h :: U x d -> x; h = undefined -- avoiding local tyvar
instance Nat x => Nat0 (U x B1) where
    toInt n = 2*(toInt (h n)) + 1
      where h :: U x d -> x; h = undefined

instance Nat B1
instance Nat x => Nat (U x B0)
instance Nat x => Nat (U x B1)

-- some popular numbers
type N0 = B0
type N1 = B1
type N2 = U B1 B0
type N4 = U (U B1 B0) B0
type N8 = U (U (U B1 B0) B0) B0

nat0 = undefined::N0
nat1 = undefined::N1
nat2 = undefined::N2
nat4 = undefined::N4
nat8 = undefined::N8

tn8 = toInt nat8


-- Addition relation

class (Nat0 x, Nat y) => Succ x y | x -> y, y -> x

-- by structural induction on the first argument
instance Succ B0 B1
instance Succ B1 (U B1 B0)
instance Nat x => Succ (U x B0) (U x B1)
-- this triggers the need for undecidable instances <sigh>
instance (Nat x, Succ x (U y d)) => Succ (U x B1) (U (U y d) B0)

succ :: Succ x y => x -> y; succ = undefined
pred :: Succ x y => y -> x; pred = undefined
tn9 = toInt $ succ nat8
tn7 = toInt $ pred nat8



class (Nat0 x, Nat0 y, Nat0 z) => Add' x y z | x y -> z, z x -> y

-- by structural induction on the first argument
instance Nat0 y   => Add' B0 y y
instance Succ y z => Add' B1 y z
instance (Nat x, Nat (U z dz), Add' x y' z, AddC y' dz y)
    => Add' (U x B0) y (U z dz)
instance (Nat x, Nat0 z, Add' x y' zh, AddC y' dy y, Succ (U zh dy) z)
    => Add' (U x B1) y z

-- Asserting 2*xh + d = x where x is a binary digit. xh may be zero.
-- Essentially, this is the general, non-structural,
-- constructor/deconstructor of a binary number.
class (Nat0 xh, Nat0 x) => AddC xh d x | xh d -> x, x -> xh d

instance AddC B0 B0 B0
instance AddC B0 B1 B1
instance (Nat0 (U B1 d)) => AddC B1 d  (U B1 d)
instance (Nat0 (U x d), Nat0 (U (U x d) d')) => AddC (U x d) d' (U (U x d) d')

-- the addition relation with full dependencies
class (Add' x y z, Add' y x z) => Add x y z | x y -> z, z x -> y, z y -> x
instance (Add' x y z, Add' y x z) => Add x y z

add :: Add x y z => x -> y -> z; add = undefined
sub :: Add x y z => z -> x -> y; sub = undefined

ts16  = add nat8 nat8
ts16' = add (succ nat8) (pred nat8)
ts14  = add (pred nat8) (pred nat8)
ts0   = sub nat8 nat8
ts4   = toInt $ sub nat8 nat4
-- predictable error:
-- ts4'   = sub (undefined::N4) (undefined::N8)


-- Equality and order: the comparison relation
data BLT
data BEQ
data BGT

-- assert that the comparison relation r (BLT, BEQ, or BGT) holds between 
-- x and y
class (Nat0 x, Nat0 y) => NCompare x y r | x y -> r

-- by structural induction on the first, and then the second argument
instance NCompare B0 B0 BEQ
instance NCompare B0 B1 BLT
instance Nat (U y dy) => NCompare B0 (U y dy) BLT
instance NCompare B1 B0 BGT
instance NCompare B1 B1 BEQ
instance Nat (U y dy) => NCompare B1 (U y dy) BLT
instance Nat (U x dx) => NCompare (U x dx) B0 BGT
instance Nat (U x dx) => NCompare (U x dx) B1 BGT
instance (Nat (U x dx), Nat (U y dy), NCompare dx dy dr, NCompare x y r',
	  NCS r' dr r)
    => NCompare (U x dx) (U y dy) r

-- strengthen the comparison relation
class NCS r1 r2 r3 | r1 r2 -> r3
instance NCS BEQ r r
instance NCS BGT r BGT
instance NCS BLT r BLT

cmp :: NCompare x y r => x -> y -> r; cmp = undefined

tc1 = cmp nat0 nat0
tc2 = cmp nat8 nat8
tc3 = cmp (succ nat8) nat8
tc4 = cmp nat8 (succ nat8)
tc5 = cmp (pred nat8) nat8
tc6 = cmp nat8 (pred nat8)

-- Assert that x <= y.
-- This is a popular constraint, so we implement it specially.
-- We could have said that Add n x y => NLessEq x y.
-- The following inductive definition however is a bit more optimal.
class (Nat0 x, Nat0 y) => NLessEq x y
instance NLessEq B0 B0
instance NLessEq B0 B1
instance Nat (U y dy) => NLessEq B0 (U y dy)
instance NLessEq B1 B1
instance Nat (U y dy) => NLessEq B1 (U y dy)
instance (Nat x, Nat y, NLessEq x y) => NLessEq (U x B0) (U y B0)
instance (Nat x, Nat y, NLessEq x y) => NLessEq (U x B1) (U y B1)
instance (Nat x, Nat y, NLessEq x y) => NLessEq (U x B0) (U y B1)
instance (Nat x, Nat y, NCompare x y BLT) => NLessEq (U x B1) (U y B0)

assert_leq :: NLessEq x y => x -> y -> (); assert_leq = undefined

tle1  = assert_leq nat0 nat0
tle2  = assert_leq nat8 nat8
tle3  = assert_leq nat4 nat8
-- tle31 = assert_leq nat8 nat4		-- expected error
tle4  = assert_leq nat8 (succ nat8)
tle5  = assert_leq (pred nat8) (succ nat8)
tle6  = assert_leq (pred nat8) nat8
-- tle61  = assert_leq nat8 (pred nat8) -- expected error

-- Choose the largest of x and y in the order b
class NMax x y b r | x y b -> r
instance NMax x y BLT y
instance NMax x y BEQ y
instance NMax x y BGT x

max :: (NCompare x y b, NMax x y b r) => x -> y -> r
max = undefined

tmx1 = max nat4 nat8
tmx2 = max nat8 nat4
tmx3 = max nat8 nat8

-- Multiplication relation

-- We assert that x * y = z, with x > 0
class (Nat x, Nat0 y, Nat0 z) => Mul' x y z | x y -> z, x z -> y

-- by structural induction on the first argument
instance Nat0 y => Mul' B1 y y
instance (Mul' x y zh, AddC zh B0 z) => Mul' (U x B0) y z

instance (Mul'F x y z,  Mul'B x y z) => Mul' (U x B1) y z

-- We assert that (2x+1) * y = z with x > 0
class (Nat x, Nat0 y, Nat0 z) => Mul'F x y z | x y -> z

instance Nat x => Mul'F x B0 B0
instance Nat x => Mul'F x B1 (U x B1)

-- (2x+1) * 2y
instance (Mul'F x y z, Nat x, Nat y, Nat z) => Mul'F x (U y B0) (U z B0)

-- (2x+1) * (2y+1) = 2*( (2x+1)*y + x ) + 1, y > 0
instance (Mul'F x y z', Add x z' z, Nat x, Nat y, Nat z) 
    => Mul'F x (U y B1) (U z B1)

-- We assert that (2x+1) * y = z with x > 0
-- The functional dependencies go the other way though
class (Nat x, Nat0 y, Nat0 z) => Mul'B x y z | z x -> y
instance Nat x => Mul'B x B0 B0
-- instance Nat x => Mul'B x y B1 -- cannot happen

-- (2x+1) * 2y
instance (Mul'B x y z, Nat x, Nat y, Nat z) => Mul'B x (U y B0) (U z B0)
-- (2x+1) * (2y+1) = 2*( (2x+1)*y + x ) + 1, y >= 0
instance (AddC y B1 yt, Mul'B x y z', Add x z' z, Nat x, Nat z) 
    => Mul'B x yt (U z B1)

class (Mul' x y z, Mul' y x z) => Mul x y z | x y -> z, x z -> y, y z -> x
instance (Mul' x y z, Mul' y x z) => Mul x y z


mul :: Mul x y z => x -> y -> z; mul = undefined
div :: Mul x y z => z -> x -> y; div = undefined


tm1   = mul nat2 nat8
tm2   = toInt $ mul nat8 nat2
tm3   = toInt $ mul (succ nat2) nat2
tm4   = toInt $ mul nat2 (succ nat2)
tm5   = toInt $ mul (succ nat4) (succ nat2)
tm6   = toInt $ mul (succ nat2) (succ nat4) 
tm7   = toInt $ div (mul (succ nat8) nat2) (succ nat2) -- 18/3

-- Power-of-two Exponentiation/Logarithm relation

-- Exp2 x y asserts y = 2^x
class (Nat0 x, Nat y) => Exp2 x y | x -> y, y -> x

instance Exp2 B0 B1
instance Exp2 B1 (U B1 B0)
instance (Succ x1 (U x d), Exp2 x1 (U y B0)) => Exp2 (U x d) (U (U y B0) B0)

exp2 :: Exp2 x y => x -> y; exp2 = undefined
log2 :: Exp2 x y => y -> x; log2 = undefined


te1 = exp2 (succ (succ nat8))
te1' = toInt $ exp2 (succ (succ nat8))
te2  = toInt $ log2 nat8


-- GCD: Euclid algorithm

-- GCD x y z asserts that gcd(x,y) is z
-- Do we need the full dependency? If we know x and we know z,
-- we can't tell what y exactly (except being the multiple of z)
class (Nat0 x, Nat0 y, Nat0 z) => GCD x y z | x y -> z

instance Nat0 y => GCD B0 y y
instance Nat0 y => GCD B1 y B1
instance (NCompare (U x dx) y r, GCD' r (U x dx) y z) => GCD (U x dx) y z

class (Nat x, Nat0 y, Nat0 z) => GCD' r x y z | r x y -> z

instance Nat x => GCD' BEQ x x x
instance (GCD y x z, Nat x) => GCD' BGT x y z
instance (Add x y1 y, GCD y1 x z, Nat x) => GCD' BLT x y z

gcd :: GCD x y z => x -> y -> z; gcd = undefined

tg1 = toInt $ gcd nat8 nat8
tg2 = toInt $ gcd nat8 (pred nat8)
tg3 = toInt $ gcd nat8 (pred (pred nat8))
tg4 = toInt $ gcd (pred (pred nat8)) nat8
tg5 = toInt $ gcd nat4 nat8
tg6 = toInt $ gcd (pred nat4) (succ nat8)
tg7 = toInt $ gcd (succ nat8) (pred nat4)

-- Shorthand for less-than
class (Nat0 x, Nat y) => NLess x y
instance (Succ y' y, NLessEq x y') => NLess x y