module Language.Symantic.Typing.Read where
import Data.Map.Strict (Map)
import Data.Typeable
import qualified Data.Map.Strict as Map
import qualified Data.Text as Text
import Language.Symantic.Grammar
import Language.Symantic.Typing.List
import Language.Symantic.Typing.Kind
import Language.Symantic.Typing.Type
import Language.Symantic.Typing.Show ()
import Language.Symantic.Typing.Grammar
import Language.Symantic.Typing.Variable
readType ::
Inj_Source (KindK src) src =>
Inj_Source (TypeVT src) src =>
Inj_Source (AST_Type src) src =>
Name2Type src ->
AST_Type src ->
Either (Error_Type src) (TypeVT src)
readType cs ast | EVars vs <- readVars (EVars VarsZ) ast = do
TypeT ty <- readTyVars cs vs ast
Right $ TypeVT ty
readTyVars ::
forall vs src.
Inj_Source (KindK src) src =>
Inj_Source (TypeVT src) src =>
Inj_Source (AST_Type src) src =>
Name2Type src ->
Vars src vs ->
AST_Type src ->
Either (Error_Type src) (TypeT src vs)
readTyVars cs vs ast@(BinTree0 (Token_Type_Const (At _src name))) =
readTyName cs (inj_Source ast) (lenVars vs) name
readTyVars _cs vs ast@(BinTree0 (Token_Type_Var (At _src name))) =
case lookupVars name vs of
Just (EVar v) -> Right $ TypeT $ TyVar (inj_Source ast) name v
Nothing -> error "[BUG] readTyVars: lookupVars failed"
readTyVars cs vs ast@(ast_x `BinTree2` ast_y) = do
TypeT ty_x <- readTyVars cs vs ast_x
TypeT ty_y <- readTyVars cs vs ast_y
when_KiFun (kindOf ty_x) $ \Refl ki_x_a _ki_x_b ->
when_EqKind ki_x_a (kindOf ty_y) $ \Refl ->
Right $ TypeT $ TyApp (inj_Source ast) ty_x ty_y
readTyName ::
Source src =>
Name2Type src -> src -> Len vs -> NameTy ->
Either (Error_Type src) (TypeT src vs)
readTyName cs src len name =
case Map.lookup name cs of
Just (TypeTLen t) -> Right $ t len
Nothing -> Left $ Error_Type_Constant_unknown $ At src name
readVars :: Source src => EVars src -> AST_Type src -> EVars src
readVars evs@(EVars vs) (BinTree0 (Token_Type_Var (At _src name))) =
case lookupVars name vs of
Just{} -> evs
Nothing -> do
let kv = KiType noSource
let vs' = VarsS name kv vs
EVars vs'
readVars evs BinTree0{} = evs
readVars evs (BinTree2 x y) =
readVars (readVars evs x) y
type Name2Type src = Map NameTy (TypeTLen src)
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 (TypeTLen src) where
showsPrec p (TypeTLen t) = showsPrec p $ t LenZ
class Inj_Name2Type cs where
inj_Name2Type :: Source src => Name2Type src
instance Inj_Name2Type '[] where
inj_Name2Type = Map.empty
instance
( Inj_KindP (Ty_of_Type (K c))
, K c ~ Type_of_Ty (Ty_of_Type (K c))
, Constable c
, Inj_Name2Type cs
) => Inj_Name2Type (Proxy c ': cs) where
inj_Name2Type =
Map.insert
(NameTy $ Text.pack $ show $ typeRep (Proxy @c))
(TypeTLen $ \len -> TypeT $ TyConst noSource len $
inj_ConstKi @(K c) @c $
inj_KindP @(Ty_of_Type (K c)) noSource) $
inj_Name2Type @cs
data Error_Type src
= Error_Type_Constant_unknown (At src NameTy)
| Error_Type_Con_Kind (Con_Kind src)
deriving (Eq, Show)
instance Inj_Error (Error_Type src) (Error_Type src) where
inj_Error = id
instance Inj_Error (Con_Kind src) (Error_Type src) where
inj_Error = Error_Type_Con_Kind