symantic/Language/Symantic/Compiling/Module.hs

   1 {-# LANGUAGE AllowAmbiguousTypes #-}
   2 {-# LANGUAGE ConstraintKinds #-}
   3 {-# LANGUAGE ExistentialQuantification #-}
   4 {-# LANGUAGE GADTs #-}
   5 {-# LANGUAGE PolyKinds #-}
   6 {-# LANGUAGE UndecidableInstances #-}
   7 module Language.Symantic.Compiling.Module where
   8
   9 import Data.Bool (not)
  10 import Data.Map.Strict (Map)
  11 import Data.Maybe (fromMaybe)
  12 import Data.Semigroup (Semigroup(..))
  13 import Data.Set (Set)
  14 import Data.String (IsString(..))
  15 import Prelude hiding (mod, not)
  16 import qualified Data.Map.Strict as Map
  17
  18 import Language.Symantic.Grammar
  19 import Language.Symantic.Typing
  20 import Language.Symantic.Compiling.Term
  21
  22 -- * Class 'ModuleFor'
  23 class ModuleFor src ss s where
  24         moduleFor :: (PathMod, Module src ss)
  25         moduleFor = ([], moduleEmpty)
  26
  27 importModules :: PathMod -> Modules src ss -> Imports NameTe
  28 importModules as (Modules mods) =
  29         Imports $ Map.singleton as $
  30         Map.foldrWithKey
  31          (\pm (ByFixity mp mi mq) acc ->
  32                 acc <> ByFixity
  33                  { byPrefix  = pm <$ mp
  34                  , byInfix   = pm <$ mi
  35                  , byPostfix = pm <$ mq
  36                  }
  37          ) mempty mods
  38
  39 -- * Type 'Modules'
  40 newtype Modules src ss
  41  =   Modules
  42  {   modules :: Map PathMod (Module src ss)
  43  } deriving (Eq, Show)
  44
  45 unionModules :: Modules src ss -> Modules src ss -> Either Error_Module (Modules src ss)
  46 unionModules mx@(Modules x) my@(Modules y) =
  47         case check x y of
  48          Just err -> Left err
  49          Nothing  -> Right $ unionModulesUnchecked mx my
  50         where
  51         check ::
  52          Map PathMod (Module src ss) ->
  53          Map PathMod (Module src ss) ->
  54          Maybe Error_Module
  55         check x' y' =
  56                 case Map.intersectionWith (,) x' y' of
  57                  xy | null xy -> Nothing
  58                  xy ->
  59                         let errs =
  60                                 Map.filter (not . null) $
  61                                 (<$> xy) $ \(a, b) ->
  62                                         inter a b byPrefix <>
  63                                         inter a b byInfix <>
  64                                         inter a b byPostfix in
  65                         case errs of
  66                          e | null e -> Nothing
  67                          e -> Just $ Error_Module_colliding_Term e
  68                 where
  69                 inter a b f = Map.keysSet $ Map.intersection (f a) (f b)
  70
  71 unionModulesUnchecked :: Modules src ss -> Modules src ss -> Modules src ss
  72 unionModulesUnchecked (Modules x) (Modules y) =
  73         Modules $ Map.unionWith (<>) x y
  74
  75 -- ** Type 'Error_Module'
  76 data Error_Module
  77  =   Error_Module_colliding_Term (Map PathMod (Set NameTe))
  78  |   Error_Module_ambiguous (Mod NameTe) (Map PathMod NameTe)
  79  |   Error_Module_missing PathMod
  80  |   Error_Module_missing_Term (Mod NameTe) -- FixyA
  81  deriving (Eq, Show)
  82
  83 -- ** Type 'Module'
  84 type Module src ss = ByFixity (ModuleFixy src ss Unifix)
  85                               (ModuleFixy src ss Infix)
  86                               (ModuleFixy src ss Unifix)
  87
  88 moduleEmpty :: Module src ss
  89 moduleEmpty = ByFixity
  90  { byPrefix  = mempty
  91  , byInfix   = mempty
  92  , byPostfix = mempty
  93  }
  94
  95 moduleWhere :: forall src ss. Source src => PathMod -> [DefTerm src ss] -> (PathMod, Module src ss)
  96 moduleWhere mod lst =
  97         (mod,) ByFixity
  98          { byInfix = mk $ \(n `WithFixity` fixy := t) ->
  99                 case fixy of
 100                  Fixity2 inf -> [(n, Tokenizer inf $ Token_Term . setSource (TermAVT t))]
 101                  _ -> []
 102          , byPrefix = mk $ \(n `WithFixity` fixy := t) ->
 103                 case fixy of
 104                  Fixity1 pre@Prefix{} -> [(n, Tokenizer pre $ Token_Term . setSource (TermAVT t))]
 105                  _ -> []
 106          , byPostfix = mk $ \(n `WithFixity` fixy := t) ->
 107                 case fixy of
 108                  Fixity1 post@Postfix{} -> [(n, Tokenizer post $ Token_Term . setSource (TermAVT t))]
 109                  _ -> []
 110          }
 111         where
 112         mk ::
 113          (DefTerm src ss -> [(NameTe, Tokenizer src ss fixy)]) ->
 114          Map NameTe (Tokenizer src ss fixy)
 115         mk = Map.fromList . (`foldMap` lst)
 116
 117 -- *** Type 'ModuleFixy'
 118 type ModuleFixy src ss fixy = Map NameTe (Tokenizer src ss fixy)
 119
 120 -- ** Type 'Tokenizer'
 121 data Tokenizer src ss fixy
 122  =   Tokenizer
 123  {   token_fixity :: fixy
 124  ,   token_term   :: src -> Token_Term src ss
 125  }
 126 instance (Source src, Eq fixy) => Eq (Tokenizer src ss fixy) where
 127         Tokenizer fx x == Tokenizer fy y = fx == fy && (x noSource) == (y noSource)
 128 instance Source src => Show (Tokenizer src ss fixy) where
 129         show (Tokenizer _fx x) = show (x noSource)
 130
 131 -- ** Type 'AST_Term'
 132 -- | /Abstract Syntax Tree/ of 'Token_Term'.
 133 type AST_Term src ss = BinTree (Token_Term src ss)
 134
 135 -- ** Type 'Token_Term'
 136 data Token_Term src ss
 137  =   Token_Term      (TermAVT src ss)
 138  |   Token_TermVT    (TermVT src ss '[])
 139  |   Token_Term_Abst src NameTe (AST_Type src) (AST_Term src ss)
 140  |   Token_Term_Var  src NameTe
 141  |   Token_Term_Let  src NameTe (AST_Term src ss) (AST_Term src ss)
 142  |   Token_Term_App  src
 143  -- deriving (Eq, Show)
 144 instance Source src => Eq (Token_Term src ss) where
 145         Token_Term   x == Token_Term   y = x == y
 146         Token_TermVT x == Token_TermVT y = x == y
 147         Token_Term_Abst _ nx ax rx == Token_Term_Abst _ ny ay ry = nx == ny && ax == ay && rx == ry
 148         Token_Term_Var _ x == Token_Term_Var _ y = x == y
 149         Token_Term_Let _ nx ax rx == Token_Term_Let _ ny ay ry = nx == ny && ax == ay && rx == ry
 150         Token_Term_App _ == Token_Term_App _ = True
 151         _ == _ = False
 152 instance Source src => Show (Token_Term src ss) where
 153         showsPrec p (Token_Term   x) =
 154                 showParen (p >= 10) $
 155                 showString "Token_Term" .
 156                 showChar ' ' . showsPrec 10 x
 157         showsPrec p (Token_TermVT x) =
 158                 showParen (p >= 10) $
 159                 showString "Token_TermVT" .
 160                 showChar ' ' . showsPrec 10 x
 161         showsPrec p (Token_Term_Abst _ n a r) =
 162                 showParen (p >= 10) $
 163                 showString "Token_Term_Abst" .
 164                 showChar ' ' . showsPrec 10 n .
 165                 showChar ' ' . showsPrec 10 a .
 166                 showChar ' ' . showsPrec 10 r
 167         showsPrec p (Token_Term_Var _ x) =
 168                 showParen (p >= 10) $
 169                 showString "Token_Term_Var" .
 170                 showChar ' ' . showsPrec 10 x
 171         showsPrec p (Token_Term_Let _ n a r) =
 172                 showParen (p >= 10) $
 173                 showString "Token_Term_Let" .
 174                 showChar ' ' . showsPrec 10 n .
 175                 showChar ' ' . showsPrec 10 a .
 176                 showChar ' ' . showsPrec 10 r
 177         showsPrec _p (Token_Term_App _) = showString "Token_Term_App"
 178
 179 -- ** Type 'NameTe'
 180 newtype NameTe = NameTe Name
 181  deriving (Eq, Ord, Show)
 182 instance IsString NameTe where
 183         fromString = NameTe . fromString
 184 instance NameOf NameTe where
 185         nameOf (NameTe n) = n
 186
 187 -- * Class 'ModulesInj'
 188 type ModulesInj  src ss
 189  =   ModulesInjR src ss ss
 190
 191 modulesInj ::
 192  forall src ss.
 193  ModulesInj src ss =>
 194  Either Error_Module (Modules src ss)
 195 modulesInj = modulesInjR @_ @_ @ss
 196
 197 -- ** Class 'ModulesInjR'
 198 class ModulesInjR src (ss::[*]) (rs::[*]) where
 199         modulesInjR :: Either Error_Module (Modules src ss)
 200 instance ModulesInjR src ss '[] where
 201         modulesInjR = Right $ Modules mempty
 202 instance
 203  ( ModuleFor src ss s
 204  , ModulesInjR src ss rs
 205  ) => ModulesInjR src ss (Proxy s ': rs) where
 206         modulesInjR = do
 207                 x <- modulesInjR @_ @_ @rs
 208                 let (n, m) = moduleFor @_ @_  @s
 209                 Modules (Map.singleton n m) `unionModules` x
 210
 211 -- * Type 'DefTerm'
 212 data DefTerm src ss
 213  = forall vs t.
 214  (:=) (WithFixity NameTe)
 215       (forall ts. Term src ss ts vs t)
 216
 217 -- | Lookup given 'Mod' 'NameTe' into the 'Infix' 'TermDef' of given 'Modules'.
 218 --
 219 -- NOTE: 'Token_Term_App' is returned for the space 'NameTe'.
 220 lookupDefTerm ::
 221  forall src ss fixy.
 222  Fixy (ModuleFixy src ss Unifix)
 223       (ModuleFixy src ss Infix)
 224       (ModuleFixy src ss Unifix)
 225       (ModuleFixy src ss fixy) ->
 226  Imports NameTe ->
 227  Mod NameTe ->
 228  Modules src ss ->
 229  Either Error_Module (Tokenizer src ss fixy)
 230 lookupDefTerm FixyInfix _is ([] `Mod` " ") _ms =
 231         Right $ Tokenizer
 232          { token_term   = Token_Term_App @src @ss
 233          , token_fixity = Infix (Just AssocL) 9
 234          }
 235 lookupDefTerm fixy imps mn@(m `Mod` n) (Modules mods) =
 236         let m' = m `fromMaybe` lookupImports fixy mn imps in
 237         maybe (Left $ Error_Module_missing m') Right (Map.lookup m' mods) >>=
 238         maybe (Left $ Error_Module_missing_Term mn) Right .
 239         Map.lookup n . selectByFixity fixy
 240
 241 -- | Delete given 'Mod' 'NameTe' into given 'Modules'.
 242 deleteDefTerm :: Mod NameTe -> Modules src ss -> Modules src ss
 243 deleteDefTerm (m `Mod` n) (Modules ms) = Modules $ Map.adjust del m ms
 244         where del mod = mod
 245                  { byPrefix  = Map.delete n $ byPrefix  mod
 246                  , byInfix   = Map.delete n $ byInfix   mod
 247                  , byPostfix = Map.delete n $ byPostfix mod
 248                  }
 249
 250 -- | Delete given 'Mod' 'NameTe' into 'byInfix's of given 'Modules'.
 251 deleteDefTermInfix :: Mod NameTe -> Modules src ss -> Modules src ss
 252 deleteDefTermInfix (m `Mod` n) (Modules ms) = Modules $ Map.adjust del m ms
 253         where del mod = mod{byInfix = Map.delete n $ byInfix mod}
 254
 255 -- | Delete given 'Mod' 'NameTe' into 'byPrefix's of given 'Modules'.
 256 deleteDefTermPrefix :: Mod NameTe -> Modules src ss -> Modules src ss
 257 deleteDefTermPrefix (m `Mod` n) (Modules ms) = Modules $ Map.adjust del m ms
 258         where del mod = mod{byPrefix = Map.delete n $ byPrefix mod}
 259
 260 -- | Delete given 'Mod' 'NameTe' into 'byPostfix's of given 'Modules'.
 261 deleteDefTermPostix :: Mod NameTe -> Modules src ss -> Modules src ss
 262 deleteDefTermPostix (m `Mod` n) (Modules ms) = Modules $ Map.adjust del m ms
 263         where del mod = mod{byPostfix = Map.delete n $ byPostfix mod}
 264
 265 insertDefTerm ::
 266  forall src ss.
 267  Source src =>
 268  Mod (DefTerm src ss) -> Modules src ss -> Modules src ss
 269 insertDefTerm (m `Mod` (n `WithFixity` fixy := t)) (Modules ms) =
 270         Modules $ Map.insert m (insertFixity ins fixy moduleEmpty) ms
 271         where
 272         ins :: fx -> ModuleFixy src ss fx -> ModuleFixy src ss fx
 273         ins fx = Map.insert n $ Tokenizer fx $ Token_Term . setSource (TermAVT t)
 274
 275 insertTermVT ::
 276  forall src ss.
 277  Source src =>
 278  Mod (TermVT src ss '[]) -> NameTe -> Fixity ->
 279  Modules src ss -> Modules src ss
 280 insertTermVT (m `Mod` t) n fixy (Modules ms) =
 281         Modules $ Map.insert m (insertFixity ins fixy moduleEmpty) ms
 282         where
 283         ins :: fx -> ModuleFixy src ss fx -> ModuleFixy src ss fx
 284         ins fx = Map.insert n $ Tokenizer fx $ Token_TermVT . setSource t
 285
 286 insertFixity ::
 287  (forall fx. fx -> ModuleFixy src ss fx -> ModuleFixy src ss fx) ->
 288  Fixity -> Module src ss -> Module src ss
 289 insertFixity ins fx mod =
 290         case fx of
 291          Fixity1 uni@Prefix{}  -> mod {byPrefix  = ins uni $ byPrefix  mod}
 292          Fixity2 inf@Infix{}   -> mod {byInfix   = ins inf $ byInfix   mod}
 293          Fixity1 uni@Postfix{} -> mod {byPostfix = ins uni $ byPostfix mod}