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 readTy ::
  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 readTy 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         read_TyConst 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' associated with given 'NameTy' in given 'Name2Type',
  53 -- building it for a @vs@ of given 'Len'.
  54 read_TyConst ::
  55  Source src =>
  56  Name2Type src -> src -> Len vs -> NameTy ->
  57  Either (Error_Type src) (TypeT src vs)
  58 read_TyConst cs src len name =
  59         case Map.lookup name cs of
  60          Just (Len2Type t) -> Right $ t len
  61          Nothing -> Left $ Error_Type_Constant_unknown $ At src name
  62
  63 -- | Return the given 'EVars' augmented by the ones used in given 'AST_Type'.
  64 readVars :: Source src => EVars src -> AST_Type src -> EVars src
  65 readVars evs@(EVars vs) (BinTree0 (Token_Type_Var (At _src name))) =
  66         case lookupVars name vs of
  67          Just{} -> evs
  68          Nothing -> do
  69                 let kv = KiType noSource
  70                 let vs' = VarsS name kv vs
  71                 EVars vs'
  72 readVars evs BinTree0{} = evs
  73 readVars evs (BinTree2 x y) =
  74         readVars (readVars evs x) y
  75
  76 -- * Type 'Name2Type'
  77 type Name2Type src = Map NameTy (Len2Type src)
  78
  79 -- ** Type 'Len2Type'
  80 -- | Like 'TypeT', but needing a @(@'Len'@ vs)@ to be built.
  81 --
  82 -- Useful to build a 'Name2Type' which can be used
  83 -- whatever will be the @(@'Len'@ vs)@ given to 'readTyVars'.
  84 data Len2Type src = Len2Type (forall vs. Len vs -> TypeT src vs)
  85 instance Source src => Show (Len2Type src) where
  86         showsPrec p (Len2Type t) = showsPrec p $ t LenZ
  87
  88 -- ** Class 'Inj_Name2Type'
  89 -- | Derive a 'Name2Type' from the given type-level list
  90 -- of 'Proxy'-fied /type constants/.
  91 class Inj_Name2Type cs where
  92         inj_Name2Type :: Source src => proxy cs -> Name2Type src
  93 instance Inj_Name2Type '[] where
  94         inj_Name2Type _cs = Map.empty
  95 instance
  96  ( Inj_KindP (Ty_of_Type (K c))
  97  , K c ~ Type_of_Ty (Ty_of_Type (K c))
  98  , Constable c
  99  , Inj_Name2Type cs
 100  ) => Inj_Name2Type (Proxy c ': cs) where
 101         inj_Name2Type _cs =
 102                 Map.insert
 103                  (NameTy $ Text.pack $ show $ typeRep (Proxy @c))
 104                  (Len2Type $ \len -> TypeT $ TyConst noSource len $
 105                         inj_ConstKi @(K c) @c $
 106                         inj_KindP (Proxy @(Ty_of_Type (K c))) noSource) $
 107                 inj_Name2Type (Proxy @cs)
 108
 109 -- * Type 'Error_Type'
 110 data Error_Type src
 111  =   Error_Type_Constant_unknown (At src NameTy)
 112  |   Error_Type_Con_Kind         (Con_Kind src)
 113  deriving (Eq, Show)
 114 instance Inj_Error (Error_Type src) (Error_Type src) where
 115         inj_Error = id
 116 instance Inj_Error (Con_Kind src) (Error_Type src) where
 117         inj_Error = Error_Type_Con_Kind