{-# LANGUAGE PolyKinds, TypeOperators, MultiParamTypeClasses, FunctionalDependencies,
    FlexibleContexts, UndecidableInstances, FlexibleInstances, ConstraintKinds, 
    KindSignatures, DataKinds, ScopedTypeVariables #-}

module Prelude.Type.Value where

import qualified Prelude
   (Show(show), Integer, IO, print, (+), (>>), return, String, undefined)
import Prelude(
  Bool(False, True),
  Maybe(Nothing, Just),
  Either(Left, Right),
  Ordering(LT, GT, EQ)
  )

import GHC.Prim
import GHC.TypeLits
import Data.Typeable
import Data.Bits (shift)

import Prelude.Type.Integer

-- | Proxy Type

data T a = T

type Proxy = T

proxy :: T a
proxy = T

-- * Values and Main

-- | Convert a type to a value

class Value (a :: k) (t :: *) | k -> t where value :: T a -> t 

instance (c a, Value a t) => Value (c :: k -> Constraint) t
  where value _ = value (T::T a)

instance (Value a t, Prelude.Show t) => Prelude.Show (T a) where
   show _ = Prelude.show (value (T::T a))

-- | Main
-- 
-- Example Main.hs:
--   
-- {-# LANGUAGE DataKinds, FlexibleInstances, MultiParamTypeClasses, FlexibleContexts, UndecidableInstances #-}
-- module Main (main) where
-- import Prelude.Type
-- instance Compare '[I 1, I 3] '[I 1, I 2] a
--     => Main a
-- 
-- $ ghc-stage2 Main.hs
-- $ ./Main
-- GT

type Main = Main'' ()

class Main'' a b | a -> b

class Main' m a | m -> a where main :: m (T a)
instance (Prelude.Show t, Value a t, Main'' () a) => Main' Prelude.IO a
    where main = let t = (T :: T a) in Prelude.print (value t) Prelude.>> Prelude.return t

-- Value instances

instance Value '() () where value _ = ()

instance Value a t => Value (Just a) (Maybe t)
    where value _ = Just (value (T::T a))
instance Value Nothing (Maybe t) where value _ = Nothing

instance Value True Bool where value _ = True
instance Value False Bool where value _ = False

instance Value LT Ordering where value _ = LT
instance Value EQ Ordering where value _ = EQ
instance Value GT Ordering where value _ = GT

instance Value a t => Value (Left a) (Either t s)
    where value _ = Left (value (T::T a))
instance Value a t => Value (Right a) (Either s t)
    where value _ = Right (value (T::T a))

instance (Value a t, Value b u) => Value '(a, b) (t, u)
    where value _ = (value (T::T a), value (T::T b))
instance (Value a t, Value b u, Value c v) => Value '(a, b, c) (t, u, v)
    where value _ = (value (T::T a), value (T::T b), value (T::T c))
instance (Value a t, Value b u, Value c v, Value d w) => Value '(a, b, c, d) (t, u, v, w)
    where value _ = (value (T::T a), value (T::T b), value (T::T c), value (T::T d))

instance SingI t => Value (t :: Nat) Prelude.Integer
         where value _ = fromSing (sing :: Sing t)

instance SingI t => Value (t :: Symbol) Prelude.String
         where value _ = fromSing (sing :: Sing t)

-- >>> T :: T (Kind (Nothing :: Maybe Bool))
-- Maybe Bool
instance Typeable t => Value t TypeRep where
  value T = typeOf (Prelude.undefined :: t)

instance Value '[] [a] where value _ = []
instance (Value x y, Value xs [y]) => Value (x ': xs) [y]
   where value _ = value (T :: T x) : value (T :: T xs)

instance Value Zeros Prelude.Integer where value _ = 0
instance Value Ones Prelude.Integer where value _ = -1
instance (Value i Prelude.Integer) => Value (One i) Prelude.Integer
    where value _ = shift (value (T::T i)) 1 Prelude.+ 1
instance (Value i Prelude.Integer) => Value (Zero i) Prelude.Integer
    where value _ = shift (value (T::T i)) 1