symantic/Language/Symantic/Typing/Read.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
   3 {-# LANGUAGE PolyKinds #-}
   4 {-# LANGUAGE UndecidableInstances #-}
   5 {-# LANGUAGE ViewPatterns #-}
   6 {-# OPTIONS_GHC -fno-warn-orphans #-}
   7 module Language.Symantic.Typing.Read where
   8
   9 import Control.Applicative ((<|>))
  10 import Data.Maybe (fromMaybe)
  11
  12 import Language.Symantic.Parsing
  13 import Language.Symantic.Typing.Kind
  14 import Language.Symantic.Typing.Type
  15 import Language.Symantic.Typing.Show ()
  16 import Language.Symantic.Typing.Grammar
  17
  18 -- * Class 'Read_TyName'
  19 -- | Read a 'Type' from a 'TyName'.
  20 type Read_TyName cs = Read_TyNameR cs cs
  21
  22 read_TyName
  23  :: forall src ctx ss cs.
  24     Source src
  25  => Read_TyNameR cs cs
  26  => src -> TyName
  27  -> Maybe (EType src ctx ss cs)
  28 read_TyName = read_TyNameR (Proxy @cs)
  29
  30 -- ** Class 'Read_TyNameR'
  31 class Read_TyNameR cs rs where
  32         read_TyNameR
  33          :: Source src
  34          => Proxy rs -> src -> TyName
  35          -> Maybe (EType src ctx ss cs)
  36 instance Read_TyNameR cs '[] where
  37         read_TyNameR _rs _src _n = Nothing
  38 instance
  39  ( Read_TyNameC cs c
  40  , Read_TyNameR cs rs
  41  ) => Read_TyNameR cs (Proxy c ': rs) where
  42         read_TyNameR _rs src n =
  43                 read_TyNameC (Proxy @c)  src n <|>
  44                 read_TyNameR (Proxy @rs) src n
  45
  46 -- ** Class 'Read_TyNameC'
  47 class Read_TyNameC cs c where
  48         read_TyNameC
  49          :: Source src
  50          => Proxy c -> src -> TyName
  51          -> Maybe (EType src ctx ss cs)
  52
  53 -- * Type 'Error_Type'
  54 data Error_Type src
  55  =   Error_Type_Token_invalid    src
  56  |   Error_Type_Constant_unknown (At src TyName)
  57  |   Error_Type_Con_Kind         (Con_Kind src)
  58  deriving (Eq, Show)
  59
  60 instance Inj_Error (Error_Type src) (Error_Type src) where
  61         inj_Error = id
  62 instance Inj_Error (Con_Kind src) (Error_Type src) where
  63         inj_Error = inj_Error . Error_Type_Con_Kind
  64
  65 -- * Class 'Read_Type'
  66 -- | Read a 'Type' from an 'AST_Type'.
  67 class Read_Type cs where
  68         read_Type
  69          :: forall ctx ss src err ret.
  70             Inj_Error  (Error_Type src) err
  71          => Inj_Error  (Con_Kind   src) err
  72          => Inj_Source (EKind src) src
  73          => Inj_Source (EType src '[] ss cs) src
  74          => Inj_Source (AST_Type src) src
  75          => AST_Type src
  76          -> (forall k h. Type src ctx ss cs (h::k) -> Either err ret)
  77          -> Either err ret
  78
  79 instance Read_TyName cs => Read_Type cs where
  80         read_Type
  81          :: forall ctx ss src err ret.
  82             Inj_Error  (Error_Type src) err
  83          => Inj_Error  (Con_Kind   src) err
  84          => Inj_Source (EKind src) src
  85          => Inj_Source (EType src '[] ss cs) src
  86          => Inj_Source (AST_Type src) src
  87          => AST_Type src
  88          -> (forall k h. Type src ctx ss cs (h::k) -> Either err ret)
  89          -> Either err ret
  90         read_Type ast@(BinTree0 (proj_EToken -> Just (_src, Token_Type_Name name))) k =
  91                 fromMaybe (Left $ inj_Error $ Error_Type_Constant_unknown @src $ At (inj_Source ast) name) $ do
  92                         EType typ <- read_TyName (inj_Source ast) name
  93                         Just $ k typ
  94         read_Type ast@(ast_x `BinTree1` ast_y) k =
  95                 read_Type @cs @ctx @ss ast_x $ \ty_x ->
  96                 read_Type @cs @ctx @ss ast_y $ \ty_y ->
  97                 if_KiArrow (kindTy ty_x) $ \Refl ki_x_a _ki_x_b ->
  98                 if_EqKind ki_x_a (kindTy ty_y) $ \Refl ->
  99                 k $ TyApp (inj_Source ast) ty_x ty_y
 100         read_Type ast _k = Left $ inj_Error $ Error_Type_Token_invalid @src $ inj_Source ast
 101          -- TODO: make this an "Oops, the impossible happened"?
 102
 103 -- | Read a 'Type'.
 104 readTy
 105  :: Read_TyName cs
 106  => Inj_Source (AST_Type src) src
 107  => Inj_Source (EType src '[] ss cs) src
 108  => Inj_Source (EKind src) src
 109  => AST_Type src
 110  -> Either (Error_Type src) (EType src ctx ss cs)
 111 readTy tok = read_Type tok (Right . EType)