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

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

import TFHOE.Raw
import TFHOE.Type.Common

-- * Type 'Type_Fun'

data Type_Fun fun next h where
	Type_Fun      :: Type_Fun fun next arg
	              -> Type_Fun fun next res
	              -> Type_Fun fun next (Fun fun arg res)
	Type_Fun_Next :: next h -> Type_Fun fun next h

instance -- Type_Eq
 Type_Eq next =>
 Type_Eq (Type_Fun fun next) where
	type_eq
	 (arg1 `Type_Fun` res1)
	 (arg2 `Type_Fun` res2)
	 | Just Refl <- arg1 `type_eq` arg2
	 , Just Refl <- res1 `type_eq` res2
	 = Just Refl
	type_eq (Type_Fun_Next x)
	        (Type_Fun_Next y) = x `type_eq` y
	type_eq _ _ = Nothing
instance -- Eq
 Type_Eq next =>
 Eq (Type_Fun fun next h) where
	x == y = isJust $ type_eq x y
instance -- Type_from Raw
 Type_from Raw next =>
 Type_from Raw (Type_Fun fun next) where
	type_from (Raw "->" [raw_arg, raw_res]) k =
		type_from raw_arg $ \ty_arg ->
		type_from raw_res $ \ty_res ->
		k (ty_arg `Type_Fun` ty_res)
	type_from raw k = type_from raw $ k . Type_Fun_Next
instance -- String_from_Type
 String_from_Type next =>
 String_from_Type (Type_Fun fun next) where
	string_from_type (arg `Type_Fun` res) =
		"(" ++ string_from_type arg ++ " -> "
		    ++ string_from_type res ++ ")"
	string_from_type (Type_Fun_Next t) = string_from_type t
instance -- Show
 String_from_Type next =>
 Show (Type_Fun fun next h) where
	show = string_from_type

-- ** Type 'Fun'

-- | A type synonym for the host-type function,
-- wrapping argument and result within a type constructor @fun@,
-- which is used in the 'Repr_Host' instance of 'Expr_Fun'
-- to implement 'val' and 'lazy'.
type Fun fun arg res = (fun arg -> fun res)