{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
module TFHOE.Type.Bool where

import Data.Maybe (isJust)
import Data.Type.Equality ((:~:)(Refl))

import TFHOE.Raw
import TFHOE.Type.Common
import TFHOE.Type.Fun

-- * Type 'Type_Bool'

-- | GADT for integer type:
--
-- * singleton (bijective mapping between Haskell type @h@ and the GADT's terms),
-- * and extensible (through @next@).
data Type_Bool (next:: * -> *) h where
	Type_Bool      :: Type_Bool next Bool -- Introduce an 'Bool' type.
	Type_Bool_Next :: next h -> Type_Bool next h -- Introduce a type extension @next@.

type Type_Fun_Bool fun next = Type_Fun fun (Type_Bool next)
type Type_Fun_Bool_End fun  = Type_Fun_Bool fun Type_End

instance -- Type_Eq
 Type_Eq next =>
 Type_Eq (Type_Bool next) where
	type_eq Type_Bool Type_Bool = Just Refl
	type_eq (Type_Bool_Next x) (Type_Bool_Next y) = x `type_eq` y
	type_eq _ _ = Nothing
instance -- Eq
 Type_Eq next =>
 Eq (Type_Bool next h) where
	x == y = isJust $ type_eq x y
instance -- Type_from Raw
 Type_from Raw next =>
 Type_from Raw (Type_Bool next) where
	type_from (Raw "Bool" []) k = k Type_Bool
	type_from raw k = type_from raw $ k . Type_Bool_Next
instance -- String_from_Type
 String_from_Type next =>
 String_from_Type (Type_Bool next) where
	string_from_type Type_Bool = "Bool"
	string_from_type (Type_Bool_Next t) = string_from_type t
instance -- Show
 String_from_Type next =>
 Show (Type_Bool next h) where
	show = string_from_type