{-# OPTIONS -fglasgow-exts #-}

module GSmall where

import Representations

-- (Lazy) Peano numbers.

data Size = Zero | Succ Size
  deriving (Eq, Ord, Show)

num Zero     = 0
num (Succ a) = 1 + num a

sizeAdd Zero     b = b
sizeAdd (Succ a) b = Succ (sizeAdd a b)

-- Generic structural size and minimum.

class GSize f where
  gsize' :: (a -> Size) -> f a -> Size

instance GSize Unit where
  gsize' _ _ = Succ Zero

instance GSize Id where
  gsize' f (Id r) = Succ (f r)

instance GSize (K a) where
  gsize' f _ = Succ Zero

instance (GSize f, GSize g) => GSize (Sum f g) where
  gsize' f (Inl x) = gsize' f x
  gsize' f (Inr y) = gsize' f y

instance (GSize f, GSize g) => GSize (Prod f g) where
  gsize' f (Prod x y) = gsize' f x `sizeAdd` gsize' f y

gsize :: (PFView a, GSize (PF a)) => a -> Size
gsize = gsize' gsize . from

gminimum' :: (GSize f, GSize g) => (a -> Size) -> (b -> Size) -> f a -> g b -> Either (f a) (g b)
gminimum' f g a b = if gsize' f a < gsize' g b then Left a else Right b

gminimum :: (PFView a, GSize (PF a), PFView b, GSize (PF b)) => a -> b -> Either a b
gminimum a b = if gsize a < gsize b then Left a else Right b

-- Small type class for simple types.

class Small a where
  small :: a

instance Small () where
  small = ()

instance Small Bool where
  small = False

instance Small Int where
  small = 0

instance Small Char where
  small = '\NUL'

-- Generic small function. Computes the structural smallest instance of a
-- container certain type.

class GSmall f where
  gsmall' :: (a -> Size) -> a -> f a

instance GSmall Unit where
  gsmall' _ _ = Unit

instance GSmall Id where
  gsmall' _ f = Id f

instance Small a => GSmall (K a) where
  gsmall' _ _ = K small

instance (GSize f, GSize g, GSmall f, GSmall g) => GSmall (Sum f g) where
  gsmall' s f = either Inl Inr
    $ gminimum' s s (gsmall' s f) (gsmall' s f)

instance (GSmall f, GSmall g) => GSmall (Prod f g) where
  gsmall' s f = Prod (gsmall' s f) (gsmall' s f)

gsmall :: (GSize (PF a), GSmall (PF a), PFView a) => a
gsmall = to $ gsmall' gsize gsmall