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

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

import TFHOE.Raw
import TFHOE.Type.Common
import TFHOE.Type.Bool

-- * Type 'Type_Int'

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

type Type_Fun_Bool_Int repr next = Type_Fun_Bool repr (Type_Int next)
type Type_Fun_Bool_Int_End repr  = Type_Fun_Bool_Int repr Type_End

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