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  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 :: forall src ss. Inj_Modules src ss => Either Error_Module (Modules src ss)
 242 inj_Modules = inj_ModulesR (Proxy @ss)
 243
 244 -- ** Class 'Inj_ModulesR'
 245 class Inj_ModulesR src (ss::[*]) (rs::[*]) where
 246         inj_ModulesR :: Proxy rs -> Either Error_Module (Modules src ss)
 247 instance Inj_ModulesR src ss '[] where
 248         inj_ModulesR _rs = Right $ Modules mempty
 249 instance
 250  ( ModuleFor src ss s
 251  , Inj_ModulesR src ss rs
 252  ) => Inj_ModulesR src ss (Proxy s ': rs) where
 253         inj_ModulesR _s = do
 254                 x <- inj_ModulesR (Proxy @rs)
 255                 let (n, m) = moduleFor (Proxy @s)
 256                 Modules (Map.singleton n m) `unionModules` x
 257
 258 -- * Type 'DefTerm'
 259 data DefTerm src ss
 260  = forall vs t.
 261  (:=) (WithFixity NameTe)
 262       (forall ts. Term src ss ts vs t)
 263
 264 -- | Lookup given 'Mod' 'NameTe' into the 'Infix' 'TermDef' of given 'Modules'.
 265 --
 266 -- NOTE: 'Token_Term_App' is returned for the space 'NameTe'.
 267 lookupDefTerm ::
 268  forall src ss fixy.
 269  FixitySing fixy ->
 270  Imports ->
 271  Mod NameTe ->
 272  Modules src ss ->
 273  Either Error_Module (Tokenizer fixy src ss)
 274 lookupDefTerm FixitySing_Infix _is ([] `Mod` " ") _ms =
 275         Right $ Tokenizer
 276          { token_term   = Token_Term_App @src @ss
 277          , token_fixity = Infix (Just AssocL) 9
 278          }
 279 lookupDefTerm fixy (Imports is) mn@(m `Mod` n) (Modules mods) =
 280         let mod_fixy = module_fixity fixy in
 281         case Map.lookup m is of
 282          Nothing ->
 283                 maybe (Left $ Error_Module_missing m) Right (Map.lookup m mods) >>=
 284                 maybe (Left $ Error_Module_missing_Term mn) Right .
 285                 Map.lookup n . mod_fixy
 286          Just ims ->
 287                 let look =
 288                  -- n matches amongst ims
 289                         (`Map.mapMaybeWithKey` ims) $ \im _ft -> -- TODO: filter NameTe
 290                                 Map.lookup im mods >>=
 291                                 Map.lookup n . mod_fixy >>=
 292                                 Just . Map.singleton n in
 293                 case Map.minView look of
 294                  Nothing -> Left $ Error_Module_missing_Term mn
 295                  Just (r, rs) | null rs -> Right $ snd $ Map.findMin r
 296                               | otherwise -> Left $ Error_Module_ambiguous mn $ fst . Map.findMin <$> look
 297
 298 -- | Delete given 'Mod' 'NameTe' into given 'Modules'.
 299 deleteDefTerm :: Mod NameTe -> Modules src ss -> Modules src ss
 300 deleteDefTerm (m `Mod` n) (Modules ms) = Modules $ Map.adjust del m ms
 301         where del mod = mod
 302                  { module_prefix  = Map.delete n $ module_prefix  mod
 303                  , module_infix   = Map.delete n $ module_infix   mod
 304                  , module_postfix = Map.delete n $ module_postfix mod
 305                  }
 306
 307 -- | Delete given 'Mod' 'NameTe' into 'module_infix's of given 'Modules'.
 308 deleteDefTermInfix :: Mod NameTe -> Modules src ss -> Modules src ss
 309 deleteDefTermInfix (m `Mod` n) (Modules ms) = Modules $ Map.adjust del m ms
 310         where del mod = mod{module_infix = Map.delete n $ module_infix mod}
 311
 312 -- | Delete given 'Mod' 'NameTe' into 'module_prefix's of given 'Modules'.
 313 deleteDefTermPrefix :: Mod NameTe -> Modules src ss -> Modules src ss
 314 deleteDefTermPrefix (m `Mod` n) (Modules ms) = Modules $ Map.adjust del m ms
 315         where del mod = mod{module_prefix = Map.delete n $ module_prefix mod}
 316
 317 -- | Delete given 'Mod' 'NameTe' into 'module_postfix's of given 'Modules'.
 318 deleteDefTermPostix :: Mod NameTe -> Modules src ss -> Modules src ss
 319 deleteDefTermPostix (m `Mod` n) (Modules ms) = Modules $ Map.adjust del m ms
 320         where del mod = mod{module_postfix = Map.delete n $ module_postfix mod}
 321
 322 insertDefTerm ::
 323  forall src ss.
 324  Source src =>
 325  Mod (DefTerm src ss) -> Modules src ss -> Modules src ss
 326 insertDefTerm (m `Mod` (n `WithFixity` fixy := t)) (Modules ms) =
 327         Modules $ Map.insert m (insFixy fixy moduleEmpty) ms
 328         where
 329         insFixy :: Fixity -> Module src ss -> Module src ss
 330         insFixy f mod =
 331                 case f of
 332                  Fixity1 uni@Prefix{}  -> mod {module_prefix  = ins uni $ module_prefix  mod}
 333                  Fixity2 inf@Infix{}   -> mod {module_infix   = ins inf $ module_infix   mod}
 334                  Fixity1 uni@Postfix{} -> mod {module_postfix = ins uni $ module_postfix mod}
 335         ins :: f -> ModuleFixy src ss f -> ModuleFixy src ss f
 336         ins f = Map.insert n $ Tokenizer f $ Token_Term . setSource (TermAVT t)
 337
 338 insertTermVT ::
 339  forall src ss.
 340  Source src =>
 341  Mod (TermVT src ss '[]) -> NameTe -> Fixity ->
 342  Modules src ss -> Modules src ss
 343 insertTermVT (m `Mod` t) n fixy (Modules ms) =
 344         Modules $ Map.insert m (insFixy fixy moduleEmpty) ms
 345         where
 346         insFixy :: Fixity -> Module src ss -> Module src ss
 347         insFixy f mod =
 348                 case f of
 349                  Fixity1 uni@Prefix{}  -> mod {module_prefix  = ins uni $ module_prefix  mod}
 350                  Fixity2 inf@Infix{}   -> mod {module_infix   = ins inf $ module_infix   mod}
 351                  Fixity1 uni@Postfix{} -> mod {module_postfix = ins uni $ module_postfix mod}
 352         ins :: f -> ModuleFixy src ss f -> ModuleFixy src ss f
 353         ins f = Map.insert n $ Tokenizer f $ Token_TermVT . setSource t
 354
 355 -- ** Type 'WithFixity'
 356 data WithFixity a
 357  =   WithFixity a Fixity
 358  deriving (Eq, Show)
 359 instance IsString (WithFixity NameTe) where
 360         fromString a = WithFixity (fromString a) (Fixity2 infixN5)
 361
 362 withInfix :: a -> Infix -> WithFixity a
 363 withInfix a inf = a `WithFixity` Fixity2 inf
 364 withInfixR :: a -> Precedence -> WithFixity a
 365 withInfixR a p = a `WithFixity` Fixity2 (infixR p)
 366 withInfixL :: a -> Precedence -> WithFixity a
 367 withInfixL a p = a `WithFixity` Fixity2 (infixL p)
 368 withInfixN :: a -> Precedence -> WithFixity a
 369 withInfixN a p = a `WithFixity` Fixity2 (infixN p)
 370 withInfixB :: a -> (Side, Precedence) -> WithFixity a
 371 withInfixB a (lr, p) = a `WithFixity` Fixity2 (infixB lr p)
 372 withPrefix :: a -> Precedence -> WithFixity a
 373 withPrefix a p = a `WithFixity` Fixity1 (Prefix p)
 374 withPostfix :: a -> Precedence -> WithFixity a
 375 withPostfix a p = a `WithFixity` Fixity1 (Postfix p)
 376
 377 -- ** Type 'FixitySing'
 378 data FixitySing fixy where
 379  FixitySing_Prefix  :: FixitySing Unifix
 380  FixitySing_Infix   :: FixitySing Infix
 381  FixitySing_Postfix :: FixitySing Unifix
 382 deriving instance Eq (FixitySing fixy)
 383 deriving instance Show (FixitySing fixy)