{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Language.Symantic.Compiling.Term
 ( module Language.Symantic.Compiling.Term
 , module Language.Symantic.Compiling.Term.Grammar
 ) where

import qualified Data.Kind as Kind
import Data.Proxy (Proxy(..))
import qualified Data.Text as Text
import Data.Type.Equality ((:~:)(..))
import GHC.Exts (Constraint)

import Language.Symantic.Helper.Data.Type.List
import Language.Symantic.Parsing
import Language.Symantic.Typing

import Language.Symantic.Compiling.Term.Grammar

-- * Type 'Term'
-- | Closed 'TermO'.
data Term is h
 =   Term
 (forall term. ( Sym_of_Ifaces is term
               , Sym_of_Iface (Proxy (->)) term
               ) => term h)

-- ** Type 'TermO'
-- | An open term (i.e. with a /lambda context/).
-- The data type wraps a universal quantification
-- over an interpreter @term@
-- qualified by the symantics of a term.
--
-- Moreover the term is abstracted by a 'LamCtx_Term'
-- built top-down by 'compileO',
-- to enable 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: 'compileO'.
--
-- * @(@'Sym_of_Ifaces'@ ls term)@ and @(@'Sym_of_Ifaces'@ rs term)@
-- make a zipper needed to be able to write the recursing 'CompileR' instance.
--
-- * @(@'Sym_of_Iface'@ (@'Proxy'@ (->)) term)@
-- is needed to handle partially applied functions.
data TermO ctx h is ls rs
 =   TermO
 (forall term. ( Sym_of_Ifaces is term
               , Sym_of_Ifaces ls term
               , Sym_of_Ifaces rs term
               , Sym_of_Iface (Proxy (->)) term
               ) => LamCtx_Term term ctx -> term h)

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

-- * Type 'Compile'
-- | Convenient type synonym wrapping 'CompileR' to initiate its recursion.
class Compile is where
	compileO :: EToken meta is -> CompileT meta ctx ret is '[] is
instance CompileR is '[] is => Compile is where
	compileO (EToken tok) = compileR tok

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

-- ** Type 'CompileT'
-- | Convenient type synonym defining a term parser.
type CompileT meta ctx ret is ls rs
 = LamCtx_Type is Term_Name 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 (TyConsts_of_Ifaces is) (h::Kind.Type)
    -> TermO ctx h is ls rs
    -> Either (Error_Term meta is) ret )
 -- ^ The accumulating continuation called bottom-up.
 -> Either (Error_Term meta is) ret

-- ** Class 'CompileR'
-- | Intermediate type class to construct an instance of 'Compile'
-- from many instances of 'CompileI', 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 CompileR (is::[*]) (ls::[*]) (rs::[*]) where
	compileR :: TokenR meta is rs i -> CompileT meta ctx ret is ls rs

-- | Recurse into into the given 'TokenR'
-- to call the 'compileI' instance associated
-- to the 'TokenT' it contains.
instance
 ( CompileI is i
 , CompileR is (i ': ls) (r ': rs)
 ) => CompileR is ls (i ': r ': rs) where
	compileR tok ctx k =
		case tok of
		 TokenZ _m t -> compileI t ctx k
		 TokenS t ->
			compileR t ctx $ \typ (TermO te :: TermO ctx h is (i ': ls) (r ': rs)) ->
				k typ (TermO te :: TermO ctx h is ls (i ': r ': rs))
-- | End the recursion.
instance
 CompileI is i =>
 CompileR is ls (i ': '[]) where
	compileR (TokenZ _m t) ctx k = compileI t ctx k
	compileR TokenS{} _ctx _k = error "Oops, the impossible happened..."

-- ** Class 'CompileI'
-- | Handle the work of 'Compile' for a given /interface/ @i@.
class CompileI (is::[*]) (i:: *) where
	compileI :: TokenT meta is i -> CompileT 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 'TyConsts_of_Ifaces'
type TyConsts_of_Ifaces is = Nub (TyConsts_of_IfaceR is)

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

