+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
import Control.Applicative (Applicative(..))
import Data.List (foldl1')
-import Data.Proxy
+import Data.Map.Strict (Map)
+import Data.Maybe (fromMaybe)
+import Data.Semigroup (Semigroup(..))
import Data.String (IsString(..))
-import Data.Text (Text)
import qualified Data.Char as Char
-import qualified Data.Kind as K
+import qualified Data.Map.Strict as Map
import qualified Data.Text as Text
-import Language.Symantic.Parsing
+import Language.Symantic.Grammar as G
+import Language.Symantic.Typing.Kind
+import Language.Symantic.Typing.Variable
+import Language.Symantic.Typing.List
+import Language.Symantic.Typing.Module
+import Language.Symantic.Typing.Type
--- * Type 'TyName'
-newtype TyName = TyName Text
- deriving (Eq, Ord, Show)
-instance IsString TyName where
- fromString = TyName . fromString
+-- * Type 'AST_Type'
+-- | /Abstract Syntax Tree/ of 'Token_Type'.
+type AST_Type src = BinTree (Token_Type src)
+
+-- ** Type 'Token_Type'
+data Token_Type src
+ = Token_Type_Const (TypeTLen src)
+ | Token_Type_Var (At src NameVar)
+ -- deriving (Eq, Show)
+instance Source src => Eq (Token_Type src) where
+ Token_Type_Const (TypeTLen x) == Token_Type_Const (TypeTLen y) = x LenZ == y LenZ
+ Token_Type_Var (At _ x) == Token_Type_Var (At _ y) = x == y
+ _ == _ = False
+instance (Source src, Show (TypeT src '[])) => Show (Token_Type src) where
+ showsPrec p (Token_Type_Const x) =
+ showParen (p >= 10) $
+ showString "Token_Type_Const" .
+ showChar ' ' . showsPrec 10 x
+ showsPrec p (Token_Type_Var (At _ x)) =
+ showParen (p >= 10) $
+ showString "Token_Type_Var" .
+ showChar ' ' . showsPrec 10 x
+
+-- * Type 'ModulesTy'
+type ModulesTy src = Map (Mod NameTy) (TypeTLen src)
-{-
--- * Type 'Token_Type'
-type Token_Type = Type () '[] ()
--- data Token_Type
+-- ** Type 'TypeTLen'
+-- | Like 'TypeT', but needing a @(@'Len'@ vs)@ to be built.
+--
+-- Useful to build a 'ModulesTy' which can be used
+-- whatever will be the @(@'Len'@ vs)@ given to 'readTyVars'.
+newtype TypeTLen src = TypeTLen (forall vs. Len vs -> TypeT src vs)
+instance Source src => Eq (TypeTLen src) where
+ TypeTLen x == TypeTLen y = x LenZ == y LenZ
+instance (Source src, Show (TypeT src '[])) => Show (TypeTLen src) where
+ showsPrec p (TypeTLen t) = showsPrec p $ t LenZ
+typeTLen ::
+ forall c src.
+ Source src =>
+ Constable c =>
+ KindInjP (Ty_of_Type (K c)) =>
+ K c ~ Type_of_Ty (Ty_of_Type (K c)) =>
+ src ->
+ TypeTLen src
+typeTLen src =
+ TypeTLen $ \len -> TypeT $
+ TyConst src len $
+ constKiInj @(K c) @c $
+ kindInjP @(Ty_of_Type (K c)) noSource
+
+-- ** Class 'ModulesTyInj'
+-- | Derive a 'ModulesTy' from the given type-level list
+-- of 'Proxy'-fied /type constants/.
+class ModulesTyInj ts where
+ modulesTyInj :: Source src => ModulesTy src
+instance ModulesTyInj '[] where
+ modulesTyInj = Map.empty
instance
- ( Compile_TyNameR TyName cs rs
- , Inj_TyConst cs K.Type
- ) => Compile_TyNameR TyName cs (Proxy K.Type ': rs) where
- compile_TyNameR _rs src (TyName "Type") k = k (tySourced @K.Type src)
- compile_TyNameR _rs src raw k = compile_TyNameR (Proxy @rs) src raw k
-instance Show_TyConst cs => Show_TyConst (Proxy K.Type ': cs) where
- show_TyConst TyConstZ{} = "Type"
- show_TyConst (TyConstS c) = show_TyConst c
--}
+ ( KindInjP (Ty_of_Type (K c))
+ , K c ~ Type_of_Ty (Ty_of_Type (K c))
+ , Constable c
+ , ModulesTyInj ts
+ ) => ModulesTyInj (Proxy c ': ts) where
+ modulesTyInj =
+ Map.insert
+ (nameTyOf $ Proxy @c)
+ (typeTLen @c noSource) $
+ modulesTyInj @ts
--- * Type 'AST_Type'
-type AST_Type src = BinTree (EToken src '[Proxy K.Type])
-data instance TokenT ss (Proxy K.Type)
- = Token_Type_Name TyName
+-- * Class 'Gram_Mod'
+class
+ ( Gram_Char g
+ , Gram_Rule g
+ , Gram_Alt g
+ , Gram_Try g
+ , Gram_App g
+ , Gram_AltApp g
+ , Gram_RegL g
+ , Gram_CF g
+ , Gram_Comment g
+ , Gram_Op g
+ ) => Gram_Mod g where
+ g_PathMod :: CF g PathMod
+ g_PathMod = rule "PathMod" $
+ infixrG
+ (pure <$> g_NameMod)
+ (op <$ char '.')
+ where op = (<>)
+ g_NameMod :: CF g NameMod
+ g_NameMod = rule "NameMod" $
+ NameMod . Text.pack <$> identG
+ where
+ identG = (:) <$> headG <*> many (cfOf tailG)
+ headG = unicat $ Unicat Char.UppercaseLetter
+ tailG :: Terminal g Char
+ tailG =
+ unicat Unicat_Letter <+>
+ unicat Unicat_Number
-deriving instance Eq_Token ss => Eq (TokenT ss (Proxy K.Type))
-deriving instance Show_Token ss => Show (TokenT ss (Proxy K.Type))
+deriving instance Gram_Mod g => Gram_Mod (CF g)
+instance Gram_Mod EBNF
+instance Gram_Mod RuleEBNF
+
+-- * Class 'Gram_Type_Name'
+class
+ ( Gram_Char g
+ , Gram_Rule g
+ , Gram_Alt g
+ , Gram_Try g
+ , Gram_App g
+ , Gram_AltApp g
+ , Gram_RegL g
+ , Gram_CF g
+ , Gram_Comment g
+ , Gram_Op g
+ , Gram_Mod g
+ ) => Gram_Type_Name g where
+ g_ModNameTy :: CF g (Mod NameTy)
+ g_ModNameTy = rule "ModNameTy" $
+ lexeme $
+ g_ModNameTyId <+>
+ parens g_ModNameTyOp
+
+ g_ModNameTyId :: CF g (Mod NameTy)
+ g_ModNameTyId = rule "ModNameTyId" $
+ Mod
+ <$> option [] (try $ g_PathMod <* char '.')
+ <*> g_NameTyId
+ g_NameTyId :: CF g NameTy
+ g_NameTyId = rule "NameTyId" $
+ NameTy . Text.pack <$> identTyG
+ where
+ identTyG = (:) <$> headTyG <*> many (cfOf tailTyG)
+ headTyG = unicat $ Unicat Char.UppercaseLetter
+ tailTyG :: Terminal g Char
+ tailTyG =
+ unicat Unicat_Letter <+>
+ unicat Unicat_Number
+
+ g_ModNameTyOp :: CF g (Mod NameTy)
+ g_ModNameTyOp = rule "ModNameTyOp" $
+ Mod
+ <$> option [] (try $ g_PathMod <* char '.')
+ <*> g_NameTyOp
+ g_NameTyOp :: CF g NameTy
+ g_NameTyOp = rule "NameTyOp" $
+ NameTy . Text.pack <$> many (cfOf okG)
+ where
+ okG :: Terminal g Char
+ okG = choice (unicat <$>
+ [ Unicat_Symbol
+ , Unicat_Punctuation
+ , Unicat_Mark
+ ]) `but` koG
+ koG = choice (char <$> ['(', ')', '`', '\'', '[', ']'])
+
+deriving instance Gram_Type_Name g => Gram_Type_Name (CF g)
+instance Gram_Type_Name EBNF
+instance Gram_Type_Name RuleEBNF
-- * Class 'Gram_Type'
-- | Read an 'AST_Type' from a textual source.
class
- ( Alt g
- , Alter g
- , App g
- , Try g
- , Gram_CF g
+ ( Gram_Source src g
+ , Gram_Char g
, Gram_Rule g
- , Gram_Terminal g
- , Gram_Lexer g
+ , Gram_Alt g
+ , Gram_Try g
+ , Gram_App g
+ , Gram_AltApp g
+ , Gram_CF g
+ , Gram_Comment g
, Gram_Op g
- , Gram_Meta (Text_of_Source src) g
- , Inj_Source (Text_of_Source src) src
+ , Gram_Type_Name g
+ , Gram_Error (Error_Type src) g
+ , Gram_State (Imports NameTy, ModulesTy src) g
+ , Constable (->)
+ , Constable []
+ , Constable (,)
) => Gram_Type src g where
g_type :: CF g (AST_Type src)
- g_type = rule "type" $ g_type_fun
+ g_type = rule "Type" $ g_type_fun
g_type_fun :: CF g (AST_Type src)
- g_type_fun = rule "type_fun" $
- infixrG g_type_list (sourceG $ op <$ symbol "->")
- where op src = BinTree1 . BinTree1 (BinTree0 $ inj_EToken src $ Token_Type_Name "(->)")
+ g_type_fun = rule "TypeFun" $
+ infixrG g_type_list (source $ op <$ symbol "->")
+ where op src = BinTree2 . BinTree2 (BinTree0 $ Token_Type_Const $ typeTLen @(->) src)
-- TODO: maybe not harcoding g_type_list and g_type_tuple2
g_type_list :: CF g (AST_Type src)
- g_type_list = rule "type_list" $
- sourceG $ inside f
- (symbol "[") (optional (g_type)) (symbol "]")
+ g_type_list = rule "TypeList" $
+ source $ inside mk
+ (symbol "[") (optional g_type) (symbol "]")
(const <$> g_type_tuple2)
where
- n src = BinTree0 $ inj_EToken src $ Token_Type_Name "[]"
- f Nothing src = n src
- f (Just a) src = BinTree1 (n src) a
+ mk Nothing src = tok src
+ mk (Just a) src = BinTree2 (tok src) a
+ tok = BinTree0 . Token_Type_Const . typeTLen @[]
g_type_tuple2 :: CF g (AST_Type src)
- g_type_tuple2 = rule "type_tuple2" $
- try (parens (infixrG g_type (sourceG $ op <$ symbol ","))) <+> g_type_app
- where op src = BinTree1 . BinTree1 (BinTree0 $ inj_EToken src $ Token_Type_Name "(,)")
+ g_type_tuple2 = rule "TypeTuple2" $
+ try (parens (infixrG (g_type) (source $ op <$ symbol ","))) <+> (g_type_app)
+ where op src = BinTree2 . BinTree2 (BinTree0 $ Token_Type_Const $ typeTLen @(,) src)
g_type_app :: CF g (AST_Type src)
- g_type_app = rule "type_app" $
- foldl1' BinTree1 <$> some g_type_atom
+ g_type_app = rule "TypeApp" $
+ foldl1' BinTree2 <$> some (g_type_atom)
g_type_atom :: CF g (AST_Type src)
- g_type_atom = rule "type_atom" $
+ g_type_atom = rule "TypeAtom" $
try (parens g_type) <+>
- g_type_name <+>
- g_type_symbol
- g_type_name :: CF g (AST_Type src)
- g_type_name = rule "type_name" $
- sourceG $ lexeme $
- (\c cs src -> BinTree0 $ inj_EToken src $ Token_Type_Name $ fromString $ c:cs)
- <$> unicat (Unicat Char.UppercaseLetter)
+ g_type_const <+>
+ g_type_var
+ g_type_const :: CF g (AST_Type src)
+ g_type_const = rule "TypeConst" $
+ lexeme $ catch $ source $ getBefore $
+ (\n (impsTy, modsTy) src -> BinTree0 . Token_Type_Const <$> readTyName impsTy modsTy src n)
+ <$> g_ModNameTy
+ g_type_var :: CF g (AST_Type src)
+ g_type_var = rule "TypeVar" $
+ lexeme $ source $
+ (\n ns src -> BinTree0 $ Token_Type_Var $ At src $ fromString $ n:ns)
+ <$> unicat (Unicat Char.LowercaseLetter)
<*> many (choice $ unicat <$> [Unicat_Letter, Unicat_Number])
- g_type_symbol :: CF g (AST_Type src)
- g_type_symbol = rule "type_symbol" $
- sourceG $ (f <$>) $
- parens $ many $ cf_of_Terminal $ choice g_ok `but` choice g_ko
- where
- f s src = BinTree0 $ inj_EToken src $ (Token_Type_Name) $
- TyName $ Text.concat ["(", Text.pack s, ")"]
- g_ok = unicat <$>
- [ Unicat_Symbol
- , Unicat_Punctuation
- , Unicat_Mark
- ]
- g_ko = char <$> ['(', ')', '`']
deriving instance Gram_Type src g => Gram_Type src (CF g)
instance
- ( Inj_Source (Text_of_Source src) src
+ ( Gram_Source src EBNF
+ , Constable (->)
+ , Constable (,)
+ , Constable []
) => Gram_Type src EBNF
instance
- ( Inj_Source (Text_of_Source src) src
- ) => Gram_Type src RuleDef
+ ( Gram_Source src RuleEBNF
+ , Constable (->)
+ , Constable (,)
+ , Constable []
+ ) => Gram_Type src RuleEBNF
+
+-- | Lookup a 'TyConst' or 'Type' synonym
+-- associated with given 'NameTy' in given 'ModulesTy',
+-- building it for a @vs@ of given 'Len'.
+readTyName ::
+ Source src =>
+ Imports NameTy ->
+ ModulesTy src -> src -> Mod NameTy ->
+ Either (Error_Type src) (TypeTLen src)
+readTyName is ms src name@(m `Mod` n) =
+ let m' = fromMaybe m $ lookupImports FixyInfix name is in
+ case Map.lookup (m' `Mod` n) ms of
+ Just t -> Right t
+ Nothing -> Left $ Error_Type_Constant_unknown $ At src name
+
+-- * Type 'Error_Type'
+data Error_Type src
+ = Error_Type_Constant_unknown (At src (Mod NameTy))
+ | Error_Type_Con_Kind (Con_Kind src)
+ deriving (Eq, Show)
+instance ErrorInj (Error_Type src) (Error_Type src) where
+ errorInj = id
+instance ErrorInj (Con_Kind src) (Error_Type src) where
+ errorInj = Error_Type_Con_Kind
-- | List of the rules of 'Gram_Type'.
-gram_type :: Gram_Type src g => [CF g (AST_Type src)]
+gram_type :: Gram_Type () g => [CF g (AST_Type ())]
gram_type =
[ g_type
, g_type_fun
, g_type_tuple2
, g_type_app
, g_type_atom
- , g_type_name
- , g_type_symbol
+ , g_type_const
+ , g_type_var
+ -- , g_type_symbol
]