{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
-- {-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module TFHOE.Expr.Fun where

import Data.Either (Either(..))
import Data.Eq (Eq(..))
import Data.Function (($))
-- import Data.Functor.Identity (Identity)
import Data.Maybe (Maybe(..))
-- import Data.Monoid ((<>))
import Data.Proxy (Proxy(..))
-- import Data.Proxy (Proxy(..))
-- import Data.String (String)
import Data.Type.Equality ((:~:)(Refl))
-- import Data.Type.Equality ((:~:)(Refl))
-- import Text.Show (Show(..))

import TFHOE.Raw
import TFHOE.Type
import TFHOE.Expr.Common
import TFHOE.Repr.Dup

-- * Class 'Expr_Fun'

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

infixl 5 `app`

type instance Expr_from_Type (Type_Fun fun next) repr
 = ( Expr_Fun fun repr
   , Expr_from_Type next repr )

instance -- Expr_Fun Dup
 ( Expr_Fun fun r1
 , Expr_Fun fun r2
 ) => Expr_Fun fun (Dup r1 r2) where
	type Fun_from_Repr (Dup r1 r2) = Fun_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)
instance -- Expr_from Raw Type_Fun Type_Fun
 ( Type_from Raw next
 , Expr_from Raw next (Type_Fun fun next)
 ) => Expr_from Raw (Type_Fun fun next) (Type_Fun fun next) where
	expr_from _px_ty _px_ty_end ctx (Raw "var" [Raw name []]) k =
		go ctx k
		where
		go :: forall hs ret.
		 Context (Var (Type_Fun fun next)) hs
		 -> (forall h. Type_Fun fun next h
		  -> Forall_Repr_with_Context (Type_Fun fun next) hs h
		  -> Either Error_Type ret)
		 -> Either Error_Type ret
		go c k' =
			case c of
			 Context_Empty -> Left "Error: var: unbound variable"
			 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'
	expr_from _px_ty px_ty_end ctx (Raw "app" [raw_lam, raw_val]) k =
		expr_from px_ty_end px_ty_end ctx raw_lam $ \ty_lam (Forall_Repr_with_Context lam) ->
		expr_from px_ty_end px_ty_end ctx raw_val $ \ty_val (Forall_Repr_with_Context val_) ->
			case ty_lam of
			 ty_arg `Type_Fun` ty_res
			  | Just Refl <- ty_arg `type_eq` ty_val ->
				k ty_res $ Forall_Repr_with_Context $
				 \c -> lam c `app` val_ c
			 _ -> Left "Error: app: bad lambda application"
	expr_from _px_ty px_ty_end ctx (Raw "inline" [Raw name [], raw_ty_arg, raw_body]) k =
		type_from raw_ty_arg $ \ty_arg ->
			expr_from px_ty_end px_ty_end (Var name ty_arg `Context_Next` ctx) raw_body $
			 \ty_res (Forall_Repr_with_Context res) ->
				k (ty_arg `Type_Fun` ty_res) $ Forall_Repr_with_Context $
				 \c -> inline $ \arg -> res (arg `Context_Next` c)
	expr_from _px_ty px_ty_end ctx (Raw "val" [Raw name [], raw_ty_arg, raw_body]) k =
		type_from raw_ty_arg $ \ty_arg ->
			expr_from px_ty_end px_ty_end (Var name ty_arg `Context_Next` ctx) raw_body $
			 \ty_res (Forall_Repr_with_Context res) ->
				k (ty_arg `Type_Fun` ty_res) $ Forall_Repr_with_Context $
				 \c -> val $ \arg -> res (arg `Context_Next` c)
	expr_from _px_ty px_ty_end ctx (Raw "lazy" [Raw name [], raw_ty_arg, raw_body]) k =
		type_from raw_ty_arg $ \ty_arg ->
			expr_from px_ty_end px_ty_end (Var name ty_arg `Context_Next` ctx) raw_body $
			 \ty_res (Forall_Repr_with_Context res) ->
				k (ty_arg `Type_Fun` ty_res) $ Forall_Repr_with_Context $
				 \c -> lazy $ \arg -> res (arg `Context_Next` c)
	expr_from _px_ty px_ty_end ctx raw k =
		expr_from (Proxy::Proxy next) px_ty_end ctx raw k