-- ** Type family 'TyConsts_of_Iface'
type family   TyConsts_of_Iface (i:: *) :: [*]
type instance TyConsts_of_Iface (Proxy Enum) = Proxy Enum ': TyConsts_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 (TyConsts_of_Ifaces is) (h::Kind.Type)
	             -> LamCtx_Type is name hs
	             -> LamCtx_Type is name (h ': hs)
infixr 5 `LamCtx_TypeS`

-- * 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`

-- * Type 'Error_Term'
data Error_Term meta (is::[*])
 =   Error_Term_unbound Term_Name
 |   Error_Term_Typing (Error_Type meta '[Proxy Token_Type])
 |   Error_Term_Con_Type
     (Either
       (Con_Type meta '[Proxy Token_Type] (TyConsts_of_Ifaces is))
       (Con_Type meta is (TyConsts_of_Ifaces is)))
 |   Error_Term_Con_Kind (Con_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_TyConst (TyConsts_of_Ifaces is)) => Show (Error_Term meta is)

-- * Type 'Con_Type'
data Con_Type meta ts cs
 =   Con_TyEq  (Either (At meta '[Proxy Token_Type] (EType cs))
                              (At meta ts (EType cs)))
                      (At meta ts (EType cs))
 |   Con_TyApp (At meta ts (EType cs))
 |   Con_TyCon (At meta ts (KType cs Constraint))
 |   Con_TyFam (At meta ts TyFamName) [EType cs]
deriving instance
 ( Eq meta
 , Eq_Token meta ts
 ) => Eq (Con_Type meta ts cs)
deriving instance
 ( Show meta
 , Show_Token meta ts
 , Show_TyConst cs
 ) => Show (Con_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 ~ TyConsts_of_Ifaces is =>
 MonoLift (Con_Type meta is cs) (Error_Term meta is) where
	olift = Error_Term_Con_Type . Right
instance
 cs ~ TyConsts_of_Ifaces is =>
 MonoLift (Con_Type meta '[Proxy Token_Type] cs) (Error_Term meta is) where
	olift = Error_Term_Con_Type . Left
instance MonoLift (Con_Kind meta '[Proxy Token_Type]) (Error_Term meta is) where
	olift = Error_Term_Typing . Error_Type_Con_Kind
instance MonoLift (Con_Kind meta is) (Error_Term meta is) where
	olift = Error_Term_Con_Kind

-- ** Checks
check_TyEq
 :: MonoLift (Con_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_TyEq x y k =
	case unAt x `eq_Type` unAt y of
	 Just Refl -> k Refl
	 Nothing -> Left $ olift $
		Con_TyEq (Right $ EType <$> x) (EType <$> y)

check_Type_is
 :: MonoLift (Con_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 $
		Con_TyEq (Left $ EType <$> x) (EType <$> y)

check_TyApp
 :: MonoLift (Con_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_TyApp typ k =
	case unAt typ of
	 a :$ b -> k Refl a b
	 _ -> Left $ olift $
		Con_TyApp (EType <$> typ)

check_TyEq1
 :: ( MonoLift (Con_Type meta ts cs) err
    , MonoLift (Con_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_TyEq1 typ ty_fa k =
	check_TyApp ty_fa $ \Refl ty_f ty_a ->
	check_Kind
	 (At Nothing $ SKiType `SKiArrow` SKiType)
	 (kind_of ty_f <$ ty_fa) $ \Refl ->
	check_TyEq
	 (At Nothing typ)
	 (ty_f <$ ty_fa) $ \Refl ->
	k Refl ty_a

check_TyEq2
 :: ( MonoLift (Con_Type meta ts cs) err
    , MonoLift (Con_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_TyEq2 typ ty_fab k =
	check_TyApp ty_fab            $ \Refl ty_fa ty_b ->
	check_TyApp (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_TyEq
	 (At Nothing typ)
	 (ty_f <$ ty_fab) $ \Refl ->
	k Refl ty_a ty_b

check_TyCon
 :: ( Proj_TyCon cs
    , MonoLift (Con_Type meta ts cs) err )
 => At meta ts (Type cs (q::Constraint))
 -> (TyCon q -> Either err ret)
 -> Either err ret
check_TyCon typ k =
	case proj_TyCon $ unAt typ of
	 Just TyCon -> k TyCon
	 Nothing -> Left $ olift $
		Con_TyCon (KType <$> typ)

check_TyCon1
 :: ( Proj_TyCon cs
    , MonoLift (Con_Type meta ts cs) err
    , MonoLift (Con_Kind meta ts) err )
 => Type cs con
 -> At meta ts (Type cs (fa:: *))
 -> (forall f a. (fa :~: f a)
  -> TyCon (con f)
  -> Type cs (f:: * -> *)
  -> Type cs (a:: *)
  -> Either err ret)
 -> Either err ret
check_TyCon1 con ty_fa k =
	check_TyApp ty_fa $ \Refl ty_f ty_a ->
	check_Kind
	 (At Nothing (SKiType `SKiArrow` SKiType))
	 (kind_of ty_f <$ ty_fa) $ \Refl ->
	check_TyCon ((con :$ ty_f) <$ ty_fa) $ \TyCon ->
	k Refl TyCon ty_f ty_a

check_TyFam
 :: ( MonoLift (Con_Type meta ts cs) err
    , Proj_TyFam cs fam
    , Show fam )
 => At meta ts fam
 -> Types cs hs
 -> (Type cs (TyFam fam hs) -> Either err ret)
 -> Either err ret
check_TyFam fam tys k =
	case proj_TyFam (unAt fam) tys of
	 Just t -> k t
	 Nothing -> Left $ olift $
		Con_TyFam
		 (Text.pack . show <$> fam)
		 (eTypes tys)