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

import Data.Bool (not)
import Data.Map.Strict (Map)
import Data.Maybe (fromMaybe)
import Data.Semigroup (Semigroup(..))
import Data.Set (Set)
import Data.String (IsString(..))
import Prelude hiding (mod, not)
import qualified Data.Map.Strict as Map

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

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

importModules :: PathMod -> Modules src ss -> Imports NameTe
importModules as (Modules mods) =
	Imports $ Map.singleton as $
	Map.foldrWithKey
	 (\pm (ByFixity mp mi mq) acc ->
		acc <> ByFixity
		 { byPrefix  = pm <$ mp
		 , byInfix   = pm <$ mi
		 , byPostfix = pm <$ mq
		 }
	 ) mempty 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 byPrefix <>
					inter a b byInfix <>
					inter a b byPostfix 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) -- FixyA
 deriving (Eq, Show)

-- ** Type 'Module'
type Module src ss = ByFixity (ModuleFixy src ss Unifix)
                              (ModuleFixy src ss Infix)
                              (ModuleFixy src ss Unifix)

moduleEmpty :: Module src ss
moduleEmpty = ByFixity
 { byPrefix  = mempty
 , byInfix   = mempty
 , byPostfix = mempty
 }

moduleWhere :: forall src ss. Source src => PathMod -> [DefTerm src ss] -> (PathMod, Module src ss)
moduleWhere mod lst =
	(mod,) ByFixity
	 { byInfix = mk $ \(n `WithFixity` fixy := t) ->
		case fixy of
		 Fixity2 inf -> [(n, Tokenizer inf $ Token_Term . setSource (TermAVT t))]
		 _ -> []
	 , byPrefix = mk $ \(n `WithFixity` fixy := t) ->
		case fixy of
		 Fixity1 pre@Prefix{} -> [(n, Tokenizer pre $ Token_Term . setSource (TermAVT t))]
		 _ -> []
	 , byPostfix = 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 src ss fixy)]) ->
	 Map NameTe (Tokenizer src ss fixy)
	mk = Map.fromList . (`foldMap` lst)

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

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

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

-- ** 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 Name
 deriving (Eq, Ord, Show)
instance IsString NameTe where
	fromString = NameTe . fromString
instance NameOf NameTe where
	nameOf (NameTe n) = n

-- * Class 'ModulesInj'
type ModulesInj  src ss
 =   ModulesInjR src ss ss

modulesInj ::
 forall src ss.
 ModulesInj src ss =>
 Either Error_Module (Modules src ss)
modulesInj = modulesInjR @_ @_ @ss

-- ** Class 'ModulesInjR'
class ModulesInjR src (ss::[*]) (rs::[*]) where
	modulesInjR :: Either Error_Module (Modules src ss)
instance ModulesInjR src ss '[] where
	modulesInjR = Right $ Modules mempty
instance
 ( ModuleFor src ss s
 , ModulesInjR src ss rs
 ) => ModulesInjR src ss (Proxy s ': rs) where
	modulesInjR = do
		x <- modulesInjR @_ @_ @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.
 Fixy (ModuleFixy src ss Unifix)
      (ModuleFixy src ss Infix)
      (ModuleFixy src ss Unifix)
      (ModuleFixy src ss fixy) ->
 Imports NameTe ->
 Mod NameTe ->
 Modules src ss ->
 Either Error_Module (Tokenizer src ss fixy)
lookupDefTerm FixyInfix _is ([] `Mod` " ") _ms =
	Right $ Tokenizer
	 { token_term   = Token_Term_App @src @ss
	 , token_fixity = Infix (Just AssocL) 9
	 }
lookupDefTerm fixy imps mn@(m `Mod` n) (Modules mods) =
	let m' = m `fromMaybe` lookupImports fixy mn imps in
	maybe (Left $ Error_Module_missing m') Right (Map.lookup m' mods) >>=
	maybe (Left $ Error_Module_missing_Term mn) Right .
	Map.lookup n . selectByFixity fixy

-- | 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
		 { byPrefix  = Map.delete n $ byPrefix  mod
		 , byInfix   = Map.delete n $ byInfix   mod
		 , byPostfix = Map.delete n $ byPostfix mod
		 }

-- | Delete given 'Mod' 'NameTe' into 'byInfix'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{byInfix = Map.delete n $ byInfix mod}

-- | Delete given 'Mod' 'NameTe' into 'byPrefix'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{byPrefix = Map.delete n $ byPrefix mod}

-- | Delete given 'Mod' 'NameTe' into 'byPostfix'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{byPostfix = Map.delete n $ byPostfix 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 {byPrefix  = ins uni $ byPrefix  mod}
	 Fixity2 inf@Infix{}   -> mod {byInfix   = ins inf $ byInfix   mod}
	 Fixity1 uni@Postfix{} -> mod {byPostfix = ins uni $ byPostfix mod}