{-# 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 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 type 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 /lambda term context/
-- 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
               ) => TeCtx term ctx -> term h)

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

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

-- | Like 'compileO' but for a term with an empty /lambda context/.
compile
 :: Compile cs is
 => EToken meta is
 -> Either (Error_Term meta cs is) (ETerm cs is)
compile tok = closeContext (compileO tok)

-- ** Type 'CompileO'

-- | Wrap 'CompileT' to keep the /lambda context/ fully polymorphic,
-- this is useful in 'withContext' to help GHC's type solver, which
-- "Cannot instantiate unification variable with a type involving foralls".
data CompileO meta ret cs is ls rs
 =   CompileO
 { unCompileO :: forall ctx. CompileT meta ctx ret cs is ls rs }

-- | Compile with given /lambda context/.
withContext
 :: Foldable f
 => f (TeName, ETerm cs is)
 -> (forall hs. CompileT meta hs ret cs is ls rs)
 -> CompileT meta ctx ret cs is ls rs
withContext env comp = unCompileO $
	foldr
	 (\e (CompileO c) -> CompileO $ pushContext e c)
	 (CompileO comp) env

-- | Compile with a /lambda context/ augmented by given 'ETerm'.
pushContext
 :: (TeName, ETerm cs is)
 -> (forall hs. CompileT meta hs ret cs is ls rs)
 -> CompileT meta ctx ret cs is ls rs
pushContext (n, ETerm ty_n (Term te_n)) co ctx k =
	co (TyCtxS n ty_n ctx) $ \ty_y (TermO y) ->
	k ty_y $ TermO $
	 \c -> y (te_n `TeCtxS` c)

-- | Compile with the empty /lambda context/.
closeContext
 :: (forall hs. CompileT meta hs (ETerm cs is) cs is '[] is)
 -> Either (Error_Term meta cs is) (ETerm cs is)
closeContext co =
	co TyCtxZ $ \typ (TermO te) ->
	Right $ ETerm typ $ Term $ te TeCtxZ

-- ** Type 'CompileT'
-- | Convenient type synonym defining a term parser.
type CompileT meta ctx ret cs is ls rs
 = TyCtx TeName cs 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 cs (h:: *)
    -> TermO ctx h is ls rs
    -> Either (Error_Term meta cs is) ret )
 -- ^ The accumulating continuation, called bottom-up.
 -> Either (Error_Term meta cs 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 (cs::[*]) (is::[*]) (ls::[*]) (rs::[*]) where
	compileR :: TokenR meta is rs i -> CompileT meta ctx ret cs is ls rs

-- | Recurse into into the given 'TokenR'
-- to call the 'compileI' instance associated
-- to the 'TokenT' it contains.
instance
 ( CompileI cs is i
 , CompileR cs is (i ': ls) (r ': rs)
 ) => CompileR cs 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 cs is i =>
 CompileR cs 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 (cs::[*]) (is::[*]) (i:: *) where
	compileI :: TokenT meta is i -> CompileT meta ctx ret cs 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_IfacesR is)

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

{- NOTE: failed attempt to recursively collect TyConsts.
-- ** Type family 'TyConsts_imported_byR'
type family TyConsts_imported_byR (done::[*]) (cs::[*]) where
	TyConsts_imported_byR done '[] = done
	TyConsts_imported_byR done (c ': cs) =
		If (Exists c done)
		 (TyConsts_imported_byR done cs)
		 (TyConsts_imported_byR (c ': done) (TyConsts_imported_by c ++ TyConsts_imported_byR done cs))
-}

-- ** Type family 'TyConsts_of_Iface'
type family TyConsts_of_Iface (i:: *) :: [*]

-- ** Type family 'TyConsts_imported_by'
-- | Return the /type constant/s that a given /type constant/
-- wants to be part of the final list of /type constants/.
type family TyConsts_imported_by (c:: *) :: [*]

-- * Type 'TyCtx'
-- | GADT for a typing context:
-- accumulating at each /lambda abstraction/
-- the 'Type' of the introduced variable.
data TyCtx (name:: *) (cs::[*]) (hs::[*]) where
	TyCtxZ :: TyCtx name cs '[]
	TyCtxS :: name
	       -> Type cs h
	       -> TyCtx name cs hs
	       -> TyCtx name cs (h ': hs)
infixr 5 `TyCtxS`

-- * Type 'TeCtx'
-- | GADT for an evaluating context:
-- accumulating at each /lambda abstraction/
-- the @term@ of the introduced variable.
data TeCtx (term:: * -> *) (hs::[*]) where
	TeCtxZ :: TeCtx term '[]
	TeCtxS :: term h
	       -> TeCtx term hs
	       -> TeCtx term (h ': hs)
infixr 5 `TeCtxS`

-- * Type 'Error_Term'
data Error_Term meta (cs::[*]) (is::[*])
 =   Error_Term_unbound TeName
 |   Error_Term_Typing (Error_Type meta '[Proxy Token_Type])
 |   Error_Term_Con_Type
     (Either
       (Con_Type meta cs '[Proxy Token_Type])
       (Con_Type meta cs is))
 |   Error_Term_Con_Kind (Con_Kind meta is)
deriving instance (Eq meta, Eq_Token meta is) => Eq (Error_Term meta cs is)
deriving instance (Show meta, Show_Token meta is, Show_TyConst cs) => Show (Error_Term meta cs is)

-- * Type 'Con_Type'
data Con_Type meta cs ts
 =   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 cs ts)
deriving instance
 ( Show meta
 , Show_Token meta ts
 , Show_TyConst cs
 ) => Show (Con_Type meta cs ts)

instance MonoLift (Error_Type meta '[Proxy Token_Type]) (Error_Term meta cs ts) where
	olift = Error_Term_Typing . olift
instance MonoLift (Error_Term meta cs ts) (Error_Term meta cs ts) where
	olift = id
instance
 MonoLift (Con_Type meta cs is) (Error_Term meta cs is) where
	olift = Error_Term_Con_Type . Right
instance
 MonoLift (Con_Type meta cs '[Proxy Token_Type]) (Error_Term meta cs is) where
	olift = Error_Term_Con_Type . Left
instance MonoLift (Con_Kind meta '[Proxy Token_Type]) (Error_Term meta cs is) where
	olift = Error_Term_Typing . Error_Type_Con_Kind
instance MonoLift (Con_Kind meta is) (Error_Term meta cs is) where
	olift = Error_Term_Con_Kind

-- ** Checks
check_TyEq
 :: MonoLift (Con_Type meta cs ts) 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 cs ts) 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 cs ts) 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 cs ts) 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 cs ts) 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 cs ts) 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 cs ts) 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 cs ts) 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)