symantic/Language/Symantic/Typing/Compile.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.Compile where
   8
   9 import Data.Maybe (fromMaybe)
  10
  11 import Language.Symantic.Parsing
  12 import Language.Symantic.Typing.Kind
  13 import Language.Symantic.Typing.Constant
  14 import Language.Symantic.Typing.Type
  15 import Language.Symantic.Typing.Grammar
  16
  17 -- * Class 'CompileTyName'
  18 -- | Read a 'Type' from a 'TyName'.
  19 type CompileTyName cs = Compile_TyNameR cs cs
  20
  21 compileTyName
  22  :: forall src cs ret.
  23  (Compile_TyNameR cs cs, Source src)
  24  => src -> TyName
  25  -> (forall k c. Type src cs (c::k) -> Maybe ret)
  26  -> Maybe ret
  27 compileTyName = compile_TyNameR (Proxy @cs)
  28
  29 -- ** Class 'Compile_TyNameR'
  30 class Compile_TyNameR cs rs where
  31         compile_TyNameR
  32          :: Source src
  33          => Proxy rs -> src -> TyName
  34          -> (forall k c. Type src cs (c::k) -> Maybe ret)
  35          -> Maybe ret
  36
  37 instance Compile_TyNameR cs '[] where
  38         compile_TyNameR _rs _src _n _k = Nothing
  39
  40 -- TODO: move each of these to a dedicated module.
  41 instance
  42  ( Compile_TyNameR cs rs
  43  , Inj_TyConst cs Fractional
  44  ) => Compile_TyNameR  cs (Proxy Fractional ': rs) where
  45         compile_TyNameR _cs src (TyName "Fractional") k = k (tySourced @Fractional src)
  46         compile_TyNameR _rs src n k = compile_TyNameR (Proxy @rs) src n k
  47 instance
  48  ( Compile_TyNameR cs rs
  49  , Inj_TyConst cs []
  50  , Inj_TyConst cs Char
  51  ) => Compile_TyNameR cs (Proxy String ': rs) where
  52         compile_TyNameR _cs src (TyName "String") k = k (TyApp src (tySourced @[] src) (tySourced @Char src))
  53         compile_TyNameR _rs src n k = compile_TyNameR (Proxy @rs) src n k
  54
  55 -- * Type 'Error_Type'
  56 data Error_Type src
  57  =   Error_Type_Token_invalid    src
  58  |   Error_Type_Constant_unknown (At src TyName)
  59  |   Error_Type_Con_Kind         (Con_Kind src)
  60  deriving (Eq, Show)
  61
  62 instance Inj_Error (Error_Type src) (Error_Type src) where
  63         inj_Error = id
  64 instance Inj_Error (Con_Kind src) (Error_Type src) where
  65         inj_Error = inj_Error . Error_Type_Con_Kind
  66
  67 -- * Class 'CompileTy'
  68 -- | Read a 'Type' from an 'AST_Type'.
  69 class CompileTy cs where
  70         compileTy ::
  71          ( Inj_Error  (Error_Type src) err
  72          , Inj_Error  (Con_Kind   src) err
  73          , Inj_Source (EKind src)    src
  74          , Inj_Source (EType src cs) src
  75          , Inj_Source (AST_Type src) src
  76          ) => AST_Type src
  77          -> (forall k h. Type src cs (h::k) -> Either err ret)
  78          -> Either err ret
  79
  80 instance
  81  ( CompileTyName cs
  82  ) => CompileTy cs where
  83         compileTy
  84          :: forall src err ret.
  85          ( Inj_Error  (Error_Type src) err
  86          , Inj_Error  (Con_Kind   src) err
  87          , Inj_Source (EKind src)    src
  88          , Inj_Source (EType src cs) src
  89          , Inj_Source (AST_Type src) src
  90          ) => AST_Type src
  91          -> (forall k h. Type src cs (h::k) -> Either err ret)
  92          -> Either err ret
  93         compileTy ast@(BinTree0 (proj_EToken -> Just (_src, Token_Type_Name name))) k =
  94                 fromMaybe (Left $ inj_Error $ Error_Type_Constant_unknown @src $ At (inj_Source ast) name) $
  95                 compileTyName (inj_Source ast) name $ \typ -> Just $
  96                 k typ
  97         compileTy ast@(ast_x `BinTree1` ast_y) k =
  98                 compileTy @cs ast_x $ \ty_x ->
  99                 compileTy @cs ast_y $ \ty_y ->
 100                 if_KiArrow (kindTy ty_x) $ \Refl ki_x_a _ki_x_b ->
 101                 if_EqKind ki_x_a (kindTy ty_y) $ \Refl ->
 102                 k $ TyApp (inj_Source ast) ty_x ty_y
 103         compileTy ast _k = Left $ inj_Error $ Error_Type_Token_invalid @src $ inj_Source ast
 104          -- TODO: make this an "Oops, the impossible happened"?
 105
 106 compile_EType
 107  :: ( CompileTyName cs
 108     , Inj_Source (AST_Type src) src
 109     , Inj_Source (EType src cs) src
 110     , Inj_Source (EKind src)    src
 111     )
 112  => AST_Type src
 113  -> Either (Error_Type src) (EType src cs)
 114 compile_EType tok = compileTy tok (Right . EType)
 115
 116
 117 -- * Type 'Src'
 118 data Src txt cs is
 119  =   Src_Less
 120  |   Src_Text     txt
 121  |   Src_Token    (EToken (Src txt cs is) is)
 122  |   Src_AST_Term (AST_Term (Src txt cs is) is)
 123  |   Src_AST_Type (AST_Type (Src txt cs is))
 124  |   Src_Type     (EType  (Src txt cs is) cs)
 125  |   Src_Term
 126 deriving instance (Eq_Token (Src txt cs is) is, Eq txt) => Eq (Src txt cs is)
 127 deriving instance
 128  ( Show_Token (Src txt cs is) is
 129  , Show_TyConst cs
 130  , Show txt
 131  , Proj_TyConst cs (->)
 132  , Proj_TyConst cs (#>)
 133  , Source txt
 134  ) => Show (Src txt cs is)
 135 type instance Text_of_Source (Src txt cs is) = txt
 136
 137 instance Source (Src txt cs is) where
 138         sourceLess = Src_Less
 139 instance Inj_Source txt (Src txt cs is) where
 140         inj_Source = Src_Text
 141 instance Inj_Source (EToken (Src txt cs is) is) (Src txt cs is) where
 142         inj_Source = Src_Token
 143 instance Inj_Source (AST_Term (Src txt cs is) is) (Src txt cs is) where
 144         inj_Source = Src_AST_Term
 145 instance Inj_Source (AST_Type (Src txt cs is)) (Src txt cs is) where
 146         inj_Source = Src_AST_Type
 147 instance Inj_Source (EType (Src txt cs is) cs) (Src txt cs is) where
 148         inj_Source = Src_Type