{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UndecidableInstances #-}
module Language.Symantic.Compiling.Module where

import Data.Bool (not)
import Data.Map.Strict (Map)
import Data.Semigroup (Semigroup(..))
import Data.Set (Set)
import Data.String (IsString(..))
import Data.Text (Text)
import Prelude hiding (mod, not, any)
import qualified Data.Kind as K
import qualified Data.Map.Strict as Map

import Language.Symantic.Grammar
import Language.Symantic.Typing
import Language.Symantic.Compiling.Term

-- * Type 'Mod'
data Mod a = Mod PathMod a
 deriving (Eq, Functor, Ord, Show)

-- ** Type 'PathMod'
type PathMod = [NameMod]

-- ** Type 'NameMod'
newtype NameMod = NameMod Text
 deriving (Eq, Ord, Show)
instance IsString NameMod where
	fromString = NameMod . fromString

-- * Class 'ModuleFor'
class ModuleFor src ss s where
	moduleFor :: (PathMod, Module src ss)
	moduleFor = ([], moduleEmpty)

-- * Type 'Imports'
newtype Imports = Imports (Map PathMod (Map PathMod FilterImports))
 deriving (Eq, Show)
type FilterImports = Maybe (Set NameTe)

importQualifiedAs :: PathMod -> Modules src ss -> Imports
importQualifiedAs as (Modules mods) = Imports $ Map.fromList [(as, Nothing <$ mods)]

-- * Type 'Modules'
newtype Modules src ss
 =   Modules
 {   modules :: Map PathMod (Module src ss)
 } deriving (Eq, Show)

unionModules :: Modules src ss -> Modules src ss -> Either Error_Module (Modules src ss)
unionModules mx@(Modules x) my@(Modules y) =
	case check x y of
	 Just err -> Left err
	 Nothing  -> Right $ unionModulesUnchecked mx my
	where
	check ::
	 Map PathMod (Module src ss) ->
	 Map PathMod (Module src ss) ->
	 Maybe Error_Module
	check x' y' =
		case Map.intersectionWith (,) x' y' of
		 xy | null xy -> Nothing
		 xy ->
			let errs =
				Map.filter (not . null) $
				(<$> xy) $ \(a, b) ->
					inter a b module_prefix <>
					inter a b module_infix <>
					inter a b module_postfix in
			case errs of
			 e | null e -> Nothing
			 e -> Just $ Error_Module_colliding_Term e
		where
		inter a b f = Map.keysSet $ Map.intersection (f a) (f b)

unionModulesUnchecked :: Modules src ss -> Modules src ss -> Modules src ss
unionModulesUnchecked (Modules x) (Modules y) =
	Modules $ Map.unionWith (<>) x y

-- ** Type 'Error_Module'
data Error_Module
 =   Error_Module_colliding_Term (Map PathMod (Set NameTe))
 |   Error_Module_ambiguous (Mod NameTe) (Map PathMod NameTe)
 |   Error_Module_missing PathMod
 |   Error_Module_missing_Term (Mod NameTe)
 deriving (Eq, Show)

-- ** Type 'Module'
data Module src ss
 =   Module
 {   module_prefix  :: ModuleFixy src ss Unifix
 ,   module_infix   :: ModuleFixy src ss Infix
 ,   module_postfix :: ModuleFixy src ss Unifix
 } deriving (Eq, Show)

module_fixity :: FixitySing fixy -> Module src ss -> ModuleFixy src ss fixy
module_fixity = \case
	 FixitySing_Prefix  -> module_prefix
	 FixitySing_Infix   -> module_infix
	 FixitySing_Postfix -> module_postfix

moduleEmpty :: Module src ss
moduleEmpty = Module
 { module_prefix  = mempty
 , module_infix   = mempty
 , module_postfix = mempty
 }

moduleWhere :: forall src ss. Source src => PathMod -> [DefTerm src ss] -> (PathMod, Module src ss)
moduleWhere mod lst =
	(mod,) Module
	 { module_infix = mk $ \(n `WithFixity` fixy := t) ->
		case fixy of
		 Fixity2 inf -> [(n, Tokenizer inf $ Token_Term . setSource (TermAVT t))]
		 _ -> []
	 , module_prefix = mk $ \(n `WithFixity` fixy := t) ->
		case fixy of
		 Fixity1 pre@Prefix{} -> [(n, Tokenizer pre $ Token_Term . setSource (TermAVT t))]
		 _ -> []
	 , module_postfix = mk $ \(n `WithFixity` fixy := t) ->
		case fixy of
		 Fixity1 post@Postfix{} -> [(n, Tokenizer post $ Token_Term . setSource (TermAVT t))]
		 _ -> []
	 }
	where
	mk ::
	 (DefTerm src ss -> [(NameTe, Tokenizer fixy src ss)]) ->
	 Map NameTe (Tokenizer fixy src ss)
	mk = Map.fromList . (`foldMap` lst)

-- *** Type 'ModuleFixy'
type ModuleFixy src ss fixy = Map NameTe (Tokenizer fixy src ss)

instance Semigroup (Module src ss) where
	x <> y =
		Module
		 { module_prefix  = module_prefix  x <> module_prefix  y
		 , module_infix   = module_infix   x <> module_infix   y
		 , module_postfix = module_postfix x <> module_postfix y
		 }

-- ** Type 'Tokenizer'
data Tokenizer fixy src ss
 =   Tokenizer
 {   token_fixity :: fixy
 ,   token_term   :: src -> Token_Term src ss
 }
instance (Source src, Eq fixy) => Eq (Tokenizer fixy src ss) where
	Tokenizer fx x == Tokenizer fy y = fx == fy && (x noSource) == (y noSource)
instance Source src => Show (Tokenizer fixy src ss) where
	show (Tokenizer _fx x) = show (x noSource)

-- ** Type 'Token_Term'
data Token_Term src ss
 =   Token_Term      (TermAVT src ss)
 |   Token_TermVT    (TermVT src ss '[])
 |   Token_Term_Abst src NameTe (AST_Type src) (AST_Term src ss)
 |   Token_Term_Var  src NameTe
 |   Token_Term_Let  src NameTe (AST_Term src ss) (AST_Term src ss)
 |   Token_Term_App  src
 -- deriving (Eq, Show)
instance Source src => Eq (Token_Term src ss) where
	Token_Term   x == Token_Term   y = x == y
	Token_TermVT x == Token_TermVT y = x == y
	Token_Term_Abst _ nx ax rx == Token_Term_Abst _ ny ay ry = nx == ny && ax == ay && rx == ry
	Token_Term_Var _ x == Token_Term_Var _ y = x == y
	Token_Term_Let _ nx ax rx == Token_Term_Let _ ny ay ry = nx == ny && ax == ay && rx == ry
	Token_Term_App _ == Token_Term_App _ = True
	_ == _ = False
instance Source src => Show (Token_Term src ss) where
	showsPrec p (Token_Term   x) =
		showParen (p >= 10) $
		showString "Token_Term" .
		showChar ' ' . showsPrec 10 x
	showsPrec p (Token_TermVT x) =
		showParen (p >= 10) $
		showString "Token_TermVT" .
		showChar ' ' . showsPrec 10 x
	showsPrec p (Token_Term_Abst _ n a r) =
		showParen (p >= 10) $
		showString "Token_Term_Abst" .
		showChar ' ' . showsPrec 10 n .
		showChar ' ' . showsPrec 10 a .
		showChar ' ' . showsPrec 10 r
	showsPrec p (Token_Term_Var _ x) =
		showParen (p >= 10) $
		showString "Token_Term_Var" .
		showChar ' ' . showsPrec 10 x
	showsPrec p (Token_Term_Let _ n a r) =
		showParen (p >= 10) $
		showString "Token_Term_Let" .
		showChar ' ' . showsPrec 10 n .
		showChar ' ' . showsPrec 10 a .
		showChar ' ' . showsPrec 10 r
	showsPrec _p (Token_Term_App _) = showString "Token_Term_App"

-- ** Type 'NameTe'
newtype NameTe = NameTe Text
 deriving (Eq, Ord, Show)
instance IsString NameTe where
	fromString = NameTe . fromString

-- * Type 'CtxTy'
-- | /Typing context/
-- accumulating at each /lambda abstraction/
-- the 'Type' of the introduced variable.
-- It is built top-down from the closest
-- including /lambda abstraction/ to the farest.
data CtxTy src (ts::[K.Type]) where
	CtxTyZ :: CtxTy src '[]
	CtxTyS :: NameTe
	       -> Type  src '[] t
	       -> CtxTy src ts
	       -> CtxTy src (t ': ts)
infixr 5 `CtxTyS`

appendCtxTy
 :: CtxTy src ts0
 -> CtxTy src ts1
 -> CtxTy src (ts0 ++ ts1)
appendCtxTy CtxTyZ c          = c
appendCtxTy (CtxTyS n t c) c' = CtxTyS n t $ appendCtxTy c c'



-- ** Type 'AST_Term'
-- | /Abstract Syntax Tree/ of 'Token_Term'.
type AST_Term src ss = BinTree (Token_Term src ss)

-- * Class 'Inj_Modules'
type Inj_Modules  src ss
 =   Inj_ModulesR src ss ss

inj_Modules ::
 forall src ss.
 Inj_Modules src ss =>
 Either Error_Module (Modules src ss)
inj_Modules = inj_ModulesR @_ @_ @ss

-- ** Class 'Inj_ModulesR'
class Inj_ModulesR src (ss::[*]) (rs::[*]) where
	inj_ModulesR :: Either Error_Module (Modules src ss)
instance Inj_ModulesR src ss '[] where
	inj_ModulesR = Right $ Modules mempty
instance
 ( ModuleFor src ss s
 , Inj_ModulesR src ss rs
 ) => Inj_ModulesR src ss (Proxy s ': rs) where
	inj_ModulesR = do
		x <- inj_ModulesR @_ @_ @rs
		let (n, m) = moduleFor @_ @_  @s
		Modules (Map.singleton n m) `unionModules` x

-- * Type 'DefTerm'
data DefTerm src ss
 = forall vs t.
 (:=) (WithFixity NameTe)
      (forall ts. Term src ss ts vs t)

-- | Lookup given 'Mod' 'NameTe' into the 'Infix' 'TermDef' of given 'Modules'.
--
-- NOTE: 'Token_Term_App' is returned for the space 'NameTe'.
lookupDefTerm ::
 forall src ss fixy.
 FixitySing fixy ->
 Imports ->
 Mod NameTe ->
 Modules src ss ->
 Either Error_Module (Tokenizer fixy src ss)
lookupDefTerm FixitySing_Infix _is ([] `Mod` " ") _ms =
	Right $ Tokenizer
	 { token_term   = Token_Term_App @src @ss
	 , token_fixity = Infix (Just AssocL) 9
	 }
lookupDefTerm fixy (Imports is) mn@(m `Mod` n) (Modules mods) =
	let mod_fixy = module_fixity fixy in
	case Map.lookup m is of
	 Nothing ->
		maybe (Left $ Error_Module_missing m) Right (Map.lookup m mods) >>=
		maybe (Left $ Error_Module_missing_Term mn) Right .
		Map.lookup n . mod_fixy
	 Just ims ->
		let look =
		 -- n matches amongst ims
			(`Map.mapMaybeWithKey` ims) $ \im _ft -> -- TODO: filter NameTe
				Map.lookup im mods >>=
				Map.lookup n . mod_fixy >>=
				Just . Map.singleton n in
		case Map.minView look of
		 Nothing -> Left $ Error_Module_missing_Term mn
		 Just (r, rs) | null rs -> Right $ snd $ Map.findMin r
		              | otherwise -> Left $ Error_Module_ambiguous mn $ fst . Map.findMin <$> look

-- | Delete given 'Mod' 'NameTe' into given 'Modules'.
deleteDefTerm :: Mod NameTe -> Modules src ss -> Modules src ss
deleteDefTerm (m `Mod` n) (Modules ms) = Modules $ Map.adjust del m ms
	where del mod = mod
		 { module_prefix  = Map.delete n $ module_prefix  mod
		 , module_infix   = Map.delete n $ module_infix   mod
		 , module_postfix = Map.delete n $ module_postfix mod
		 }

-- | Delete given 'Mod' 'NameTe' into 'module_infix's of given 'Modules'.
deleteDefTermInfix :: Mod NameTe -> Modules src ss -> Modules src ss
deleteDefTermInfix (m `Mod` n) (Modules ms) = Modules $ Map.adjust del m ms
	where del mod = mod{module_infix = Map.delete n $ module_infix mod}

-- | Delete given 'Mod' 'NameTe' into 'module_prefix's of given 'Modules'.
deleteDefTermPrefix :: Mod NameTe -> Modules src ss -> Modules src ss
deleteDefTermPrefix (m `Mod` n) (Modules ms) = Modules $ Map.adjust del m ms
	where del mod = mod{module_prefix = Map.delete n $ module_prefix mod}

-- | Delete given 'Mod' 'NameTe' into 'module_postfix's of given 'Modules'.
deleteDefTermPostix :: Mod NameTe -> Modules src ss -> Modules src ss
deleteDefTermPostix (m `Mod` n) (Modules ms) = Modules $ Map.adjust del m ms
	where del mod = mod{module_postfix = Map.delete n $ module_postfix mod}

insertDefTerm ::
 forall src ss.
 Source src =>
 Mod (DefTerm src ss) -> Modules src ss -> Modules src ss
insertDefTerm (m `Mod` (n `WithFixity` fixy := t)) (Modules ms) =
	Modules $ Map.insert m (insertFixity ins fixy moduleEmpty) ms
	where
	ins :: fx -> ModuleFixy src ss fx -> ModuleFixy src ss fx
	ins fx = Map.insert n $ Tokenizer fx $ Token_Term . setSource (TermAVT t)

insertTermVT ::
 forall src ss.
 Source src =>
 Mod (TermVT src ss '[]) -> NameTe -> Fixity ->
 Modules src ss -> Modules src ss
insertTermVT (m `Mod` t) n fixy (Modules ms) =
	Modules $ Map.insert m (insertFixity ins fixy moduleEmpty) ms
	where
	ins :: fx -> ModuleFixy src ss fx -> ModuleFixy src ss fx
	ins fx = Map.insert n $ Tokenizer fx $ Token_TermVT . setSource t

insertFixity ::
 (forall fx. fx -> ModuleFixy src ss fx -> ModuleFixy src ss fx) ->
 Fixity -> Module src ss -> Module src ss
insertFixity ins fx mod =
	case fx of
	 Fixity1 uni@Prefix{}  -> mod {module_prefix  = ins uni $ module_prefix  mod}
	 Fixity2 inf@Infix{}   -> mod {module_infix   = ins inf $ module_infix   mod}
	 Fixity1 uni@Postfix{} -> mod {module_postfix = ins uni $ module_postfix mod}

-- ** Type 'WithFixity'
data WithFixity a
 =   WithFixity a Fixity
 deriving (Eq, Show)
instance IsString (WithFixity NameTe) where
	fromString a = WithFixity (fromString a) (Fixity2 infixN5)

withInfix :: a -> Infix -> WithFixity a
withInfix a inf = a `WithFixity` Fixity2 inf
withInfixR :: a -> Precedence -> WithFixity a
withInfixR a p = a `WithFixity` Fixity2 (infixR p)
withInfixL :: a -> Precedence -> WithFixity a
withInfixL a p = a `WithFixity` Fixity2 (infixL p)
withInfixN :: a -> Precedence -> WithFixity a
withInfixN a p = a `WithFixity` Fixity2 (infixN p)
withInfixB :: a -> (Side, Precedence) -> WithFixity a
withInfixB a (lr, p) = a `WithFixity` Fixity2 (infixB lr p)
withPrefix :: a -> Precedence -> WithFixity a
withPrefix a p = a `WithFixity` Fixity1 (Prefix p)
withPostfix :: a -> Precedence -> WithFixity a
withPostfix a p = a `WithFixity` Fixity1 (Postfix p)

-- ** Type 'FixitySing'
data FixitySing fixy where
 FixitySing_Prefix  :: FixitySing Unifix
 FixitySing_Infix   :: FixitySing Infix
 FixitySing_Postfix :: FixitySing Unifix
deriving instance Eq (FixitySing fixy)
deriving instance Show (FixitySing fixy)