+{-# 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.Proxy (Proxy(..))
+import Data.Maybe (fromMaybe)
import Data.Semigroup (Semigroup(..))
import Data.Set (Set)
import Data.String (IsString(..))
-import Data.Text (Text)
-import Prelude hiding (mod, not, any)
+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
--- * 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)]
+ 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) =
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
+ 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
= 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)
+ | Error_Module_missing_Term (Mod NameTe) -- FixyA
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
+type Module src ss = ByFixity (ModuleFixy src ss Unifix)
+ (ModuleFixy src ss Infix)
+ (ModuleFixy src ss Unifix)
moduleEmpty :: Module src ss
-moduleEmpty = Module
- { module_prefix = mempty
- , module_infix = mempty
- , module_postfix = mempty
+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,) Module
- { module_infix = mk $ \(n `WithFixity` fixy := t) ->
+ (mod,) ByFixity
+ { byInfix = mk $ \(n `WithFixity` fixy := t) ->
case fixy of
- Fixity2 inf -> [(n, Tokenizer inf $ Token_Term . setSource (TermVT_CF t))]
+ Fixity2 inf -> [(n, Tokenizer inf $ Token_Term . setSource (TermAVT t))]
_ -> []
- , module_prefix = mk $ \(n `WithFixity` fixy := t) ->
+ , byPrefix = mk $ \(n `WithFixity` fixy := t) ->
case fixy of
- Fixity1 pre@Prefix{} -> [(n, Tokenizer pre $ Token_Term . setSource (TermVT_CF t))]
+ Fixity1 pre@Prefix{} -> [(n, Tokenizer pre $ Token_Term . setSource (TermAVT t))]
_ -> []
- , module_postfix = mk $ \(n `WithFixity` fixy := t) ->
+ , byPostfix = mk $ \(n `WithFixity` fixy := t) ->
case fixy of
- Fixity1 post@Postfix{} -> [(n, Tokenizer post $ Token_Term . setSource (TermVT_CF t))]
+ 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)
+ (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 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 ModuleFixy src ss fixy = Map NameTe (Tokenizer src ss fixy)
-- ** Type 'Tokenizer'
-data Tokenizer fixy src ss
+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 (TermVT_CF 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)
+ -- 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 '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
+-- ** 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
-inj_Modules :: forall src ss. Inj_Modules src ss => Either Error_Module (Modules src ss)
-inj_Modules = inj_ModulesR (Proxy @ss)
+-- * Class 'ModulesInj'
+type ModulesInj src ss
+ = ModulesInjR src ss 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
+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
- , 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)
+ , 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 es. Term src ss es vs t)
+ (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 ->
+ 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 fixy src ss)
-lookupDefTerm FixitySing_Infix _is ([] `Mod` " ") _ms =
+ 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 (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
+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
- { module_prefix = Map.delete n $ module_prefix mod
- , module_infix = Map.delete n $ module_infix mod
- , module_postfix = Map.delete n $ module_postfix mod
+ { byPrefix = Map.delete n $ byPrefix mod
+ , byInfix = Map.delete n $ byInfix mod
+ , byPostfix = Map.delete n $ byPostfix mod
}
--- | Delete given 'Mod' 'NameTe' into 'module_infix's of given 'Modules'.
+-- | 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{module_infix = Map.delete n $ module_infix mod}
+ where del mod = mod{byInfix = Map.delete n $ byInfix mod}
--- | Delete given 'Mod' 'NameTe' into 'module_prefix's of given 'Modules'.
+-- | 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{module_prefix = Map.delete n $ module_prefix mod}
+ where del mod = mod{byPrefix = Map.delete n $ byPrefix mod}
--- | Delete given 'Mod' 'NameTe' into 'module_postfix's of given 'Modules'.
+-- | 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{module_postfix = Map.delete n $ module_postfix mod}
+ 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 (insFixy fixy moduleEmpty) ms
+ Modules $ Map.insert m (insertFixity ins 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)
+ ins :: fx -> ModuleFixy src ss fx -> ModuleFixy src ss fx
+ ins fx = Map.insert n $ Tokenizer fx $ Token_Term . setSource (TermAVT t)
-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)
+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}
sourcephile / git / haskell / symantic.git / blobdiff