symantic/Language/Symantic/Typing/Read.hs

   1 {-# LANGUAGE PolyKinds #-}
   2 module Language.Symantic.Typing.Read where
   3
   4 import Data.Map.Strict (Map)
   5 import Data.Typeable
   6 import qualified Data.Map.Strict as Map
   7 import qualified Data.Text as Text
   8
   9 import Language.Symantic.Grammar
  10 import Language.Symantic.Typing.List
  11 import Language.Symantic.Typing.Kind
  12 import Language.Symantic.Typing.Type
  13 import Language.Symantic.Typing.Show ()
  14 import Language.Symantic.Typing.Grammar
  15 import Language.Symantic.Typing.Variable
  16
  17 -- | Read a 'Type' from an 'AST_Type', given its 'Vars'.
  18 readType ::
  19  Inj_Source (KindK src) src =>
  20  Inj_Source (TypeVT src) src =>
  21  Inj_Source (AST_Type src) src =>
  22  Name2Type src ->
  23  AST_Type src ->
  24  Either (Error_Type src) (TypeVT src)
  25 readType cs ast | EVars vs <- readVars (EVars VarsZ) ast = do
  26         TypeT ty <- readTyVars cs vs ast
  27         Right $ TypeVT ty
  28
  29 -- | Read a 'Type' from an 'AST_Type', given its 'Vars'.
  30 readTyVars ::
  31  forall vs src.
  32  Inj_Source (KindK src) src =>
  33  Inj_Source (TypeVT src) src =>
  34  Inj_Source (AST_Type src) src =>
  35  Name2Type src ->
  36  Vars src vs ->
  37  AST_Type src ->
  38  Either (Error_Type src) (TypeT src vs)
  39 readTyVars cs vs ast@(BinTree0 (Token_Type_Const (At _src name))) =
  40         readTyName cs (inj_Source ast) (lenVars vs) name
  41 readTyVars _cs vs ast@(BinTree0 (Token_Type_Var (At _src name))) =
  42         case lookupVars name vs of
  43          Just (EVar v) -> Right $ TypeT $ TyVar (inj_Source ast) name v
  44          Nothing -> error "[BUG] readTyVars: lookupVars failed"
  45 readTyVars cs vs ast@(ast_x `BinTree2` ast_y) = do
  46         TypeT ty_x <- readTyVars cs vs ast_x
  47         TypeT ty_y <- readTyVars cs vs ast_y
  48         when_KiFun (kindOf ty_x) $ \Refl ki_x_a _ki_x_b ->
  49                 when_EqKind ki_x_a (kindOf ty_y) $ \Refl ->
  50                         Right $ TypeT $ TyApp (inj_Source ast) ty_x ty_y
  51
  52 -- | Lookup a 'TyConst' or 'Type' synonym
  53 -- associated with given 'NameTy' in given 'Name2Type',
  54 -- building it for a @vs@ of given 'Len'.
  55 readTyName ::
  56  Source src =>
  57  Name2Type src -> src -> Len vs -> NameTy ->
  58  Either (Error_Type src) (TypeT src vs)
  59 readTyName cs src len name =
  60         case Map.lookup name cs of
  61          Just (Len2Type t) -> Right $ t len
  62          Nothing -> Left $ Error_Type_Constant_unknown $ At src name
  63
  64 -- | Return the given 'EVars' augmented by the ones used in given 'AST_Type'.
  65 readVars :: Source src => EVars src -> AST_Type src -> EVars src
  66 readVars evs@(EVars vs) (BinTree0 (Token_Type_Var (At _src name))) =
  67         case lookupVars name vs of
  68          Just{} -> evs
  69          Nothing -> do
  70                 let kv = KiType noSource
  71                 let vs' = VarsS name kv vs
  72                 EVars vs'
  73 readVars evs BinTree0{} = evs
  74 readVars evs (BinTree2 x y) =
  75         readVars (readVars evs x) y
  76
  77 -- * Type 'Name2Type'
  78 type Name2Type src = Map NameTy (Len2Type src)
  79
  80 -- ** Type 'Len2Type'
  81 -- | Like 'TypeT', but needing a @(@'Len'@ vs)@ to be built.
  82 --
  83 -- Useful to build a 'Name2Type' which can be used
  84 -- whatever will be the @(@'Len'@ vs)@ given to 'readTyVars'.
  85 data Len2Type src = Len2Type (forall vs. Len vs -> TypeT src vs)
  86 instance Source src => Show (Len2Type src) where
  87         showsPrec p (Len2Type t) = showsPrec p $ t LenZ
  88
  89 -- ** Class 'Inj_Name2Type'
  90 -- | Derive a 'Name2Type' from the given type-level list
  91 -- of 'Proxy'-fied /type constants/.
  92 class Inj_Name2Type cs where
  93         inj_Name2Type :: Source src => proxy cs -> Name2Type src
  94 instance Inj_Name2Type '[] where
  95         inj_Name2Type _cs = Map.empty
  96 instance
  97  ( Inj_KindP (Ty_of_Type (K c))
  98  , K c ~ Type_of_Ty (Ty_of_Type (K c))
  99  , Constable c
 100  , Inj_Name2Type cs
 101  ) => Inj_Name2Type (Proxy c ': cs) where
 102         inj_Name2Type _cs =
 103                 Map.insert
 104                  (NameTy $ Text.pack $ show $ typeRep (Proxy @c))
 105                  (Len2Type $ \len -> TypeT $ TyConst noSource len $
 106                         inj_ConstKi @(K c) @c $
 107                         inj_KindP (Proxy @(Ty_of_Type (K c))) noSource) $
 108                 inj_Name2Type (Proxy @cs)
 109
 110 -- * Type 'Error_Type'
 111 data Error_Type src
 112  =   Error_Type_Constant_unknown (At src NameTy)
 113  |   Error_Type_Con_Kind         (Con_Kind src)
 114  deriving (Eq, Show)
 115 instance Inj_Error (Error_Type src) (Error_Type src) where
 116         inj_Error = id
 117 instance Inj_Error (Con_Kind src) (Error_Type src) where
 118         inj_Error = Error_Type_Con_Kind