Bool.hs

{-# LANGUAGE UndecidableInstances, OverlappingInstances, FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables, EmptyDataDecls, MultiParamTypeClasses #-}
{- LANGUAGE TypeOperators -}
{- Enable the above to compile with GHC >= 6.8 -}
{- 6.6 fails to even parse it -}
--
-- .$Header$
module Data.Type.Test.Bool where

import Data.Type.Apply
import Data.Type.Bool
import Data.Type.Eq
import Data.Type.TList

t9 :: TTrue
t9 = tNot hFalse
t10 :: TFalse
t10 = tNot hTrue

data Test a

vtt :: Test TTrue
vtt = undefined

vtf :: Test TFalse
vtf = undefined

t11 :: TFalse
t11 = tNot vtt
t12 :: TTrue
t12 = tNot vtf

t1 :: TFalse
t1 = tAnd hFalse hFalse
t2 :: TFalse
t2 = tAnd hFalse hTrue
t3 :: TFalse
t3 = tAnd hTrue hFalse
t4 :: TTrue
t4 = tAnd hTrue hTrue

t13 :: TFalse
t13 = tAnd vtf vtf
t14 :: TFalse
t14 = tAnd vtf vtt
t15 :: TFalse
t15 = tAnd vtt vtf
t16 :: TTrue
t16 = tAnd vtt vtt

t5 :: TFalse
t5 = tOr hFalse hFalse
t6 :: TTrue
t6 = tOr hFalse hTrue
t7 :: TTrue
t7 = tOr hTrue hFalse
t8 :: TTrue
t8 = tOr hTrue hTrue

t17 :: TFalse
t17 = tOr vtf vtf
t18 :: TTrue
t18 = tOr vtf vtt
t19 :: TTrue
t19 = tOr vtt vtf
t20 :: TTrue
t20 = tOr vtt vtt

data Test2 a b

vt2ff :: Test2 TFalse TFalse
vt2ff = undefined

{-
t21 :: TTrue
t21 = cNot vt2ff
-}

data F = F
data C = C
data X = X

data Member s

member :: Member s
member = undefined

mNil :: Member TNil
mNil = member

mUnit :: a -> Member a
mUnit _ = member

mCons :: Member a -> Member b -> Member (a :*: b)
mCons _ _ = member

infixr 5 `mCons`

instance Apply (Member TNil) a TFalse

instance (TypeEq h a b1, Apply (Member t) a b2, TOr b1 b2 b) =>
    Apply (Member (h :*: t)) a b

class TypeClassify s t where
    typeClassify :: s -> t -> Bool

instance forall t a b. (Apply (Member t) a b, AsBool b) =>
    TypeClassify (Member t) a
  where
    typeClassify _ _ = asBool (undefined :: b)

class AsBool b where
    asBool :: b -> Bool

instance AsBool TTrue where
    asBool _ = True

instance AsBool TFalse where
    asBool _ = False

t22 :: TFalse
t22 = apply mNil F
t23 :: TTrue
t23 = apply (mUnit F `mCons` mNil) F
t24 :: TFalse
t24 = apply (mUnit F `mCons` mNil) C
t25 :: TFalse
t25 = apply (mUnit F `mCons` mUnit C `mCons` mNil) X
t26 :: TTrue
t26 = apply (mUnit F `mCons` mUnit C `mCons` mNil) F
t27 :: TTrue
t27 = apply (mUnit F `mCons` mUnit C `mCons` mNil) C

data Member' s

member' :: Member' s
member' = undefined

mNil' :: Member' TNil
mNil' = member'

mUnit' :: a -> Member' a
mUnit' _ = member'

mCons' :: Member' a -> Member' b -> Member' (a :*: b)
mCons' _ _ = member'

infixr 5 `mCons'`

instance Apply (Member' TNil) a TFalse

instance TypeEq s a b => Apply (Member' s) a b

-- instance TOr (TypeEq h a b1) (Apply (Member' t) a b2) b =>
instance (TypeEq h a b1, Apply (Member' t) a b2, TOr b1 b2 b) =>
    Apply (Member' (h :*: t)) a b

t28 :: TFalse
t28 = apply mNil' F
t29 :: TTrue
t29 = apply (mUnit' F `mCons'` mNil') F
t30 :: TFalse
t30 = apply (mUnit' F `mCons'` mNil') C
t31 :: TFalse
t31 = apply (mUnit' F `mCons'` mUnit' C `mCons'` mNil') X
t32 :: TTrue
t32 = apply (mUnit' F `mCons'` mUnit' C `mCons'` mNil') F
t33 :: TTrue
t33 = apply (mUnit' F `mCons'` mUnit' C `mCons'` mNil') C
t34 :: TFalse
t34 = apply (mUnit' F) X
t35 :: TTrue
t35 = apply (mUnit' F) F

-- vim: expandtab:tabstop=4:shiftwidth=4