{-# 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.Proxy (Proxy(..))
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.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

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

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

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

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

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

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
 }

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 (TermVT_CF t))]
		 _ -> []
	 , module_prefix = mk $ \(n `WithFixity` fixy := t) ->
		case fixy of
		 Fixity1 pre@Prefix{} -> [(n, Tokenizer pre $ Token_Term . setSource (TermVT_CF t))]
		 _ -> []
	 , module_postfix = mk $ \(n `WithFixity` fixy := t) ->
		case fixy of
		 Fixity1 post@Postfix{} -> [(n, Tokenizer post $ Token_Term . setSource (TermVT_CF 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)

deriving instance
 ( Show (Tokenizer Unifix src ss)
 , Show (Tokenizer Infix  src ss)
 ) => Show (Module 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
 }

-- ** Type 'Token_Term'
data Token_Term src ss
 =   Token_Term (TermVT_CF 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)

-- ** 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 (Proxy @ss)

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

-- * Type 'DefTerm'
data DefTerm src ss
 = forall vs t.
 (:=) (WithFixity NameTe)
      (forall es. Term src ss es 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 (insFixy fixy moduleEmpty) ms
	where
	insFixy :: Fixity -> Module src ss -> Module src ss
	insFixy f mod =
		case f 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}
	ins :: f -> ModuleFixy src ss f -> ModuleFixy src ss f
	ins f = Map.insert n $ Tokenizer f $ Token_Term . setSource (TermVT_CF t)

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