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
data Mod a = Mod PathMod a
deriving (Eq, Functor, Ord, Show)
type PathMod = [NameMod]
newtype NameMod = NameMod Text
deriving (Eq, Ord, Show)
instance IsString NameMod where
fromString = NameMod . fromString
class ModuleFor src ss s where
moduleFor :: (PathMod, Module src ss)
moduleFor = ([], moduleEmpty)
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)]
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
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)
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 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
}
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)
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
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"
newtype NameTe = NameTe Text
deriving (Eq, Ord, Show)
instance IsString NameTe where
fromString = NameTe . fromString
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 src ss = BinTree (Token_Term src ss)
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 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
data DefTerm src ss
= forall vs t.
(:=) (WithFixity NameTe)
(forall ts. Term src ss ts vs t)
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 =
(`Map.mapMaybeWithKey` ims) $ \im _ft ->
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
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
}
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}
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}
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}
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)
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)