symantic/Language/Symantic/Compiling/Module.hs

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