{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Language.LOL.Symantic.Type.Fun where

import Control.Arrow (left)
import Data.Maybe (isJust)
import Data.Type.Equality ((:~:)(Refl))
import Data.Proxy

import Language.LOL.Symantic.AST
import Language.LOL.Symantic.Type.Common

-- * Type 'Type_Fun'

-- | The function type.
data Type_Fun lam root h where
	Type_Fun :: root h_arg
	         -> root h_res
	         -> Type_Fun lam root (Lambda lam h_arg h_res)

type instance Root_of_Type (Type_Fun lam root) = root
type instance Error_of_Type ast (Type_Fun lam root) = Error_Type_Fun ast

-- | Convenient alias to include a 'Type_Fun' within a type.
type_fun
 :: Type_Root_Lift (Type_Fun lam) root
 => root h_arg -> root h_res
 -> root (Lambda lam h_arg h_res)
type_fun arg res = type_root_lift (Type_Fun arg res)

instance -- Type_Eq
 Type_Eq root =>
 Type_Eq (Type_Fun lam root) 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 _ _ = Nothing
instance -- Eq
 Type_Eq root =>
 Eq (Type_Fun lam root h) where
	x == y = isJust $ type_eq x y
instance -- Type_from AST
 ( Type_Eq root
 , Type_from AST root
 , Type_Root_Lift (Type_Fun lam) root
 , Error_Type_Lift (Error_Type AST) (Error_of_Type AST root)
   -- NOTE: require UndecidableInstances.
 , Error_Type_Lift (Error_Type_Fun AST) (Error_of_Type AST root)
   -- NOTE: require UndecidableInstances.
 , Error_Type_Unlift (Error_Type AST) (Error_of_Type AST root)
 , Root_of_Type root ~ root
 , Implicit_HBool (Is_Last_Type (Type_Fun lam root) root)
 ) => Type_from AST (Type_Fun lam root) where
	type_from _px_ty ast k =
		case ast of
		 AST "->" asts ->
			case asts of
			 [ast_arg, ast_res] ->
				left (\err ->
					case error_type_unlift err of
					 Just (Error_Type_Unsupported_here (a::AST)) ->
						error_type_lift $ Error_Type_Unsupported a
					 _ -> err) $
				type_from (Proxy::Proxy root) ast_arg $ \(ty_arg::root h_arg) ->
				type_from (Proxy::Proxy root) ast_res $ \(ty_res::root h_res) ->
					k (type_root_lift $ ty_arg `Type_Fun` ty_res
					 :: root (Lambda lam h_arg h_res))
			 _ -> Left $ error_type_lift $
				Error_Type_Fun_Wrong_number_of_arguments 2 ast
		 _ -> Left $
			case hbool :: HBool (Is_Last_Type (Type_Fun lam root) root) of
			 HTrue  -> error_type_lift $ Error_Type_Unsupported ast
			 HFalse -> error_type_lift $ Error_Type_Unsupported_here ast
instance -- String_from_Type
 String_from_Type root =>
 String_from_Type (Type_Fun lam root) where
	string_from_type (arg `Type_Fun` res) =
		"(" ++ string_from_type arg ++ " -> "
		    ++ string_from_type res ++ ")"
instance -- Show
 String_from_Type root =>
 Show (Type_Fun lam root h) where
	show = string_from_type

-- ** Type 'Lambda'

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

-- * Type 'Error_Type_Fun'

-- | The 'Error_of_Type' of 'Type_Fun'.
data Error_Type_Fun ast
 =   Error_Type_Fun_Wrong_number_of_arguments Int ast
 deriving (Eq, Show)