{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
-- | Expression for /lambda abstraction/s
-- in /Higher-Order Abstract Syntax/ (HOAS).
module Language.Symantic.Expr.Lambda where

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

import Language.Symantic.Type
import Language.Symantic.Expr.Common
import Language.Symantic.Trans.Common

-- * Class 'Lambda_from_Repr'
-- | 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 'Expr_from';
-- a downside of this approach 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 when it does not actually need @lam@ to do its work
-- (eg. 'Repr_Text').
--
-- Basically this means having sometimes to add a type annotation
-- to the interpreter call to specify @lam@.
type family Lambda_from_Repr (repr:: * -> *) :: {-lam-}(* -> *)

-- * Class 'Sym_Lambda_App'
-- | Symantic.
class (lam ~ Lambda_from_Repr repr) => Sym_Lambda_App lam repr where
	-- | /Lambda application/.
	app :: repr (Lambda lam arg res) -> repr arg -> repr res
	default app    :: Trans t repr => t repr (Lambda lam arg res) -> t repr arg -> t repr res
	app  f x = trans_lift $ trans_apply f `app` trans_apply x
infixl 5 `app`
-- * Class 'Sym_Lambda_Inline'
-- | Symantic.
class (lam ~ Lambda_from_Repr repr, Sym_Lambda_App lam repr) => Sym_Lambda_Inline lam repr where
	-- | /Call-by-name/ /lambda abstraction/.
	inline :: (repr arg -> repr res) -> repr (Lambda lam arg res)
	default inline :: Trans t repr => (t repr arg -> t repr res) -> t repr (Lambda lam arg res)
	inline f = trans_lift $ inline $ trans_apply . f . trans_lift
	
	-- | Convenient 'inline' wrapper.
	let_inline
	 :: Sym_Lambda_Inline lam repr
	 => repr var -> (repr var -> repr res) -> repr res
	let_inline x y = inline y `app` x
-- * Class 'Sym_Lambda_Val'
-- | Symantic.
class (lam ~ Lambda_from_Repr repr, Sym_Lambda_App lam repr) => Sym_Lambda_Val lam repr where
	-- | /Call-by-value/ /lambda abstraction/.
	val :: (repr arg -> repr res) -> repr (Lambda lam arg res)
	default val :: Trans t repr => (t repr arg -> t repr res) -> t repr (Lambda lam arg res)
	val f = trans_lift $ val $ trans_apply . f . trans_lift
	
	-- | Convenient 'val' wrapper.
	let_val
	 :: Sym_Lambda_Val lam repr
	 => repr var -> (repr var -> repr res) -> repr res
	let_val x y = val y `app` x
-- * Class 'Sym_Lambda_Lazy'
-- | Symantic.
class (lam ~ Lambda_from_Repr repr, Sym_Lambda_App lam repr) => Sym_Lambda_Lazy lam repr where
	-- | /Call-by-need/ /lambda abstraction/ (aka. /lazyness/): lazy shares its argument, no matter what.
	lazy :: (repr arg -> repr res) -> repr (Lambda lam arg res)
	default lazy :: Trans t repr => (t repr arg -> t repr res) -> t repr (Lambda lam arg res)
	lazy f = trans_lift $ lazy $ trans_apply . f . trans_lift
	
	-- | Convenient 'lazy' wrapper.
	let_lazy
	 :: Sym_Lambda_Lazy lam repr
	 => repr var -> (repr var -> repr res) -> repr res
	let_lazy x y = lazy y `app` x

-- * Type 'Expr_Lambda_App'
-- | Expression.
data Expr_Lambda_App (lam:: * -> *) (root:: *)
type instance Root_of_Expr      (Expr_Lambda_App lam root)      = root
type instance Type_of_Expr      (Expr_Lambda_App lam root)      = Type_Fun lam
type instance Sym_of_Expr       (Expr_Lambda_App lam root) repr = Sym_Lambda_App lam repr
type instance Error_of_Expr ast (Expr_Lambda_App lam root)      = Error_Expr_Lambda ast

-- * Type 'Expr_Lambda_Inline'
-- | Expression.
data Expr_Lambda_Inline (lam:: * -> *) (root:: *)
type instance Root_of_Expr      (Expr_Lambda_Inline lam root)      = root
type instance Type_of_Expr      (Expr_Lambda_Inline lam root)      = No_Type
type instance Sym_of_Expr       (Expr_Lambda_Inline lam root) repr = Sym_Lambda_Inline lam repr
type instance Error_of_Expr ast (Expr_Lambda_Inline lam root)      = No_Error_Expr

-- * Type 'Expr_Lambda_Val'
-- | Expression.
data Expr_Lambda_Val (lam:: * -> *) (root:: *)
type instance Root_of_Expr      (Expr_Lambda_Val lam root)      = root
type instance Type_of_Expr      (Expr_Lambda_Val lam root)      = No_Type
type instance Sym_of_Expr       (Expr_Lambda_Val lam root) repr = Sym_Lambda_Val lam repr
type instance Error_of_Expr ast (Expr_Lambda_Val lam root)      = No_Error_Expr

-- * Type 'Expr_Lambda_Lazy'
-- | Expression.
data Expr_Lambda_Lazy (lam:: * -> *) (root:: *)
type instance Root_of_Expr      (Expr_Lambda_Lazy lam root)      = root
type instance Type_of_Expr      (Expr_Lambda_Lazy lam root)      = No_Type
type instance Sym_of_Expr       (Expr_Lambda_Lazy lam root) repr = Sym_Lambda_Lazy lam repr
type instance Error_of_Expr ast (Expr_Lambda_Lazy lam root)      = No_Error_Expr

-- | Parsing utility to check that the given type is a 'Type_Fun'
-- or raise 'Error_Expr_Type_mismatch'.
check_type_fun
 :: forall ast ex root lam ty h ret.
 ( root ~ Root_of_Expr ex
 , ty ~ Type_Root_of_Expr ex
 , Lift_Type   (Type_Fun lam) (Type_of_Expr root)
 , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 )
 => Proxy ex -> ast -> ty h
 -> (Type_Fun lam ty h -> Either (Error_of_Expr ast root) ret)
 -> Either (Error_of_Expr ast root) ret
check_type_fun ex ast ty k =
	case unlift_type $ unType_Root ty of
	 Just ty_f -> k ty_f
	 Nothing -> Left $
		error_expr ex $
		Error_Expr_Type_mismatch ast
		 (Exists_Type (type_var0 SZero `type_fun` type_var0 (SSucc SZero)
		 :: Type_Root_of_Expr ex (Lambda lam Var0 Var0)))
		 (Exists_Type ty)

-- | Parse a /lambda variable/.
var_from
 :: forall ast lam root hs ret.
 ( Type_from ast (Type_Root_of_Expr root)
 , Lift_Error_Expr (Error_Expr_Lambda ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => Text -> Expr_From ast (Expr_Lambda_App lam root) hs ret
var_from name _ex ast = go
	where
	go :: forall ex hs'. (ex ~ (Expr_Lambda_App lam root))
	 => Context (Lambda_Var (Type_Root_of_Expr ex)) hs'
	 -> ( forall h. Type_Root_of_Expr ex h
	    -> Forall_Repr_with_Context ex hs' h
	    -> Either (Error_of_Expr ast (Root_of_Expr ex)) ret )
	 ->    Either (Error_of_Expr ast (Root_of_Expr ex)) ret
	go c k' =
		case c of
		 Context_Empty -> Left $ lift_error_expr $
			Error_Expr_Lambda_Var_unbound name ast
		 Lambda_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'

-- | Parse 'app'.
app_from
 :: forall ty ast lam root hs ret.
 ( ty ~ Type_Root_of_Expr root
 , Type_from ast ty
 , Eq_Type ty
 , Expr_from ast root
 , Lift_Type_Root (Type_Fun lam) ty
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
 , Root_of_Expr root ~ root
 ) => ast -> ast
 -> Expr_From ast (Expr_Lambda_App lam root) hs ret
app_from ast_lam ast_arg_actual ex ast ctx k =
	expr_from (Proxy::Proxy root) ast_lam ctx $
	 \(ty_lam::Type_Root_of_Expr root h_lam) (Forall_Repr_with_Context lam) ->
	expr_from (Proxy::Proxy root) ast_arg_actual ctx $
	 \(ty_arg_actual::Type_Root_of_Expr root h_arg_actual)
	  (Forall_Repr_with_Context arg_actual) ->
		case unlift_type $ unType_Root ty_lam of
		 Nothing -> Left $
			error_expr ex $
			Error_Expr_Type_mismatch ast
			 (Exists_Type (type_var0 SZero `type_fun` type_var0 (SSucc SZero)
			 :: Type_Root_of_Expr (Expr_Lambda_App lam root) (Lambda lam Var0 Var0)))
			 (Exists_Type ty_lam)
		 Just (Type_Type2 Proxy ty_arg_expected ty_res
		  :: Type_Fun lam (Type_Root_of_Expr root) h_lam) ->
			check_eq_type ex ast
			 ty_arg_expected ty_arg_actual $ \Refl ->
				k ty_res $ Forall_Repr_with_Context $
				 \c -> lam c `app` arg_actual c

-- | Parse given /lambda abstraction/.
lam_from
 :: forall ty ast (lam:: * -> *) root hs ret ex.
 ( ty ~ Type_Root_of_Expr root
 , root ~ Root_of_Expr ex
 , root ~ Root_of_Expr root
 , Type_from ast ty
 , Expr_from ast root
 , Lift_Type_Root (Type_Fun lam) ty
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 ) => Proxy lam
 -> (forall repr arg res
      . Sym_of_Expr ex repr
      => (repr arg -> repr res)
      -> repr (Lambda lam arg res))
 -> Text -> ast -> ast
 -> Expr_From ast ex hs ret
lam_from _ lam name ast_ty_arg ast_body ex ast ctx k =
	case type_from
	 (Proxy::Proxy (Type_Root_of_Expr root))
	 ast_ty_arg (Right . Exists_Type) of
	 Left err -> Left $ error_expr ex $ Error_Expr_Type err ast
	 Right (Exists_Type (ty_arg::Type_Root_of_Expr root h_arg)) ->
		expr_from (Proxy::Proxy root) ast_body
		 (Lambda_Var name ty_arg `Context_Next` ctx) $
		 \(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)

-- | Parse given /let/.
let_from
 :: forall ty ast root hs ret ex.
 ( ty ~ Type_Root_of_Expr root
 , root ~ Root_of_Expr ex
 , root ~ Root_of_Expr root
 , Type_from ast ty
 , Expr_from ast root
 -- , Lift_Type_Root (Type_Fun lam) ty
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 ) => (forall repr var res. Sym_of_Expr ex repr
      => repr var -> (repr var -> repr res) -> repr res)
 -> Text -> ast -> ast
 -> Expr_From ast ex hs ret
let_from let_ name ast_var ast_body _ex _ast ctx k =
	expr_from (Proxy::Proxy root) ast_var ctx $
	 \(ty_var::Type_Root_of_Expr root h_var) (Forall_Repr_with_Context var) ->
		expr_from (Proxy::Proxy root) ast_body
		 (Lambda_Var name ty_var `Context_Next` ctx) $
		 \(ty_res::Type_Root_of_Expr root h_res) (Forall_Repr_with_Context res) ->
			k ty_res $ Forall_Repr_with_Context $
			 \c -> let_ (var c) $
				 \arg -> res (arg `Context_Next` c)

-- * Type 'Error_Expr_Lambda'
data Error_Expr_Lambda ast
 =   Error_Expr_Lambda_Var_unbound Lambda_Var_Name ast
 deriving (Eq, Show)