import Data.String (IsString(..))
import Data.Text (Text)
import Prelude hiding (mod, not, any)
+import qualified Data.Kind as K
import qualified Data.Map.Strict as Map
import Language.Symantic.Grammar
instance IsString NameMod where
fromString = NameMod . fromString
--- ** Type 'NameTe'
-newtype NameTe = NameTe Text
- deriving (Eq, Ord, Show)
-instance IsString NameTe where
- fromString = NameTe . fromString
-
-- * Class 'ModuleFor'
class ModuleFor src ss s where
moduleFor :: Proxy s -> (PathMod, Module src ss)
-- * Type 'Imports'
newtype Imports = Imports (Map PathMod (Map PathMod FilterImports))
+ deriving (Eq, Show)
type FilterImports = Maybe (Set NameTe)
-importModulesAs :: PathMod -> Modules src ss -> Imports
-importModulesAs as (Modules mods) = Imports $ Map.fromList [(as, Nothing <$ mods)]
+importQualifiedAs :: PathMod -> Modules src ss -> Imports
+importQualifiedAs as (Modules mods) = Imports $ Map.fromList [(as, Nothing <$ mods)]
-- * Type 'Modules'
newtype Modules src ss
= Modules
{ modules :: Map PathMod (Module src ss)
- }
+ } deriving (Eq, Show)
unionModules :: Modules src ss -> Modules src ss -> Either Error_Module (Modules src ss)
unionModules mx@(Modules x) my@(Modules y) =
{ module_prefix :: ModuleFixy src ss Unifix
, module_infix :: ModuleFixy src ss Infix
, module_postfix :: ModuleFixy src ss Unifix
- }
+ } deriving (Eq, Show)
module_fixity :: FixitySing fixy -> Module src ss -> ModuleFixy src ss fixy
module_fixity = \case
(mod,) Module
{ module_infix = mk $ \(n `WithFixity` fixy := t) ->
case fixy of
- Fixity2 inf -> [(n, Tokenizer inf $ Token_Term . setSource (TermVT_CF t))]
+ Fixity2 inf -> [(n, Tokenizer inf $ Token_Term . setSource (TermAVT t))]
_ -> []
, module_prefix = mk $ \(n `WithFixity` fixy := t) ->
case fixy of
- Fixity1 pre@Prefix{} -> [(n, Tokenizer pre $ Token_Term . setSource (TermVT_CF t))]
+ Fixity1 pre@Prefix{} -> [(n, Tokenizer pre $ Token_Term . setSource (TermAVT t))]
_ -> []
, module_postfix = mk $ \(n `WithFixity` fixy := t) ->
case fixy of
- Fixity1 post@Postfix{} -> [(n, Tokenizer post $ Token_Term . setSource (TermVT_CF t))]
+ Fixity1 post@Postfix{} -> [(n, Tokenizer post $ Token_Term . setSource (TermAVT t))]
_ -> []
}
where
-- *** Type 'ModuleFixy'
type ModuleFixy src ss fixy = Map NameTe (Tokenizer fixy src ss)
-deriving instance
- ( Show (Tokenizer Unifix src ss)
- , Show (Tokenizer Infix src ss)
- ) => Show (Module src ss)
instance Semigroup (Module src ss) where
x <> y =
Module
{ token_fixity :: fixy
, token_term :: src -> Token_Term src ss
}
+instance (Source src, Eq fixy) => Eq (Tokenizer fixy src ss) where
+ Tokenizer fx x == Tokenizer fy y = fx == fy && (x noSource) == (y noSource)
+instance Source src => Show (Tokenizer fixy src ss) where
+ show (Tokenizer _fx x) = show (x noSource)
-- ** Type 'Token_Term'
data Token_Term src ss
- = Token_Term (TermVT_CF src ss)
+ = Token_Term (TermAVT src ss)
+ | Token_TermVT (TermVT src ss '[])
| Token_Term_Abst src NameTe (AST_Type src) (AST_Term src ss)
| Token_Term_Var src NameTe
| Token_Term_Let src NameTe (AST_Term src ss) (AST_Term src ss)
| Token_Term_App src
- deriving (Eq, Show)
+ -- deriving (Eq, Show)
+instance Source src => Eq (Token_Term src ss) where
+ Token_Term x == Token_Term y = x == y
+ Token_TermVT x == Token_TermVT y = x == y
+ Token_Term_Abst _ nx ax rx == Token_Term_Abst _ ny ay ry = nx == ny && ax == ay && rx == ry
+ Token_Term_Var _ x == Token_Term_Var _ y = x == y
+ Token_Term_Let _ nx ax rx == Token_Term_Let _ ny ay ry = nx == ny && ax == ay && rx == ry
+ Token_Term_App _ == Token_Term_App _ = True
+ _ == _ = False
+instance Source src => Show (Token_Term src ss) where
+ showsPrec p (Token_Term x) =
+ showParen (p >= 10) $
+ showString "Token_Term" .
+ showChar ' ' . showsPrec 10 x
+ showsPrec p (Token_TermVT x) =
+ showParen (p >= 10) $
+ showString "Token_TermVT" .
+ showChar ' ' . showsPrec 10 x
+ showsPrec p (Token_Term_Abst _ n a r) =
+ showParen (p >= 10) $
+ showString "Token_Term_Abst" .
+ showChar ' ' . showsPrec 10 n .
+ showChar ' ' . showsPrec 10 a .
+ showChar ' ' . showsPrec 10 r
+ showsPrec p (Token_Term_Var _ x) =
+ showParen (p >= 10) $
+ showString "Token_Term_Var" .
+ showChar ' ' . showsPrec 10 x
+ showsPrec p (Token_Term_Let _ n a r) =
+ showParen (p >= 10) $
+ showString "Token_Term_Let" .
+ showChar ' ' . showsPrec 10 n .
+ showChar ' ' . showsPrec 10 a .
+ showChar ' ' . showsPrec 10 r
+ showsPrec _p (Token_Term_App _) = showString "Token_Term_App"
+
+-- ** Type 'NameTe'
+newtype NameTe = NameTe Text
+ deriving (Eq, Ord, Show)
+instance IsString NameTe where
+ fromString = NameTe . fromString
+
+-- * Type 'CtxTy'
+-- | /Typing context/
+-- accumulating at each /lambda abstraction/
+-- the 'Type' of the introduced variable.
+-- It is built top-down from the closest
+-- including /lambda abstraction/ to the farest.
+data CtxTy src (ts::[K.Type]) where
+ CtxTyZ :: CtxTy src '[]
+ CtxTyS :: NameTe
+ -> Type src '[] t
+ -> CtxTy src ts
+ -> CtxTy src (t ': ts)
+infixr 5 `CtxTyS`
+
+appendCtxTy
+ :: CtxTy src ts0
+ -> CtxTy src ts1
+ -> CtxTy src (ts0 ++ ts1)
+appendCtxTy CtxTyZ c = c
+appendCtxTy (CtxTyS n t c) c' = CtxTyS n t $ appendCtxTy c c'
+
+
-- ** Type 'AST_Term'
-- | /Abstract Syntax Tree/ of 'Token_Term'.
data DefTerm src ss
= forall vs t.
(:=) (WithFixity NameTe)
- (forall es. Term src ss es vs t)
+ (forall ts. Term src ss ts vs t)
-- | Lookup given 'Mod' 'NameTe' into the 'Infix' 'TermDef' of given 'Modules'.
--
Fixity2 inf@Infix{} -> mod {module_infix = ins inf $ module_infix mod}
Fixity1 uni@Postfix{} -> mod {module_postfix = ins uni $ module_postfix mod}
ins :: f -> ModuleFixy src ss f -> ModuleFixy src ss f
- ins f = Map.insert n $ Tokenizer f $ Token_Term . setSource (TermVT_CF t)
+ ins f = Map.insert n $ Tokenizer f $ Token_Term . setSource (TermAVT t)
+
+insertTermVT ::
+ forall src ss.
+ Source src =>
+ Mod (TermVT src ss '[]) -> NameTe -> Fixity ->
+ Modules src ss -> Modules src ss
+insertTermVT (m `Mod` t) n fixy (Modules ms) =
+ Modules $ Map.insert m (insFixy fixy moduleEmpty) ms
+ where
+ insFixy :: Fixity -> Module src ss -> Module src ss
+ insFixy f mod =
+ case f of
+ Fixity1 uni@Prefix{} -> mod {module_prefix = ins uni $ module_prefix mod}
+ Fixity2 inf@Infix{} -> mod {module_infix = ins inf $ module_infix mod}
+ Fixity1 uni@Postfix{} -> mod {module_postfix = ins uni $ module_postfix mod}
+ ins :: f -> ModuleFixy src ss f -> ModuleFixy src ss f
+ ins f = Map.insert n $ Tokenizer f $ Token_TermVT . setSource t
-- ** Type 'WithFixity'
data WithFixity a
sourcephile / git / haskell / symantic.git / blobdiff