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.Map.Strict as Map
  19
  20 import Language.Symantic.Grammar
  21 import Language.Symantic.Typing
  22 import Language.Symantic.Compiling.Term
  23
  24 -- * Type 'Mod'
  25 data Mod a = Mod PathMod a
  26  deriving (Eq, Functor, Ord, Show)
  27
  28 -- ** Type 'PathMod'
  29 type PathMod = [NameMod]
  30
  31 -- ** Type 'NameMod'
  32 newtype NameMod = NameMod Text
  33  deriving (Eq, Ord, Show)
  34 instance IsString NameMod where
  35         fromString = NameMod . fromString
  36
  37 -- ** Type 'NameTe'
  38 newtype NameTe = NameTe Text
  39  deriving (Eq, Ord, Show)
  40 instance IsString NameTe where
  41         fromString = NameTe . fromString
  42
  43 -- * Class 'ModuleFor'
  44 class ModuleFor src ss s where
  45         moduleFor :: Proxy s -> (PathMod, Module src ss)
  46         moduleFor _s = ([], moduleEmpty)
  47
  48 -- * Type 'Imports'
  49 newtype Imports = Imports (Map PathMod (Map PathMod FilterImports))
  50 type FilterImports = Maybe (Set NameTe)
  51
  52 importModulesAs :: PathMod -> Modules src ss -> Imports
  53 importModulesAs as (Modules mods) = Imports $ Map.fromList [(as, Nothing <$ mods)]
  54
  55 -- * Type 'Modules'
  56 newtype Modules src ss
  57  =   Modules
  58  {   modules :: Map PathMod (Module src ss)
  59  }
  60
  61 unionModules :: Modules src ss -> Modules src ss -> Either Error_Module (Modules src ss)
  62 unionModules mx@(Modules x) my@(Modules y) =
  63         case check x y of
  64          Just err -> Left err
  65          Nothing  -> Right $ unionModulesUnchecked mx my
  66         where
  67         check ::
  68          Map PathMod (Module src ss) ->
  69          Map PathMod (Module src ss) ->
  70          Maybe Error_Module
  71         check x' y' =
  72                 case Map.intersectionWith (,) x' y' of
  73                  xy | null xy -> Nothing
  74                  xy ->
  75                         let errs =
  76                                 Map.filter (not . null) $
  77                                 (<$> xy) $ \(a, b) ->
  78                                         inter a b module_prefix <>
  79                                         inter a b module_infix <>
  80                                         inter a b module_postfix in
  81                         case errs of
  82                          e | null e -> Nothing
  83                          e -> Just $ Error_Module_colliding_Term e
  84                 where
  85                 inter a b f = Map.keysSet $ Map.intersection (f a) (f b)
  86
  87 unionModulesUnchecked :: Modules src ss -> Modules src ss -> Modules src ss
  88 unionModulesUnchecked (Modules x) (Modules y) =
  89         Modules $ Map.unionWith (<>) x y
  90
  91 -- ** Type 'Error_Module'
  92 data Error_Module
  93  =   Error_Module_colliding_Term (Map PathMod (Set NameTe))
  94  |   Error_Module_ambiguous (Mod NameTe) (Map PathMod NameTe)
  95  |   Error_Module_missing PathMod
  96  |   Error_Module_missing_Term (Mod NameTe)
  97  deriving (Eq, Show)
  98
  99 -- ** Type 'Module'
 100 data Module src ss
 101  =   Module
 102  {   module_prefix  :: ModuleFixy src ss Unifix
 103  ,   module_infix   :: ModuleFixy src ss Infix
 104  ,   module_postfix :: ModuleFixy src ss Unifix
 105  }
 106
 107 module_fixity :: FixitySing fixy -> Module src ss -> ModuleFixy src ss fixy
 108 module_fixity = \case
 109          FixitySing_Prefix  -> module_prefix
 110          FixitySing_Infix   -> module_infix
 111          FixitySing_Postfix -> module_postfix
 112
 113 moduleEmpty :: Module src ss
 114 moduleEmpty = Module
 115  { module_prefix  = mempty
 116  , module_infix   = mempty
 117  , module_postfix = mempty
 118  }
 119
 120 moduleWhere :: forall src ss. Source src => PathMod -> [DefTerm src ss] -> (PathMod, Module src ss)
 121 moduleWhere mod lst =
 122         (mod,) Module
 123          { module_infix = mk $ \(n `WithFixity` fixy := t) ->
 124                 case fixy of
 125                  Fixity2 inf -> [(n, Tokenizer inf $ Token_Term . setSource (TermVT_CF t))]
 126                  _ -> []
 127          , module_prefix = mk $ \(n `WithFixity` fixy := t) ->
 128                 case fixy of
 129                  Fixity1 pre@Prefix{} -> [(n, Tokenizer pre $ Token_Term . setSource (TermVT_CF t))]
 130                  _ -> []
 131          , module_postfix = mk $ \(n `WithFixity` fixy := t) ->
 132                 case fixy of
 133                  Fixity1 post@Postfix{} -> [(n, Tokenizer post $ Token_Term . setSource (TermVT_CF t))]
 134                  _ -> []
 135          }
 136         where
 137         mk ::
 138          (DefTerm src ss -> [(NameTe, Tokenizer fixy src ss)]) ->
 139          Map NameTe (Tokenizer fixy src ss)
 140         mk = Map.fromList . (`foldMap` lst)
 141
 142 -- *** Type 'ModuleFixy'
 143 type ModuleFixy src ss fixy = Map NameTe (Tokenizer fixy src ss)
 144
 145 deriving instance
 146  ( Show (Tokenizer Unifix src ss)
 147  , Show (Tokenizer Infix  src ss)
 148  ) => Show (Module src ss)
 149 instance Semigroup (Module src ss) where
 150         x <> y =
 151                 Module
 152                  { module_prefix  = module_prefix  x <> module_prefix  y
 153                  , module_infix   = module_infix   x <> module_infix   y
 154                  , module_postfix = module_postfix x <> module_postfix y
 155                  }
 156
 157 -- ** Type 'Tokenizer'
 158 data Tokenizer fixy src ss
 159  =   Tokenizer
 160  {   token_fixity :: fixy
 161  ,   token_term   :: src -> Token_Term src ss
 162  }
 163
 164 -- ** Type 'Token_Term'
 165 data Token_Term src ss
 166  =   Token_Term (TermVT_CF src ss)
 167  |   Token_Term_Abst src NameTe (AST_Type src) (AST_Term src ss)
 168  |   Token_Term_Var  src NameTe
 169  |   Token_Term_Let  src NameTe (AST_Term src ss) (AST_Term src ss)
 170  |   Token_Term_App  src
 171  deriving (Eq, Show)
 172
 173 -- ** Type 'AST_Term'
 174 -- | /Abstract Syntax Tree/ of 'Token_Term'.
 175 type AST_Term src ss = BinTree (Token_Term src ss)
 176
 177 -- * Class 'Inj_Modules'
 178 type Inj_Modules  src ss
 179  =   Inj_ModulesR src ss ss
 180
 181 inj_Modules :: forall src ss. Inj_Modules src ss => Either Error_Module (Modules src ss)
 182 inj_Modules = inj_ModulesR (Proxy @ss)
 183
 184 -- ** Class 'Inj_ModulesR'
 185 class Inj_ModulesR src (ss::[*]) (rs::[*]) where
 186         inj_ModulesR :: Proxy rs -> Either Error_Module (Modules src ss)
 187 instance Inj_ModulesR src ss '[] where
 188         inj_ModulesR _rs = Right $ Modules mempty
 189 instance
 190  ( ModuleFor src ss s
 191  , Inj_ModulesR src ss rs
 192  ) => Inj_ModulesR src ss (Proxy s ': rs) where
 193         inj_ModulesR _s = do
 194                 x <- inj_ModulesR (Proxy @rs)
 195                 let (n, m) = moduleFor (Proxy @s)
 196                 Modules (Map.singleton n m) `unionModules` x
 197
 198 -- * Type 'DefTerm'
 199 data DefTerm src ss
 200  = forall vs t.
 201  (:=) (WithFixity NameTe)
 202       (forall es. Term src ss es vs t)
 203
 204 -- | Lookup given 'Mod' 'NameTe' into the 'Infix' 'TermDef' of given 'Modules'.
 205 --
 206 -- NOTE: 'Token_Term_App' is returned for the space 'NameTe'.
 207 lookupDefTerm ::
 208  forall src ss fixy.
 209  FixitySing fixy ->
 210  Imports ->
 211  Mod NameTe ->
 212  Modules src ss ->
 213  Either Error_Module (Tokenizer fixy src ss)
 214 lookupDefTerm FixitySing_Infix _is ([] `Mod` " ") _ms =
 215         Right $ Tokenizer
 216          { token_term   = Token_Term_App @src @ss
 217          , token_fixity = Infix (Just AssocL) 9
 218          }
 219 lookupDefTerm fixy (Imports is) mn@(m `Mod` n) (Modules mods) =
 220         let mod_fixy = module_fixity fixy in
 221         case Map.lookup m is of
 222          Nothing ->
 223                 maybe (Left $ Error_Module_missing m) Right (Map.lookup m mods) >>=
 224                 maybe (Left $ Error_Module_missing_Term mn) Right .
 225                 Map.lookup n . mod_fixy
 226          Just ims ->
 227                 let look =
 228                  -- n matches amongst ims
 229                         (`Map.mapMaybeWithKey` ims) $ \im _ft -> -- TODO: filter NameTe
 230                                 Map.lookup im mods >>=
 231                                 Map.lookup n . mod_fixy >>=
 232                                 Just . Map.singleton n in
 233                 case Map.minView look of
 234                  Nothing -> Left $ Error_Module_missing_Term mn
 235                  Just (r, rs) | null rs -> Right $ snd $ Map.findMin r
 236                               | otherwise -> Left $ Error_Module_ambiguous mn $ fst . Map.findMin <$> look
 237
 238 -- | Delete given 'Mod' 'NameTe' into given 'Modules'.
 239 deleteDefTerm :: Mod NameTe -> Modules src ss -> Modules src ss
 240 deleteDefTerm (m `Mod` n) (Modules ms) = Modules $ Map.adjust del m ms
 241         where del mod = mod
 242                  { module_prefix  = Map.delete n $ module_prefix  mod
 243                  , module_infix   = Map.delete n $ module_infix   mod
 244                  , module_postfix = Map.delete n $ module_postfix mod
 245                  }
 246
 247 -- | Delete given 'Mod' 'NameTe' into 'module_infix's of given 'Modules'.
 248 deleteDefTermInfix :: Mod NameTe -> Modules src ss -> Modules src ss
 249 deleteDefTermInfix (m `Mod` n) (Modules ms) = Modules $ Map.adjust del m ms
 250         where del mod = mod{module_infix = Map.delete n $ module_infix mod}
 251
 252 -- | Delete given 'Mod' 'NameTe' into 'module_prefix's of given 'Modules'.
 253 deleteDefTermPrefix :: Mod NameTe -> Modules src ss -> Modules src ss
 254 deleteDefTermPrefix (m `Mod` n) (Modules ms) = Modules $ Map.adjust del m ms
 255         where del mod = mod{module_prefix = Map.delete n $ module_prefix mod}
 256
 257 -- | Delete given 'Mod' 'NameTe' into 'module_postfix's of given 'Modules'.
 258 deleteDefTermPostix :: Mod NameTe -> Modules src ss -> Modules src ss
 259 deleteDefTermPostix (m `Mod` n) (Modules ms) = Modules $ Map.adjust del m ms
 260         where del mod = mod{module_postfix = Map.delete n $ module_postfix mod}
 261
 262 insertDefTerm ::
 263  forall src ss.
 264  Source src =>
 265  Mod (DefTerm src ss) -> Modules src ss -> Modules src ss
 266 insertDefTerm (m `Mod` (n `WithFixity` fixy := t)) (Modules ms) =
 267         Modules $ Map.insert m (insFixy fixy moduleEmpty) ms
 268         where
 269         insFixy :: Fixity -> Module src ss -> Module src ss
 270         insFixy f mod =
 271                 case f of
 272                  Fixity1 uni@Prefix{}  -> mod {module_prefix  = ins uni $ module_prefix  mod}
 273                  Fixity2 inf@Infix{}   -> mod {module_infix   = ins inf $ module_infix   mod}
 274                  Fixity1 uni@Postfix{} -> mod {module_postfix = ins uni $ module_postfix mod}
 275         ins :: f -> ModuleFixy src ss f -> ModuleFixy src ss f
 276         ins f = Map.insert n $ Tokenizer f $ Token_Term . setSource (TermVT_CF t)
 277
 278 -- ** Type 'WithFixity'
 279 data WithFixity a
 280  =   WithFixity a Fixity
 281  deriving (Eq, Show)
 282 instance IsString (WithFixity NameTe) where
 283         fromString a = WithFixity (fromString a) (Fixity2 infixN5)
 284
 285 withInfix :: a -> Infix -> WithFixity a
 286 withInfix a inf = a `WithFixity` Fixity2 inf
 287 withInfixR :: a -> Precedence -> WithFixity a
 288 withInfixR a p = a `WithFixity` Fixity2 (infixR p)
 289 withInfixL :: a -> Precedence -> WithFixity a
 290 withInfixL a p = a `WithFixity` Fixity2 (infixL p)
 291 withInfixN :: a -> Precedence -> WithFixity a
 292 withInfixN a p = a `WithFixity` Fixity2 (infixN p)
 293 withInfixB :: a -> (Side, Precedence) -> WithFixity a
 294 withInfixB a (lr, p) = a `WithFixity` Fixity2 (infixB lr p)
 295 withPrefix :: a -> Precedence -> WithFixity a
 296 withPrefix a p = a `WithFixity` Fixity1 (Prefix p)
 297 withPostfix :: a -> Precedence -> WithFixity a
 298 withPostfix a p = a `WithFixity` Fixity1 (Postfix p)
 299
 300 -- ** Type 'FixitySing'
 301 data FixitySing fixy where
 302  FixitySing_Prefix  :: FixitySing Unifix
 303  FixitySing_Infix   :: FixitySing Infix
 304  FixitySing_Postfix :: FixitySing Unifix
 305 deriving instance Eq (FixitySing fixy)
 306 deriving instance Show (FixitySing fixy)