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
data T a = T
type Proxy = T
proxy :: T a
proxy = T
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))
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
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)
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