symantic/Language/Symantic/Compiling/Term.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE PolyKinds #-}
   4 {-# LANGUAGE TypeInType #-}
   5 {-# LANGUAGE UndecidableInstances #-}
   6 {-# OPTIONS_GHC -fno-warn-orphans #-}
   7 module Language.Symantic.Compiling.Term
   8  ( module Language.Symantic.Compiling.Term
   9  , module Language.Symantic.Compiling.Term.Grammar
  10  ) where
  11
  12 import Control.Arrow (left)
  13 import Data.Proxy (Proxy(..))
  14 import qualified Data.Kind as K
  15
  16 import Language.Symantic.Helper.Data.Type.List
  17 import Language.Symantic.Helper.Data.Type.Peano
  18 import Language.Symantic.Parsing
  19 import Language.Symantic.Typing
  20
  21 import Language.Symantic.Compiling.Term.Grammar
  22
  23 -- | The function 'Type' @(->)@,
  24 -- with an infix notation more readable.
  25 (~>) :: Source src
  26      => Inj_TyConst cs (->)
  27      => Type src ctx ss cs a
  28      -> Type src ctx ss cs b
  29      -> Type src ctx ss cs (a -> b)
  30 (~>) a b = (ty @(->) `tyApp` a) `tyApp` b
  31 infixr 5 ~>
  32
  33 -- * Type 'Inj_Sym'
  34 -- | Convenient type synonym wrapping 'Inj_SymP'
  35 -- applied on the correct 'Index'.
  36 type Inj_Sym ss s = Inj_SymP (Index ss (Proxy s)) ss s
  37
  38 -- | Inject a given /symantic/ @s@ into a list of them,
  39 -- by returning a function which given a 'TeSym' on @s@
  40 -- returns the same 'TeSym' on @ss@.
  41 inj_Sym :: forall s ss ctx h.
  42  Inj_Sym ss s
  43  => TeSym ctx '[Proxy s] h
  44  -> TeSym ctx ss h
  45 inj_Sym = inj_SymP (Proxy @(Index ss (Proxy s)))
  46
  47 -- ** Class 'Inj_SymP'
  48 class Inj_SymP p ss s where
  49         inj_SymP :: Proxy p -> TeSym ctx '[Proxy s] h -> TeSym ctx ss h
  50 instance Inj_SymP Zero (Proxy s ': ss) (s::k) where
  51         inj_SymP _ = \(TeSym te) -> TeSym te
  52 instance Inj_SymP p ss s => Inj_SymP (Succ p) (not_s ': ss) s where
  53         inj_SymP _p = \(te::TeSym ctx '[Proxy s] h) ->
  54                 case inj_SymP (Proxy @p) te :: TeSym ctx ss h of
  55                  TeSym te' -> TeSym te'
  56
  57 -- * Type 'CtxTy'
  58 -- | GADT for a /typing context/:
  59 -- accumulating at each /lambda abstraction/
  60 -- the 'Type' of the introduced variable.
  61 data CtxTy src ss (cs::[K.Type]) (hs::[K.Type]) where
  62         CtxTyZ :: CtxTy src ss cs '[]
  63         CtxTyS :: TeName
  64                -> Type src ctx ss cs h
  65                -> CtxTy src ss cs hs
  66                -> CtxTy src ss cs (h ': hs)
  67 infixr 5 `CtxTyS`
  68
  69 appendCtxTy
  70  :: CtxTy src ss cs hs0
  71  -> CtxTy src ss cs hs1
  72  -> CtxTy src ss cs (hs0 ++ hs1)
  73 appendCtxTy CtxTyZ c          = c
  74 appendCtxTy (CtxTyS n t c) c' = CtxTyS n t $ appendCtxTy c c'
  75
  76 -- * Class 'Compile'
  77 class Compile cs ss where
  78         compile :: Source src
  79                 => Inj_Source (EType src '[] ss cs) src
  80                 => Inj_Source (EKind src) src
  81                 => Inj_Source (AST_Type src) src
  82                 => AST_Term src ss
  83                 -> CtxTy src ss cs ctx
  84                 -- ^ The bound variables in scope and their types:
  85                 -- built top-down in the heterogeneous list @ctx@,
  86                 -- from the closest including /lambda abstraction/ to the farest.
  87                 -> Either (Error_Term src ss cs)
  88                           (KTerm src ctx ss cs)
  89 instance
  90  ( Show_TyConst cs
  91  , Inj_TyConst  cs (->)
  92  , Proj_TyConst cs (->)
  93  , Proj_TyConst cs (#>)
  94  , Proj_TyCon   cs
  95  , Read_TyName  cs
  96  , CompileR ss cs ss
  97  ) => Compile cs ss where
  98         compile :: forall src ctx. Source src
  99                 => Inj_Source (EType src '[] ss cs) src
 100                 => Inj_Source (EKind src) src
 101                 => Inj_Source (AST_Type src) src
 102                 => AST_Term src ss
 103                 -> CtxTy src ss cs ctx
 104                 -> Either (Error_Term src ss cs)
 105                           (KTerm src ctx ss cs)
 106         compile tr ctx = do
 107                 ts <- go `traverse` tr
 108                 (_vs, Just m) <- inj_Error `left` evalTreeKT ts
 109                 Right $ polyTy `bindKT` m
 110                 where
 111                 go :: Token_Term src ss
 112                    -> Either (Error_Term src ss cs)
 113                              (KTerm src ctx ss cs)
 114                 go (Token_Term (EToken _src tok)) = Right $ compileR tok
 115                 go (Token_Term_Abst _src name_arg tok_ty_arg tok_body) =
 116                         read_Type tok_ty_arg $ \(ty_arg::Type src ctx ss cs h) ->
 117                         if_EqKind (inj_Kind @K.Type) (kindTy ty_arg) $ \Refl -> do
 118                         KT (Term ty_res (TeSym res)) <- -- FIXME: pattern failure
 119                                 compile tok_body (CtxTyS name_arg ty_arg ctx)
 120                         Right $ KT $ Term (ty_arg ~> unTerms ty_res) $
 121                                 TeSym $ \c -> lam $ \arg -> res (arg `CtxTeS` c)
 122                 go (Token_Term_Var _src nam) = lookupTeVar nam ctx
 123                         where
 124                         lookupTeVar :: forall ctxTy.
 125                             TeName
 126                          -> CtxTy src ss cs ctxTy
 127                          -> Either (Error_Term src ss cs)
 128                                    (KTerm src ctxTy ss cs)
 129                         lookupTeVar name ctxTy =
 130                                 case ctxTy of
 131                                  CtxTyZ -> Left $ Error_Term_unbound name
 132                                  CtxTyS n typ _ | n == name ->
 133                                         Right $ KT $ Term (unTerms typ) $
 134                                                 TeSym $ \(te `CtxTeS` _) -> te
 135                                  CtxTyS _n _typ ctxTy' -> do
 136                                         KT t <- lookupTeVar name ctxTy'
 137                                         case t of
 138                                          Term typ (TeSym te) ->
 139                                                 Right $ KT $ Term (unTerms typ) $ -- TODO: optimize?
 140                                                         TeSym $ \(_ `CtxTeS` c) -> te c
 141                                          _ -> error "[BUG] lookupTeVar: impossible case"
 142                 go (Token_Term_Let _src name tok_bound tok_body) = do
 143                         KT (Term ty_bound (TeSym bound)) <- -- FIXME: pattern failure
 144                                 compile tok_bound ctx
 145                         KT (Term ty_res   (TeSym res))   <- -- FIXME: pattern failure
 146                                 compile tok_body (CtxTyS name ty_bound ctx)
 147                         Right $ KT $ Term (unTerms ty_res) $
 148                                 TeSym $ \c -> let_ (bound c) $ \arg -> res (arg `CtxTeS` c)
 149                 go (Token_Term_App _ctx) =
 150                         Right $
 151                                 tyQuant "a" $ \a ->
 152                                 tyQuant "b" $ \b ->
 153                                 KT $ Term ((a ~> b) ~> a ~> b) $
 154                                 TeSym $ \_c -> apply
 155
 156 -- ** Class 'CompileR'
 157 -- | Intermediate type class to construct an instance of 'Compile'
 158 -- from many instances of 'CompileS', one for each item of @ss@.
 159 class CompileR (ss::[K.Type]) (cs::[K.Type]) (ssR::[K.Type]) where
 160         compileR :: Source src
 161                  => Inj_Source (EType src '[] ss cs) src
 162                  => Inj_Source (EKind src) src
 163                  => Inj_Source (AST_Type src) src
 164                  => TokenR ss ssR s
 165                  -> KTerm src ctx ss cs
 166 -- | Recurse into the given 'TokenR'
 167 -- to call the 'compileS' instance associated
 168 -- to the 'TokenT' it contains.
 169 instance
 170  ( CompileS ss cs s
 171  , CompileR ss cs (r ': ssR)
 172  ) => CompileR ss cs (Proxy s ': r ': ssR) where
 173         compileR = \case
 174          TokenZ to -> compileS to
 175          TokenS to -> compileR to
 176 -- | End the recursion.
 177 instance
 178  CompileS ss cs s =>
 179  CompileR ss cs (Proxy s ': '[]) where
 180         compileR (TokenZ to) = compileS to
 181         compileR TokenS{}    = error "[BUG] compileR: TokenS is impossible here"
 182
 183 -- ** Class 'CompileS'
 184 -- | Handle the work of 'Compile' for a given /symantic/ @s@.
 185 class CompileS (ss::[K.Type]) (cs::[K.Type]) (s::ks) where
 186         compileS :: Source src
 187                  => Inj_Source (EType src '[] ss cs) src
 188                  => Inj_Source (EKind src) src
 189                  => Inj_Source (AST_Type src) src
 190                  => TokenT ss (Proxy s)
 191                  -> KTerm src ctx ss cs
 192
 193 instance Inj_Error (Error_Type src) (Error_Term src ss cs) where
 194         inj_Error = Error_Term_Typing
 195 instance Inj_Error (Con_Kind src) (Error_Term src ss cs) where
 196         inj_Error = Error_Term_Typing . Error_Type_Con_Kind
 197 instance Inj_Error (Error_TeApp src ss cs) (Error_Term src ss cs) where
 198         inj_Error = Error_Term_TeApp
 199
 200 -- * Type 'Error_Term'
 201 data Error_Term src ss cs
 202  =   Error_Term_unbound TeName
 203  |   Error_Term_Typing (Error_Type src)
 204  |   Error_Term_TeApp (Error_TeApp src ss cs)
 205  |   Error_Term_Con_Type (Con_Type src '[] ss cs)
 206  {-    Error_Term_Con_Kind (Con_Kind src) -}
 207 deriving instance
 208  ( Eq src
 209  , Eq_Token ss
 210  , Inj_Source (EType src '[] ss cs) src
 211  ) => Eq (Error_Term src ss cs)
 212 deriving instance
 213  ( Show src
 214  , Show_Token ss
 215  , Show_TyConst cs
 216  , Fixity_TyConst cs
 217  ) => Show (Error_Term src ss cs)
 218
 219
 220 -- * Type 'TyConsts'
 221 type TyConsts ss = Nub (TyConstsR ss)
 222
 223 -- * Type family 'TyConstsR'
 224 type family TyConstsR (ss::[K.Type]) where
 225         TyConstsR '[]       = '[]
 226         TyConstsR (s ': ss) = TyConstsS s ++ TyConstsR ss
 227
 228 -- * Type family 'TyConstsS'
 229 type family TyConstsS (s:: K.Type) :: [K.Type]
 230
 231 -- * Type family 'TyConsts_imported_by'
 232 -- | Return the /type constant/s that a given /type constant/
 233 -- wants to be part of the final list of /type constants/.
 234 type family TyConsts_imported_by (c:: K.Type) :: [K.Type]
 235
 236
 237
 238
 239
 240 -- * Type 'Src'
 241 data Src txt ss cs
 242  =   Src_Less
 243  |   Src_Text     txt
 244  |   Src_Token    (EToken   (Src txt ss cs) ss)
 245  |   Src_AST_Term (AST_Term (Src txt ss cs) ss)
 246  |   Src_AST_Type (AST_Type (Src txt ss cs))
 247  |   Src_Kind     (EKind    (Src txt ss cs))
 248  |   Src_Type     (EType    (Src txt ss cs) '[] ss cs)
 249  |   Src_Term
 250 deriving instance (Eq_Token ss, Eq txt) => Eq (Src txt ss cs)
 251 deriving instance
 252  ( Show_Token ss
 253  , Show_TyConst cs
 254  , Show txt
 255  , Fixity_TyConst cs
 256  ) => Show (Src txt ss cs)
 257 type instance Text_of_Source (Src txt ss cs) = txt
 258
 259 instance Source (Src txt ss cs) where
 260         sourceLess = Src_Less
 261 instance Inj_Source txt (Src txt ss cs) where
 262         inj_Source = Src_Text
 263 instance Inj_Source (EToken (Src txt ss cs) ss) (Src txt ss cs) where
 264         inj_Source = Src_Token
 265 instance Inj_Source (AST_Term (Src txt ss cs) ss) (Src txt ss cs) where
 266         inj_Source = Src_AST_Term
 267 instance Inj_Source (AST_Type (Src txt ss cs)) (Src txt ss cs) where
 268         inj_Source = Src_AST_Type
 269 instance Inj_Source (EKind (Src txt ss cs)) (Src txt ss cs) where
 270         inj_Source = Src_Kind
 271 instance Inj_Source (EType (Src txt ss cs) '[] ss cs) (Src txt ss cs) where
 272         inj_Source = Src_Type