symantic/Language/Symantic/Typing/Read.hs

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