{-# LANGUAGE PolyKinds #-}
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 ()
-- | Read a 'Type' from an 'AST_Type', given its 'Vars'.
readType ::
- Inj_Source (KindK src) src =>
- Inj_Source (TypeVT src) src =>
- Inj_Source (AST_Type src) src =>
- Name2Type src ->
+ SourceInj (KindK src) src =>
+ SourceInj (TypeVT src) src =>
+ SourceInj (AST_Type src) 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
+readType ast | EVars vs <- readVars (EVars VarsZ) ast = do
+ TypeT ty <- readTyVars vs ast
Right $ TypeVT ty
-- | Read a 'Type' from an 'AST_Type', given its 'Vars'.
readTyVars ::
forall vs src.
- Inj_Source (KindK src) src =>
- Inj_Source (TypeVT src) src =>
- Inj_Source (AST_Type src) src =>
- Name2Type src ->
+ SourceInj (KindK src) src =>
+ SourceInj (TypeVT src) src =>
+ SourceInj (AST_Type src) 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))) =
+readTyVars vs (BinTree0 (Token_Type_Const (TypeTLen t))) =
+ Right $ t (lenVars vs)
+ -- readTyName is ms (sourceInj ast) (lenVars vs) name
+readTyVars vs (BinTree0 (Token_Type_Var (At src name))) =
case lookupVars name vs of
- Just (EVar v) -> Right $ TypeT $ TyVar (inj_Source ast) name v
+ Just (EVar v) -> Right $ TypeT $ TyVar src 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
+readTyVars vs ast@(ast_x `BinTree2` ast_y) = do
+ TypeT ty_x <- readTyVars vs ast_x
+ TypeT ty_y <- readTyVars 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
-
--- | Lookup a 'TyConst' or 'Type' synonym
--- associated with given 'NameTy' in given 'Name2Type',
--- building it for a @vs@ of given 'Len'.
-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
+ Right $ TypeT $ TyApp (sourceInj ast) ty_x ty_y
-- | Return the given 'EVars' augmented by the ones used in given 'AST_Type'.
readVars :: Source src => EVars src -> AST_Type src -> EVars src
readVars evs BinTree0{} = evs
readVars evs (BinTree2 x y) =
readVars (readVars evs x) y
-
--- * Type 'Name2Type'
-type Name2Type src = Map NameTy (TypeTLen src)
-
--- ** Type 'TypeTLen'
--- | Like 'TypeT', but needing a @(@'Len'@ vs)@ to be built.
---
--- Useful to build a 'Name2Type' 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 (TypeTLen src) where
- showsPrec p (TypeTLen t) = showsPrec p $ t LenZ
-
--- ** Class 'Inj_Name2Type'
--- | Derive a 'Name2Type' from the given type-level list
--- of 'Proxy'-fied /type constants/.
-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
-
--- * Type 'Error_Type'
-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