{-# LANGUAGE GADTs #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Language.Symantic.Compiling.Term where

import qualified Data.Function as Fun
import qualified Data.Kind as Kind
import Data.Monoid ((<>))
import Data.Proxy (Proxy(..))
import Data.Text (Text)
import qualified Data.Text as Text
import Data.Type.Equality ((:~:)(..))
import GHC.Exts (Constraint)
import Prelude hiding (not)

import Language.Symantic.Lib.Data.Type.List
import Language.Symantic.Parsing
import Language.Symantic.Typing
import Language.Symantic.Interpreting
import Language.Symantic.Transforming.Trans

-- * Type 'Term'
-- | 'TermLC' applied on a 'LamCtx_Type'.
data Term is h
 =   Term
 (forall term. ( Sym_of_Ifaces is term
               , Sym_Lambda term
               ) => term h)

-- ** Type 'TermLC'
-- | A data type embedding a universal quantification
-- over an interpreter @term@
-- and qualified by the symantics of a term.
--
-- Moreover the term is abstracted by a 'LamCtx_Term'
-- built top-down at parsing time
-- to build a /Higher-Order Abstract Syntax/ (HOAS)
-- for /lambda abstractions/ ('lam').
--
-- This data type is used to keep a parsed term polymorphic enough
-- to stay interpretable by different interpreters.
--
-- * @(@'Sym_of_Ifaces'@ is term)@
-- is needed when a symantic method includes a polymorphic type
-- and thus calls: 'term_from'.
--
-- * @(@'Sym_of_Ifaces'@ ls term)@ and @(@'Sym_of_Ifaces'@ rs term)@
-- are needed to be able to write the instance:
-- @(@'Term_fromR'@ is ls (i ': rs) ast)@.
--
-- * @(@'Sym_Lambda'@ term)@
-- is needed to be able to parse partially applied functions
-- (when their type is knowable).
data TermLC ctx h is ls rs
 =   TermLC
 (forall term. ( Sym_of_Ifaces is term
               , Sym_of_Ifaces ls term
               , Sym_of_Ifaces rs term
               , Sym_Lambda term
               ) => LamCtx_Term term ctx -> term h)

-- * Type 'ETerm'
-- | Existential 'Term', with its 'Type'.
data ETerm is
 = forall (h::Kind.Type). ETerm
   (Type (Consts_of_Ifaces is) h)
   (Term is h)

-- | Like 'term_from' but for a term with an empty /lambda context/.
closed_term_from
 :: Term_from is
 => EToken meta is
 -> Either (Error_Term meta is) (ETerm is)
closed_term_from tok =
	term_from tok LamCtx_TypeZ $ \typ (TermLC te) ->
	Right $ ETerm typ $ Term $ te LamCtx_TermZ

-- * Type 'Term_from'
-- | Convenient type synonym wrapping 'Term_fromR' to initiate its recursion.
class Term_from is where
	term_from :: EToken meta is -> Term_fromT meta ctx ret is '[] is
instance Term_fromR is '[] is => Term_from is where
	term_from (EToken tok) = term_fromR tok

-- ** Type 'Term_fromT'
-- | Convenient type synonym defining a term parser.
type Term_fromT meta ctx ret is ls rs
 = LamCtx_Type is Name_LamVar ctx
 -- ^ The bound variables in scope and their types:
 -- built top-down in the heterogeneous list @ctx@,
 -- from the closest including /lambda abstraction/ to the farest.
 -> ( forall h.
       Type (Consts_of_Ifaces is) (h::Kind.Type)
    -> TermLC ctx h is ls rs
    -> Either (Error_Term meta is) ret )
 -- ^ The accumulating continuation called bottom-up.
 -> Either (Error_Term meta is) ret

-- ** Class 'Term_fromR'
-- | Intermediate type class to construct an instance of 'Term_from'
-- from many instances of 'Term_fromI', one for each item of @is@.
--
-- * @is@: starting  list of /term constants/.
-- * @ls@: done      list of /term constants/.
-- * @rs@: remaining list of /term constants/.
class Term_fromR (is::[*]) (ls::[*]) (rs::[*]) where
	term_fromR :: TokenR meta is rs i -> Term_fromT meta ctx ret is ls rs
	{-
	term_fromR _tok _ctx _k = Left $ Error_Term_unbound
	default term_fromR :: AST ast => Term_fromT meta ctx ret is ls rs
	term_fromR ast _ctx _k =
		Left $ Error_Term_unbound $
		At (Just ast) $ ast_lexem ast
	-}

-- | Test whether @i@ handles the work of 'Term_from' or not,
-- or recurse on @rs@, preserving the starting list of /term constants/,
-- and keeping a list of those done to construct 'TermLC'.
instance
 ( Term_fromI is i
 , Term_fromR is (i ': ls) (r ': rs)
 ) => Term_fromR is ls (i ': r ': rs) where
	term_fromR tok ctx k =
		case tok of
		 TokenZ _m t -> term_fromI t ctx k
		 TokenS t ->
			term_fromR t ctx $ \typ (TermLC te :: TermLC ctx h is (i ': ls) (r ': rs)) ->
				k typ (TermLC te :: TermLC ctx h is ls (i ': r ': rs))
-- | End the recursion.
instance
 Term_fromI is i =>
 Term_fromR is ls (i ': '[]) where
	term_fromR (TokenZ _m t) ctx k = term_fromI t ctx k
	term_fromR TokenS{} _ctx _k = error "Oops, the impossible happened..."

-- ** Class 'Term_fromI'
-- | Handle the work of 'Term_from' for a given /interface/ @i@,
-- that is: maybe it handles the given /interface/,
-- and if so, maybe the term type-checks.
class Term_fromI (is::[*]) (i:: *) where
	term_fromI :: TokenT meta is i -> Term_fromT meta ctx ret is ls (i ': rs)

-- * Type family 'Sym_of_Ifaces'
type family Sym_of_Ifaces (is::[*]) (term:: * -> *) :: Constraint where
	Sym_of_Ifaces '[] term = ()
	Sym_of_Ifaces (i ': is) term = (Sym_of_Iface i term, Sym_of_Ifaces is term)

-- ** Type family 'Sym_of_Iface'
type family Sym_of_Iface (i:: *) :: {-term-}(* -> *) -> Constraint

-- * Type 'Consts_of_Ifaces'
type Consts_of_Ifaces is = Nub (Consts_of_IfaceR is)

-- ** Type family 'Consts_of_IfaceR'
type family Consts_of_IfaceR (is::[*]) where
	Consts_of_IfaceR '[] = '[]
	Consts_of_IfaceR (i ': is) = Consts_of_Iface i ++ Consts_of_IfaceR is

-- ** Type family 'Consts_of_Iface'
type family   Consts_of_Iface (i::k) :: [*]
type instance Consts_of_Iface (Proxy Enum) = Proxy Enum ': Consts_imported_by Enum

-- * Type 'LamCtx_Type'
-- | GADT for a typing context,
-- accumulating an @item@ at each lambda;
-- used to accumulate object-types (in 'Expr_From')
-- or host-terms (in 'HostI')
-- associated with the 'LamVar's in scope.
data LamCtx_Type (is::[*]) (name:: *) (ctx::[*]) where
	LamCtx_TypeZ :: LamCtx_Type is name '[]
	LamCtx_TypeS :: name
	             -> Type (Consts_of_Ifaces is) (h::Kind.Type)
	             -> LamCtx_Type is name hs
	             -> LamCtx_Type is name (h ': hs)
infixr 5 `LamCtx_TypeS`

-- ** Type 'Name_LamVar'
type Name_LamVar = Text

-- * Type 'LamCtx_Term'
data LamCtx_Term (term:: * -> *) (ctx::[*]) where
	LamCtx_TermZ :: LamCtx_Term term '[]
	LamCtx_TermS :: term h
	             -> LamCtx_Term term hs
	             -> LamCtx_Term term (h ': hs)
infixr 5 `LamCtx_TermS`

{-
data Constraint_Type meta ts
 =   Constraint_Type_Eq (Constraint_Kind meta ts)
 -}

-- * Type 'Error_Term'
data Error_Term meta (is::[*])
 =   Error_Term_unbound Name_LamVar
 |   Error_Term_Typing (Error_Type meta '[Proxy Token_Type])
 |   Error_Term_Constraint_Type
     (Either
       (Constraint_Type meta '[Proxy Token_Type] (Consts_of_Ifaces is))
       (Constraint_Type meta is (Consts_of_Ifaces is)))
 |   Error_Term_Constraint_Kind (Constraint_Kind meta is)
deriving instance (Eq meta, Eq_Token meta is) => Eq (Error_Term meta is)
deriving instance (Show meta, Show_Token meta is, Show_Const (Consts_of_Ifaces is)) => Show (Error_Term meta is)

-- * Type 'Constraint_Type'
data Constraint_Type meta ts cs
 =   Constraint_Type_Eq  (Either (At meta '[Proxy Token_Type] (EType cs))
                                 (At meta ts (EType cs)))
                         (At meta ts (EType cs))
 |   Constraint_Type_App (At meta ts (EType cs))
 |   Constraint_Type_Con (At meta ts (KType cs Constraint))
 |   Constraint_Type_Fam (At meta ts Name_Fam) [EType cs]
deriving instance
 ( Eq meta
 , Eq_Token meta ts
 ) => Eq (Constraint_Type meta ts cs)
deriving instance
 ( Show meta
 , Show_Token meta ts
 , Show_Const cs
 ) => Show (Constraint_Type meta ts cs)


instance MonoLift (Error_Type meta '[Proxy Token_Type]) (Error_Term meta ts) where
	olift = Error_Term_Typing . olift
instance MonoLift (Error_Term meta ts) (Error_Term meta ts) where
	olift = Prelude.id
instance
 cs ~ Consts_of_Ifaces is =>
 MonoLift (Constraint_Type meta is cs) (Error_Term meta is) where
	olift = Error_Term_Constraint_Type . Right
instance
 cs ~ Consts_of_Ifaces is =>
 MonoLift (Constraint_Type meta '[Proxy Token_Type] cs) (Error_Term meta is) where
	olift = Error_Term_Constraint_Type . Left
instance MonoLift (Constraint_Kind meta '[Proxy Token_Type]) (Error_Term meta is) where
	olift = Error_Term_Typing . Error_Type_Constraint_Kind
instance MonoLift (Constraint_Kind meta is) (Error_Term meta is) where
	olift = Error_Term_Constraint_Kind

-- ** Checks
check_type
 :: MonoLift (Constraint_Type meta ts cs) err
 => At meta ts (Type cs x)
 -> At meta ts (Type cs y)
 -> ((x :~: y) -> Either err ret) -> Either err ret
check_type x y k =
	case unAt x `eq_type` unAt y of
	 Just Refl -> k Refl
	 Nothing -> Left $ olift $
		Constraint_Type_Eq (Right $ EType <$> x) (EType <$> y)

check_type_is
 :: MonoLift (Constraint_Type meta ts cs) err
 => At meta '[Proxy Token_Type] (Type cs x)
 -> At meta ts (Type cs y)
 -> ((x :~: y) -> Either err ret) -> Either err ret
check_type_is x y k =
	case unAt x `eq_type` unAt y of
	 Just Refl -> k Refl
	 Nothing -> Left $ olift $
		Constraint_Type_Eq (Left $ EType <$> x) (EType <$> y)

check_type_app
 :: MonoLift (Constraint_Type meta ts cs) err
 => At meta ts (Type cs (fa::kfa))
 -> (forall ka f a. (fa :~: f a)
  -> Type cs (f::ka -> kfa)
  -> Type cs (a::ka)
  -> Either err ret)
 -> Either err ret
check_type_app typ k =
	case unAt typ of
	 a :$ b -> k Refl a b
	 _ -> Left $ olift $
		Constraint_Type_App (EType <$> typ)

check_con
 :: ( Proj_Con cs
    , MonoLift (Constraint_Type meta ts cs) err )
 => At meta ts (Type cs (q::Constraint))
 -> (Con q -> Either err ret)
 -> Either err ret
check_con typ k =
	case proj_con $ unAt typ of
	 Just Con -> k Con
	 Nothing -> Left $ olift $
		Constraint_Type_Con (KType <$> typ)

check_con1
 :: ( Proj_Con cs
    , MonoLift (Constraint_Type meta ts cs) err
    , MonoLift (Constraint_Kind meta ts) err )
 => Type cs con
 -> At meta ts (Type cs (fa:: *))
 -> (forall f a. (fa :~: f a)
  -> Con (con f)
  -> Type cs (f:: * -> *)
  -> Type cs (a:: *)
  -> Either err ret)
 -> Either err ret
check_con1 con ty_fa k =
	check_type_app ty_fa $ \Refl ty_f ty_a ->
	check_kind
	 (At Nothing (SKiType `SKiArrow` SKiType))
	 (kind_of ty_f <$ ty_fa) $ \Refl ->
	check_con ((con :$ ty_f) <$ ty_fa) $ \Con ->
	k Refl Con ty_f ty_a

check_type1
 :: ( MonoLift (Constraint_Type meta ts cs) err
    , MonoLift (Constraint_Kind meta ts) err )
 => Type cs (f:: * -> *)
 -> At meta ts (Type cs fa)
 -> (forall a. (fa :~: f a)
  -> Type cs a
  -> Either err ret)
 -> Either err ret
check_type1 typ ty_fa k =
	check_type_app ty_fa $ \Refl ty_f ty_a ->
	check_kind
	 (At Nothing $ SKiType `SKiArrow` SKiType)
	 (kind_of ty_f <$ ty_fa) $ \Refl ->
	check_type
	 (At Nothing typ)
	 (ty_f <$ ty_fa) $ \Refl ->
	k Refl ty_a

check_type2
 :: ( MonoLift (Constraint_Type meta ts cs) err
    , MonoLift (Constraint_Kind meta ts) err )
 => Type cs (f:: * -> * -> *)
 -> At meta ts (Type cs fab)
 -> (forall a b. (fab :~: f a b)
  -> Type cs a
  -> Type cs b
  -> Either err ret)
 -> Either err ret
check_type2 typ ty_fab k =
	check_type_app ty_fab            $ \Refl ty_fa ty_b ->
	check_type_app (ty_fa <$ ty_fab) $ \Refl ty_f  ty_a ->
	check_kind
	 (At Nothing $ SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
	 (kind_of ty_f <$ ty_fab) $ \Refl ->
	check_type
	 (At Nothing typ)
	 (ty_f <$ ty_fab) $ \Refl ->
	k Refl ty_a ty_b

check_fam
 :: ( MonoLift (Constraint_Type meta ts cs) err
    , Proj_Fam cs fam
    , Show fam )
 => At meta ts fam
 -> Types cs hs
 -> (Type cs (Fam fam hs) -> Either err ret)
 -> Either err ret
check_fam fam tys k =
	case proj_fam (unAt fam) tys of
	 Just t -> k t
	 Nothing -> Left $ olift $
		Constraint_Type_Fam
		 (Text.pack . show <$> fam)
		 (etypes tys)

-- * Class 'Sym_Lambda'
class Sym_Lambda term where
	-- | /Lambda abstraction/.
	lam :: (term arg -> term res) -> term ((->) arg res)
	default lam :: Trans t term
	 => (t term arg -> t term res)
	 -> t term ((->) arg res)
	lam f = trans_lift $ lam $ trans_apply . f . trans_lift
	
	-- | /Lambda application/.
	(.$) :: term ((->) arg res) -> term arg -> term res
	default (.$) :: Trans t term
	 => t term ((->) arg res) -> t term arg -> t term res
	(.$) f x = trans_lift (trans_apply f .$ trans_apply x)
	
	-- | Convenient 'lam' and '.$' wrapper.
	let_ :: term var -> (term var -> term res) -> term res
	let_ x y = lam y .$ x
	
	id :: term a -> term a
	id a = lam Fun.id .$ a
	
	const :: term a -> term b -> term a
	const a b = lam (lam . Fun.const) .$ a .$ b
	
	-- | /Lambda composition/.
	(#) :: term (b -> c) -> term (a -> b) -> term (a -> c)
	(#) f g = lam $ \a -> f .$ (g .$ a)
	
	flip :: term (a -> b -> c) -> term (b -> a -> c)
	flip f = lam $ \b -> lam $ \a -> f .$ a .$ b

infixl 0 .$
infixr 9 #

type instance Sym_of_Iface (Proxy (->)) = Sym_Lambda
type instance Consts_of_Iface (Proxy (->)) = Proxy (->) ': Consts_imported_by (->)
type instance Consts_imported_by (->) =
 [ Proxy Applicative
 , Proxy Functor
 , Proxy Monad
 , Proxy Monoid
 ]

instance Sym_Lambda HostI where
	lam f = HostI (unHostI . f . HostI)
	(.$)  = (<*>)
instance Sym_Lambda TextI where
	lam f = TextI $ \p v ->
		let p' = Precedence 1 in
		let x = "x" <> Text.pack (show v) in
		paren p p' $ "\\" <> x <> " -> "
		 <> unTextI (f (TextI $ \_p _v -> x)) p' (succ v)
	-- (.$) = textI_infix "$" (Precedence 0)
	(.$) (TextI a1) (TextI a2) =
		TextI $ \p v ->
			let p' = precedence_App in
			paren p p' $ a1 p' v <> " " <> a2 p' v
	let_ e in_ =
		TextI $ \p v ->
			let p' = Precedence 2 in
			let x = "x" <> Text.pack (show v) in
			paren p p' $ "let" <> " " <> x <> " = "
			 <> unTextI e (Precedence 0) (succ v) <> " in "
			 <> unTextI (in_ (TextI $ \_p _v -> x)) p' (succ v)
	(#)   = textI_infix "." (Precedence 9)
	id    = textI_app1 "id"
	const = textI_app2 "const"
	flip  = textI_app1 "flip"
instance (Sym_Lambda r1, Sym_Lambda r2) => Sym_Lambda (DupI r1 r2) where
	lam f = dupI_1 lam_f `DupI` dupI_2 lam_f
		where lam_f = lam f
	(.$) = dupI2 (Proxy::Proxy Sym_Lambda) (.$)

instance Const_from Text cs => Const_from Text (Proxy (->) ': cs) where
	const_from "(->)" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Show_Const cs => Show_Const (Proxy (->) ': cs) where
	show_const ConstZ{} = "(->)"
	show_const (ConstS c) = show_const c

instance -- Proj_ConC (->)
 ( Proj_Const cs (->)
 , Proj_Consts cs (Consts_imported_by (->))
 , Proj_Con cs
 ) => Proj_ConC cs (Proxy (->)) where
	proj_conC _ (TyConst q :$ (TyConst c :$ _r))
	 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_const c (Proxy::Proxy (->))
	 = case () of
		 _ | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Con
		 _ -> Nothing
	proj_conC _ (t@(TyConst q) :$ (TyConst c :$ _a :$ b))
	 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_const c (Proxy::Proxy (->))
	 = case () of
		 _ | Just Refl <- proj_const q (Proxy::Proxy Monoid)
		   , Just Con  <- proj_con (t :$ b) -> Just Con
		 _ -> Nothing
	proj_conC _c _q = Nothing
data instance TokenT meta (ts::[*]) (Proxy (->))
 = Token_Term_Abst Name_LamVar (EToken meta '[Proxy Token_Type]) (EToken meta ts)
 | Token_Term_App              (EToken meta ts) (EToken meta ts)
 | Token_Term_Let  Name_LamVar (EToken meta ts) (EToken meta ts)
 | Token_Term_Var  Name_LamVar
deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy (->)))
deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy (->)))
instance -- Term_fromI (->)
 ( Inj_Const  (Consts_of_Ifaces is) (->)
 , Const_from Name_LamVar (Consts_of_Ifaces is)
 , Term_from is
 ) => Term_fromI is (Proxy (->)) where
	term_fromI tok ctx k =
		case tok of
		 Token_Term_Abst name_arg tok_ty_arg tok_body ->
			type_from tok_ty_arg $ \(ty_arg::Type (Consts_of_Ifaces is) h) ->
			check_kind
			 (At Nothing SKiType)
			 (At (Just $ tok_ty_arg) $ kind_of ty_arg) $ \Refl ->
			term_from tok_body
			 (LamCtx_TypeS name_arg ty_arg ctx) $
			 \ty_res (TermLC res) ->
			k (ty_arg ~> ty_res) $ TermLC $
			 \c -> lam $ \arg ->
				res (arg `LamCtx_TermS` c)
		 Token_Term_App tok_lam tok_arg_actual ->
			term_from tok_lam ctx $ \ty_lam (TermLC lam_) ->
			term_from tok_arg_actual ctx $ \ty_arg_actual (TermLC arg_actual) ->
			check_type2 (ty @(->)) (At (Just tok_lam) ty_lam) $ \Refl ty_arg ty_res ->
			check_type
			 (At (Just tok_lam) ty_arg)
			 (At (Just tok_arg_actual) ty_arg_actual) $ \Refl ->
			k ty_res $ TermLC $
			 \c -> lam_ c .$ arg_actual c
		 Token_Term_Let name tok_bound tok_body ->
			term_from tok_bound ctx $ \ty_bound (TermLC bound) ->
			term_from tok_body (LamCtx_TypeS name ty_bound ctx) $
			 \ty_res (TermLC res) ->
			k ty_res $ TermLC $
			 \c -> let_ (bound c) $ \arg -> res (arg `LamCtx_TermS` c)
		 Token_Term_Var nam -> go nam ctx k
			where
			go :: forall meta lc ret ls rs.
			    Name_LamVar
			 -> LamCtx_Type is Name_LamVar lc
			 -> ( forall h.
			       Type (Consts_of_Ifaces is) (h::Kind.Type)
			    -> TermLC lc h is ls rs
			    -> Either (Error_Term meta is) ret )
			 -> Either (Error_Term meta is) ret
			go name lc k' =
				case lc of
				 LamCtx_TypeZ -> Left $ Error_Term_unbound name
				 LamCtx_TypeS n typ _ | n == name ->
					k' typ $ TermLC $ \(te `LamCtx_TermS` _) -> te
				 LamCtx_TypeS _n _ty lc' ->
					go name lc' $ \typ (TermLC te::TermLC lc' h is '[] is) ->
					k' typ $ TermLC $ \(_ `LamCtx_TermS` c) -> te c

-- | The function 'Type' @(->)@,
-- with an infix notation more readable.
(~>) :: forall cs a b. Inj_Const cs (->)
 => Type cs a -> Type cs b -> Type cs (a -> b)
(~>) a b = ty @(->) :$ a :$ b
infixr 5 ~>

{-
-- * Class 'Sym_Type'
class Sym_Type term
instance Sym_Type term
type instance Sym_of_Iface (Proxy Token_Type) = Sym_Type
type instance Consts_of_Iface (Proxy Token_Type) = '[]
type instance Consts_imported_by Token_Type = '[]
instance -- Proj_ConC
 Proj_ConC cs (Proxy Token_Type)
instance -- Term_fromI (->)
 Term_fromI is (Proxy Token_Type) where
	term_fromI _tok _ctx _k = Left $ Error_Term_unbound
-}