{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Language.LOL.Symantic.Expr.Lambda where

import Data.Proxy (Proxy(..))
import Data.Type.Equality ((:~:)(Refl))

import Language.LOL.Symantic.AST
import Language.LOL.Symantic.Type
import Language.LOL.Symantic.Expr.Common
import Language.LOL.Symantic.Repr.Dup

-- * Class 'Sym_Lambda'

-- | /Tagless-final symantics/ for /lambda abstraction/
-- in /higher-order abstract syntax/ (HOAS),
-- and with argument @arg@ and result @res@ of 'Lambda'
-- wrapped inside 'lam': to control the calling
-- in the 'Repr_Host' instance.
class (lam ~ Lambda_from_Repr repr) => Sym_Lambda lam repr where
	-- | This type constructor is used like
	-- the functional dependency: @repr -> lam@
	-- (ie. knowing @repr@ one can determine @lam@)
	-- in order to avoid to introduce a 'Proxy' @lam@
	-- in 'let_inline', 'let_val' and 'let_lazy'.
	--
	-- Distinguishing between @lam@ and @repr@ is used to maintain
	-- the universal polymorphism of @repr@ in 'Sym_from',
	-- the downside with this however is that
	-- to be an instance of 'Sym_Lambda' for all @lam@,
	-- the @repr@ type of an interpreter
	-- has to be parameterized by @lam@,
	-- even though it does not actually need @lam@ to do its work.
	--
	-- Basically this means having sometimes to add a type annotation
	-- to the interpreter call to specify @lam@.
	type Lambda_from_Repr repr :: {-lam-}(* -> *)
	
	-- | Lambda application.
	app :: repr (Lambda lam arg res) -> repr arg -> repr res
	
	-- | /Call-by-name/ lambda.
	inline :: (repr arg -> repr res) -> repr (Lambda lam arg res)
	-- | /Call-by-value/ lambda.
	val    :: (repr arg -> repr res) -> repr (Lambda lam arg res)
	-- | /Call-by-need/ lambda (aka. /lazyness/): lazy shares its argument, no matter what.
	lazy   :: (repr arg -> repr res) -> repr (Lambda lam arg res)
	
	-- | Convenient 'inline' wrapper.
	let_inline
	 :: Sym_Lambda lam repr
	 => repr arg -> (repr arg -> repr res) -> repr res
	let_inline x y = inline y `app` x
	-- | Convenient 'val' wrapper.
	let_val
	 :: Sym_Lambda lam repr
	 => repr arg -> (repr arg -> repr res) -> repr res
	let_val x y = val y `app` x
	-- | Convenient 'lazy' wrapper.
	let_lazy
	 :: Sym_Lambda lam repr
	 => repr arg -> (repr arg -> repr res) -> repr res
	let_lazy x y = lazy y `app` x

infixl 5 `app`

instance -- Sym_Lambda Dup
 ( Sym_Lambda lam r1
 , Sym_Lambda lam r2
 ) => Sym_Lambda lam (Dup r1 r2) where
	type Lambda_from_Repr (Dup r1 r2) = Lambda_from_Repr r1
	app (f1 `Dup` f2) (x1 `Dup` x2) = app f1 x1 `Dup` app f2 x2
	inline f = dup1 (inline f) `Dup` dup2 (inline f)
	val    f = dup1 (val f)    `Dup` dup2 (val f)
	lazy   f = dup1 (lazy f)   `Dup` dup2 (lazy f)

-- * Type 'Expr_Lambda'
data Expr_Lambda (lam:: * -> *) (root:: *)
type instance Root_of_Expr (Expr_Lambda lam root) = root
type instance Type_of_Expr (Expr_Lambda lam root) = Type_Fun lam
type instance Sym_of_Expr (Expr_Lambda lam root) repr = Sym_Lambda lam repr
type instance Error_of_Expr raw (Expr_Lambda lam root)
 = Error_Expr_Lambda (Error_of_Type raw (Type_Root_of_Expr root))
                     (Type_Root_of_Expr root)
                     raw
 -- NOTE: require UndecidableInstances.

instance -- Sym_from AST Expr_Lambda
 ( Type_from AST (Type_Root_of_Expr root)
 , Sym_from AST root
 
 , Type_Root_Lift (Type_Fun lam) (Type_Root_of_Expr root)
 , Error_Type_Lift (Error_Type_Fun AST)
                   (Error_of_Type AST (Type_Root_of_Expr root))
 , Error_Expr_Lift (Error_Expr_Lambda (Error_of_Type AST (Type_Root_of_Expr root))
                                      (                   Type_Root_of_Expr root)
                                      AST)
                   (Error_of_Expr AST root)
 
 , Type_Unlift (Type_Fun lam) (Type_of_Expr root)
 
 , Root_of_Expr root ~ root
 ) => Sym_from AST (Expr_Lambda lam root) where
	sym_from _px_ex ctx raw k =
		case raw of
		 AST "var" raws ->
			case raws of
			 [AST name []] -> go ctx k
				where
				go
				 :: forall hs ret
				 . Context (Var root) hs
				 -> ( forall h
				    .  Type_Root_of_Expr root h
				    -> Forall_Repr_with_Context (Expr_Lambda lam root) hs h
				    -> Either (Maybe (Error_of_Expr AST root)) ret )
				 -> Either (Maybe (Error_of_Expr AST root)) ret
				go c k' =
					case c of
					 Context_Empty -> Left $ Just $ error_lambda_lift $
						Error_Expr_Lambda_Var_unbound name raw
					 Var n ty `Context_Next` _ | n == name ->
						k' ty $ Forall_Repr_with_Context $
						 \(repr `Context_Next` _) -> repr
					 _ `Context_Next` ctx' ->
						go ctx' $ \ty (Forall_Repr_with_Context repr) ->
							k' ty $ Forall_Repr_with_Context $
							 \(_ `Context_Next` c') -> repr c'
			 _ -> Left $ Just $ error_lambda_lift $
				Error_Expr_Fun_Wrong_number_of_arguments 1 raw
		 AST "app" raws ->
			case raws of
			 [raw_lam, raw_arg_actual] ->
				sym_from (Proxy::Proxy root) ctx raw_lam $
				 \(ty_lam::Type_Root_of_Expr root h_lam) (Forall_Repr_with_Context lam) ->
				sym_from (Proxy::Proxy root) ctx raw_arg_actual $
				 \(ty_arg_actual::Type_Root_of_Expr root h_arg_actual)
				  (Forall_Repr_with_Context arg_actual) ->
					case type_unlift $ unType_Root ty_lam of
					 Just (ty_arg_expected `Type_Fun` ty_res
					  :: Type_Fun lam (Type_Root_of_Expr root) h_lam) ->
						case ty_arg_expected `type_eq` ty_arg_actual of
						 Just Refl ->
							k ty_res $ Forall_Repr_with_Context $
							 \c -> lam c `app` arg_actual c
						 Nothing -> Left $ Just $ error_lambda_lift $
							Error_Expr_Fun_Argument_mismatch
							 (Exists_Type ty_arg_expected)
							 (Exists_Type ty_arg_actual) raw
					 Nothing -> Left $ Just $ error_lambda_lift $
						Error_Expr_Lambda_Not_a_lambda raw
			 _ -> Left $ Just $ error_lambda_lift $
				Error_Expr_Type
				 (error_type_lift $
					Error_Type_Fun_Wrong_number_of_arguments 2 raw
				 ) raw
		 AST "inline" raws -> lambda_from raws inline
		 AST "val"    raws -> lambda_from raws val
		 AST "lazy"   raws -> lambda_from raws lazy
		 _ -> Left Nothing
		where
		lambda_from raws
		 (lam::forall repr arg res. Sym_Lambda lam repr
		     => (repr arg -> repr res) -> repr (Lambda lam arg res)) =
			case raws of
			 [AST name [], raw_ty_arg, raw_body] ->
				case type_from (Proxy::Proxy (Type_Root_of_Expr root)) raw_ty_arg
				 (Right . Exists_Type) of
				 Left Nothing -> Left Nothing
				 Left (Just err) -> Left $ Just $ error_lambda_lift $ Error_Expr_Type err raw
				 Right (Exists_Type (ty_arg::Type_Root_of_Expr root h_arg)) ->
					sym_from (Proxy::Proxy root)
					 (Var name ty_arg `Context_Next` ctx) raw_body $
					 \(ty_res::Type_Root_of_Expr root h_res) (Forall_Repr_with_Context res) ->
						k (ty_arg `type_fun` ty_res
						 :: Root_of_Type (Type_Root_of_Expr root)
						                 (Lambda lam h_arg h_res)) $
						Forall_Repr_with_Context $
						 \c -> lam $ \arg -> res (arg `Context_Next` c)
			 _ -> Left $ Just $ error_lambda_lift $
				Error_Expr_Fun_Wrong_number_of_arguments 3 raw
		error_lambda_lift
		 :: Error_Expr_Lambda (Error_of_Type AST (Type_Root_of_Expr root)) (Type_Root_of_Expr root) AST
		 -> Error_of_Expr AST root
		error_lambda_lift = error_expr_lift

-- * Type 'Error_Expr_Lambda'
data Error_Expr_Lambda err_ty ty raw
 =   Error_Expr_Lambda_Not_a_lambda raw
 |   Error_Expr_Lambda_Var_unbound Var_Name raw
 |   Error_Expr_Fun_Wrong_number_of_arguments Int raw
 |   Error_Expr_Fun_Argument_mismatch (Exists_Type ty) (Exists_Type ty) raw
 |   Error_Expr_Type err_ty raw
 deriving (Eq, Show)