symantic/Language/Symantic/Compiling/Module.hs

   1 {-# LANGUAGE AllowAmbiguousTypes #-}
   2 {-# LANGUAGE ConstraintKinds #-}
   3 {-# LANGUAGE DeriveFunctor #-}
   4 {-# LANGUAGE ExistentialQuantification #-}
   5 {-# LANGUAGE GADTs #-}
   6 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
   7 {-# LANGUAGE PolyKinds #-}
   8 {-# LANGUAGE UndecidableInstances #-}
   9 module Language.Symantic.Compiling.Module where
  10
  11 import Data.Bool (not)
  12 import Data.Map.Strict (Map)
  13 import Data.Semigroup (Semigroup(..))
  14 import Data.Set (Set)
  15 import Data.String (IsString(..))
  16 import Data.Text (Text)
  17 import Prelude hiding (mod, not, any)
  18 import qualified Data.Kind as K
  19 import qualified Data.Map.Strict as Map
  20
  21 import Language.Symantic.Grammar
  22 import Language.Symantic.Typing
  23 import Language.Symantic.Compiling.Term
  24
  25 -- * Type 'Mod'
  26 data Mod a = Mod PathMod a
  27  deriving (Eq, Functor, Ord, Show)
  28
  29 -- ** Type 'PathMod'
  30 type PathMod = [NameMod]
  31
  32 -- ** Type 'NameMod'
  33 newtype NameMod = NameMod Text
  34  deriving (Eq, Ord, Show)
  35 instance IsString NameMod where
  36         fromString = NameMod . fromString
  37
  38 -- * Class 'ModuleFor'
  39 class ModuleFor src ss s where
  40         moduleFor :: (PathMod, Module src ss)
  41         moduleFor = ([], moduleEmpty)
  42
  43 -- * Type 'Imports'
  44 newtype Imports = Imports (Map PathMod (Map PathMod FilterImports))
  45  deriving (Eq, Show)
  46 type FilterImports = Maybe (Set NameTe)
  47
  48 importQualifiedAs :: PathMod -> Modules src ss -> Imports
  49 importQualifiedAs as (Modules mods) = Imports $ Map.fromList [(as, Nothing <$ mods)]
  50
  51 -- * Type 'Modules'
  52 newtype Modules src ss
  53  =   Modules
  54  {   modules :: Map PathMod (Module src ss)
  55  } deriving (Eq, Show)
  56
  57 unionModules :: Modules src ss -> Modules src ss -> Either Error_Module (Modules src ss)
  58 unionModules mx@(Modules x) my@(Modules y) =
  59         case check x y of
  60          Just err -> Left err
  61          Nothing  -> Right $ unionModulesUnchecked mx my
  62         where
  63         check ::
  64          Map PathMod (Module src ss) ->
  65          Map PathMod (Module src ss) ->
  66          Maybe Error_Module
  67         check x' y' =
  68                 case Map.intersectionWith (,) x' y' of
  69                  xy | null xy -> Nothing
  70                  xy ->
  71                         let errs =
  72                                 Map.filter (not . null) $
  73                                 (<$> xy) $ \(a, b) ->
  74                                         inter a b module_prefix <>
  75                                         inter a b module_infix <>
  76                                         inter a b module_postfix in
  77                         case errs of
  78                          e | null e -> Nothing
  79                          e -> Just $ Error_Module_colliding_Term e
  80                 where
  81                 inter a b f = Map.keysSet $ Map.intersection (f a) (f b)
  82
  83 unionModulesUnchecked :: Modules src ss -> Modules src ss -> Modules src ss
  84 unionModulesUnchecked (Modules x) (Modules y) =
  85         Modules $ Map.unionWith (<>) x y
  86
  87 -- ** Type 'Error_Module'
  88 data Error_Module
  89  =   Error_Module_colliding_Term (Map PathMod (Set NameTe))
  90  |   Error_Module_ambiguous (Mod NameTe) (Map PathMod NameTe)
  91  |   Error_Module_missing PathMod
  92  |   Error_Module_missing_Term (Mod NameTe)
  93  deriving (Eq, Show)
  94
  95 -- ** Type 'Module'
  96 data Module src ss
  97  =   Module
  98  {   module_prefix  :: ModuleFixy src ss Unifix
  99  ,   module_infix   :: ModuleFixy src ss Infix
 100  ,   module_postfix :: ModuleFixy src ss Unifix
 101  } deriving (Eq, Show)
 102
 103 module_fixity :: FixitySing fixy -> Module src ss -> ModuleFixy src ss fixy
 104 module_fixity = \case
 105          FixitySing_Prefix  -> module_prefix
 106          FixitySing_Infix   -> module_infix
 107          FixitySing_Postfix -> module_postfix
 108
 109 moduleEmpty :: Module src ss
 110 moduleEmpty = Module
 111  { module_prefix  = mempty
 112  , module_infix   = mempty
 113  , module_postfix = mempty
 114  }
 115
 116 moduleWhere :: forall src ss. Source src => PathMod -> [DefTerm src ss] -> (PathMod, Module src ss)
 117 moduleWhere mod lst =
 118         (mod,) Module
 119          { module_infix = mk $ \(n `WithFixity` fixy := t) ->
 120                 case fixy of
 121                  Fixity2 inf -> [(n, Tokenizer inf $ Token_Term . setSource (TermAVT t))]
 122                  _ -> []
 123          , module_prefix = mk $ \(n `WithFixity` fixy := t) ->
 124                 case fixy of
 125                  Fixity1 pre@Prefix{} -> [(n, Tokenizer pre $ Token_Term . setSource (TermAVT t))]
 126                  _ -> []
 127          , module_postfix = mk $ \(n `WithFixity` fixy := t) ->
 128                 case fixy of
 129                  Fixity1 post@Postfix{} -> [(n, Tokenizer post $ Token_Term . setSource (TermAVT t))]
 130                  _ -> []
 131          }
 132         where
 133         mk ::
 134          (DefTerm src ss -> [(NameTe, Tokenizer fixy src ss)]) ->
 135          Map NameTe (Tokenizer fixy src ss)
 136         mk = Map.fromList . (`foldMap` lst)
 137
 138 -- *** Type 'ModuleFixy'
 139 type ModuleFixy src ss fixy = Map NameTe (Tokenizer fixy src ss)
 140
 141 instance Semigroup (Module src ss) where
 142         x <> y =
 143                 Module
 144                  { module_prefix  = module_prefix  x <> module_prefix  y
 145                  , module_infix   = module_infix   x <> module_infix   y
 146                  , module_postfix = module_postfix x <> module_postfix y
 147                  }
 148
 149 -- ** Type 'Tokenizer'
 150 data Tokenizer fixy src ss
 151  =   Tokenizer
 152  {   token_fixity :: fixy
 153  ,   token_term   :: src -> Token_Term src ss
 154  }
 155 instance (Source src, Eq fixy) => Eq (Tokenizer fixy src ss) where
 156         Tokenizer fx x == Tokenizer fy y = fx == fy && (x noSource) == (y noSource)
 157 instance Source src => Show (Tokenizer fixy src ss) where
 158         show (Tokenizer _fx x) = show (x noSource)
 159
 160 -- ** Type 'Token_Term'
 161 data Token_Term src ss
 162  =   Token_Term      (TermAVT src ss)
 163  |   Token_TermVT    (TermVT src ss '[])
 164  |   Token_Term_Abst src NameTe (AST_Type src) (AST_Term src ss)
 165  |   Token_Term_Var  src NameTe
 166  |   Token_Term_Let  src NameTe (AST_Term src ss) (AST_Term src ss)
 167  |   Token_Term_App  src
 168  -- deriving (Eq, Show)
 169 instance Source src => Eq (Token_Term src ss) where
 170         Token_Term   x == Token_Term   y = x == y
 171         Token_TermVT x == Token_TermVT y = x == y
 172         Token_Term_Abst _ nx ax rx == Token_Term_Abst _ ny ay ry = nx == ny && ax == ay && rx == ry
 173         Token_Term_Var _ x == Token_Term_Var _ y = x == y
 174         Token_Term_Let _ nx ax rx == Token_Term_Let _ ny ay ry = nx == ny && ax == ay && rx == ry
 175         Token_Term_App _ == Token_Term_App _ = True
 176         _ == _ = False
 177 instance Source src => Show (Token_Term src ss) where
 178         showsPrec p (Token_Term   x) =
 179                 showParen (p >= 10) $
 180                 showString "Token_Term" .
 181                 showChar ' ' . showsPrec 10 x
 182         showsPrec p (Token_TermVT x) =
 183                 showParen (p >= 10) $
 184                 showString "Token_TermVT" .
 185                 showChar ' ' . showsPrec 10 x
 186         showsPrec p (Token_Term_Abst _ n a r) =
 187                 showParen (p >= 10) $
 188                 showString "Token_Term_Abst" .
 189                 showChar ' ' . showsPrec 10 n .
 190                 showChar ' ' . showsPrec 10 a .
 191                 showChar ' ' . showsPrec 10 r
 192         showsPrec p (Token_Term_Var _ x) =
 193                 showParen (p >= 10) $
 194                 showString "Token_Term_Var" .
 195                 showChar ' ' . showsPrec 10 x
 196         showsPrec p (Token_Term_Let _ n a r) =
 197                 showParen (p >= 10) $
 198                 showString "Token_Term_Let" .
 199                 showChar ' ' . showsPrec 10 n .
 200                 showChar ' ' . showsPrec 10 a .
 201                 showChar ' ' . showsPrec 10 r
 202         showsPrec _p (Token_Term_App _) = showString "Token_Term_App"
 203
 204 -- ** Type 'NameTe'
 205 newtype NameTe = NameTe Text
 206  deriving (Eq, Ord, Show)
 207 instance IsString NameTe where
 208         fromString = NameTe . fromString
 209
 210 -- * Type 'CtxTy'
 211 -- | /Typing context/
 212 -- accumulating at each /lambda abstraction/
 213 -- the 'Type' of the introduced variable.
 214 -- It is built top-down from the closest
 215 -- including /lambda abstraction/ to the farest.
 216 data CtxTy src (ts::[K.Type]) where
 217         CtxTyZ :: CtxTy src '[]
 218         CtxTyS :: NameTe
 219                -> Type  src '[] t
 220                -> CtxTy src ts
 221                -> CtxTy src (t ': ts)
 222 infixr 5 `CtxTyS`
 223
 224 appendCtxTy
 225  :: CtxTy src ts0
 226  -> CtxTy src ts1
 227  -> CtxTy src (ts0 ++ ts1)
 228 appendCtxTy CtxTyZ c          = c
 229 appendCtxTy (CtxTyS n t c) c' = CtxTyS n t $ appendCtxTy c c'
 230
 231
 232
 233 -- ** Type 'AST_Term'
 234 -- | /Abstract Syntax Tree/ of 'Token_Term'.
 235 type AST_Term src ss = BinTree (Token_Term src ss)
 236
 237 -- * Class 'Inj_Modules'
 238 type Inj_Modules  src ss
 239  =   Inj_ModulesR src ss ss
 240
 241 inj_Modules ::
 242  forall src ss.
 243  Inj_Modules src ss =>
 244  Either Error_Module (Modules src ss)
 245 inj_Modules = inj_ModulesR @_ @_ @ss
 246
 247 -- ** Class 'Inj_ModulesR'
 248 class Inj_ModulesR src (ss::[*]) (rs::[*]) where
 249         inj_ModulesR :: Either Error_Module (Modules src ss)
 250 instance Inj_ModulesR src ss '[] where
 251         inj_ModulesR = Right $ Modules mempty
 252 instance
 253  ( ModuleFor src ss s
 254  , Inj_ModulesR src ss rs
 255  ) => Inj_ModulesR src ss (Proxy s ': rs) where
 256         inj_ModulesR = do
 257                 x <- inj_ModulesR @_ @_ @rs
 258                 let (n, m) = moduleFor @_ @_  @s
 259                 Modules (Map.singleton n m) `unionModules` x
 260
 261 -- * Type 'DefTerm'
 262 data DefTerm src ss
 263  = forall vs t.
 264  (:=) (WithFixity NameTe)
 265       (forall ts. Term src ss ts vs t)
 266
 267 -- | Lookup given 'Mod' 'NameTe' into the 'Infix' 'TermDef' of given 'Modules'.
 268 --
 269 -- NOTE: 'Token_Term_App' is returned for the space 'NameTe'.
 270 lookupDefTerm ::
 271  forall src ss fixy.
 272  FixitySing fixy ->
 273  Imports ->
 274  Mod NameTe ->
 275  Modules src ss ->
 276  Either Error_Module (Tokenizer fixy src ss)
 277 lookupDefTerm FixitySing_Infix _is ([] `Mod` " ") _ms =
 278         Right $ Tokenizer
 279          { token_term   = Token_Term_App @src @ss
 280          , token_fixity = Infix (Just AssocL) 9
 281          }
 282 lookupDefTerm fixy (Imports is) mn@(m `Mod` n) (Modules mods) =
 283         let mod_fixy = module_fixity fixy in
 284         case Map.lookup m is of
 285          Nothing ->
 286                 maybe (Left $ Error_Module_missing m) Right (Map.lookup m mods) >>=
 287                 maybe (Left $ Error_Module_missing_Term mn) Right .
 288                 Map.lookup n . mod_fixy
 289          Just ims ->
 290                 let look =
 291                  -- n matches amongst ims
 292                         (`Map.mapMaybeWithKey` ims) $ \im _ft -> -- TODO: filter NameTe
 293                                 Map.lookup im mods >>=
 294                                 Map.lookup n . mod_fixy >>=
 295                                 Just . Map.singleton n in
 296                 case Map.minView look of
 297                  Nothing -> Left $ Error_Module_missing_Term mn
 298                  Just (r, rs) | null rs -> Right $ snd $ Map.findMin r
 299                               | otherwise -> Left $ Error_Module_ambiguous mn $ fst . Map.findMin <$> look
 300
 301 -- | Delete given 'Mod' 'NameTe' into given 'Modules'.
 302 deleteDefTerm :: Mod NameTe -> Modules src ss -> Modules src ss
 303 deleteDefTerm (m `Mod` n) (Modules ms) = Modules $ Map.adjust del m ms
 304         where del mod = mod
 305                  { module_prefix  = Map.delete n $ module_prefix  mod
 306                  , module_infix   = Map.delete n $ module_infix   mod
 307                  , module_postfix = Map.delete n $ module_postfix mod
 308                  }
 309
 310 -- | Delete given 'Mod' 'NameTe' into 'module_infix's of given 'Modules'.
 311 deleteDefTermInfix :: Mod NameTe -> Modules src ss -> Modules src ss
 312 deleteDefTermInfix (m `Mod` n) (Modules ms) = Modules $ Map.adjust del m ms
 313         where del mod = mod{module_infix = Map.delete n $ module_infix mod}
 314
 315 -- | Delete given 'Mod' 'NameTe' into 'module_prefix's of given 'Modules'.
 316 deleteDefTermPrefix :: Mod NameTe -> Modules src ss -> Modules src ss
 317 deleteDefTermPrefix (m `Mod` n) (Modules ms) = Modules $ Map.adjust del m ms
 318         where del mod = mod{module_prefix = Map.delete n $ module_prefix mod}
 319
 320 -- | Delete given 'Mod' 'NameTe' into 'module_postfix's of given 'Modules'.
 321 deleteDefTermPostix :: Mod NameTe -> Modules src ss -> Modules src ss
 322 deleteDefTermPostix (m `Mod` n) (Modules ms) = Modules $ Map.adjust del m ms
 323         where del mod = mod{module_postfix = Map.delete n $ module_postfix mod}
 324
 325 insertDefTerm ::
 326  forall src ss.
 327  Source src =>
 328  Mod (DefTerm src ss) -> Modules src ss -> Modules src ss
 329 insertDefTerm (m `Mod` (n `WithFixity` fixy := t)) (Modules ms) =
 330         Modules $ Map.insert m (insFixy fixy moduleEmpty) ms
 331         where
 332         insFixy :: Fixity -> Module src ss -> Module src ss
 333         insFixy f mod =
 334                 case f of
 335                  Fixity1 uni@Prefix{}  -> mod {module_prefix  = ins uni $ module_prefix  mod}
 336                  Fixity2 inf@Infix{}   -> mod {module_infix   = ins inf $ module_infix   mod}
 337                  Fixity1 uni@Postfix{} -> mod {module_postfix = ins uni $ module_postfix mod}
 338         ins :: f -> ModuleFixy src ss f -> ModuleFixy src ss f
 339         ins f = Map.insert n $ Tokenizer f $ Token_Term . setSource (TermAVT t)
 340
 341 insertTermVT ::
 342  forall src ss.
 343  Source src =>
 344  Mod (TermVT src ss '[]) -> NameTe -> Fixity ->
 345  Modules src ss -> Modules src ss
 346 insertTermVT (m `Mod` t) n fixy (Modules ms) =
 347         Modules $ Map.insert m (insFixy fixy moduleEmpty) ms
 348         where
 349         insFixy :: Fixity -> Module src ss -> Module src ss
 350         insFixy f mod =
 351                 case f of
 352                  Fixity1 uni@Prefix{}  -> mod {module_prefix  = ins uni $ module_prefix  mod}
 353                  Fixity2 inf@Infix{}   -> mod {module_infix   = ins inf $ module_infix   mod}
 354                  Fixity1 uni@Postfix{} -> mod {module_postfix = ins uni $ module_postfix mod}
 355         ins :: f -> ModuleFixy src ss f -> ModuleFixy src ss f
 356         ins f = Map.insert n $ Tokenizer f $ Token_TermVT . setSource t
 357
 358 -- ** Type 'WithFixity'
 359 data WithFixity a
 360  =   WithFixity a Fixity
 361  deriving (Eq, Show)
 362 instance IsString (WithFixity NameTe) where
 363         fromString a = WithFixity (fromString a) (Fixity2 infixN5)
 364
 365 withInfix :: a -> Infix -> WithFixity a
 366 withInfix a inf = a `WithFixity` Fixity2 inf
 367 withInfixR :: a -> Precedence -> WithFixity a
 368 withInfixR a p = a `WithFixity` Fixity2 (infixR p)
 369 withInfixL :: a -> Precedence -> WithFixity a
 370 withInfixL a p = a `WithFixity` Fixity2 (infixL p)
 371 withInfixN :: a -> Precedence -> WithFixity a
 372 withInfixN a p = a `WithFixity` Fixity2 (infixN p)
 373 withInfixB :: a -> (Side, Precedence) -> WithFixity a
 374 withInfixB a (lr, p) = a `WithFixity` Fixity2 (infixB lr p)
 375 withPrefix :: a -> Precedence -> WithFixity a
 376 withPrefix a p = a `WithFixity` Fixity1 (Prefix p)
 377 withPostfix :: a -> Precedence -> WithFixity a
 378 withPostfix a p = a `WithFixity` Fixity1 (Postfix p)
 379
 380 -- ** Type 'FixitySing'
 381 data FixitySing fixy where
 382  FixitySing_Prefix  :: FixitySing Unifix
 383  FixitySing_Infix   :: FixitySing Infix
 384  FixitySing_Postfix :: FixitySing Unifix
 385 deriving instance Eq (FixitySing fixy)
 386 deriving instance Show (FixitySing fixy)