{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts      #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  GSize
-- Copyright   :  (c) 2008 Universiteit Utrecht
-- License     :  BSD3
--
-- Maintainer  :  generics@haskell.org
-- Stability   :  experimental
-- Portability :  non-portable
--
-- Generic constructor names.
--
-----------------------------------------------------------------------------

module GSize where

-- import ConNames
-- import IndexEq

import Generics.MultiRec.Base

-- import Generics.MultiRec.Constructor

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

one = Succ Zero 

instance Num Nat where
  Zero     + y  =  y
  (Succ x) + y  =  Succ (x + y)
  fromInteger n | n < 0 = error ("Cannot create a Nat from " ++ show n)
  fromInteger 0     = Zero
  fromInteger (n+1) = Succ (fromInteger n)

-- s really necessary (not for Eq, for example, check)
class GSize (f :: (* -> *) -> (* -> *) -> * -> *) where 
    hsize ::  s ix -> f s r ix -> (forall ix. Ix s ix => s ix -> r ix -> Nat) -> Nat

instance (GSize f,GSize g) => GSize (f :+: g) where
    hsize ix (L x) f = hsize ix x f
    hsize ix (R y) f = hsize ix y f
    
instance (GSize f,Constructor c) => GSize (C c f) where
    hsize ix (C x) f = one + (hsize ix x f)

instance GSize f => GSize (f :>: ix) where
    hsize ix (Tag x) f = hsize ix x f

instance GSize (I xi) where
    hsize ix (I x) f = f index x 
    
instance (GSize f, GSize g) => GSize (f :*: g) where
    hsize ix (x :*: y) f = hsize ix x f + hsize ix y f
    
instance GSize (K Char) where
    hsize ix x f = Zero

instance GSize (K [a]) where
    hsize ix x f = Zero

instance GSize (K ()) where
    hsize ix x f = Zero
    
instance GSize (K Float) where
    hsize ix x f = Zero

instance GSize (K Int) where
    hsize ix x f = Zero

gsize :: (Ix s ix, GSize (PF s)) => s ix -> ix -> Nat
gsize ix x = hsize ix (from x) (\ix (I0 x) -> gsize ix x)

--------------------------------------------------------------------------------