symantic/Language/Symantic/Typing/Term.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 module Language.Symantic.Typing.Term where
   4
   5 import Control.Arrow (left)
   6 import Data.List (foldl')
   7 import qualified Control.Monad.Trans.State.Strict as SS
   8 import qualified Data.Map.Strict as Map
   9
  10 import Language.Symantic.Helper.Data.Type.Equality
  11 import Language.Symantic.Parsing
  12 import Language.Symantic.Typing.Kind
  13 import Language.Symantic.Typing.Constant
  14 import Language.Symantic.Typing.Constraint
  15 import Language.Symantic.Typing.Type
  16 import Language.Symantic.Typing.Show ()
  17 import Language.Symantic.Typing.Quantification
  18
  19 -- * Type 'Error_TeApp'
  20 data Error_TeApp src ss cs
  21  =   Error_TeApp_FunArg (EType src '[] ss cs)
  22      -- ^ Cannot get the expected 'Type' of the argument of the function.
  23  |   Error_TeApp_MGU (Error_MGU src ss cs)
  24      -- ^ Cannot unify the expected 'Type' of the argument of the function,
  25      -- with the 'Type' of the argument.
  26  |   Error_TeApp_Term_missing (EType src '[] ss cs)
  27      -- ^ Cannot find a 'TeTerm', either in the function or in the argument.
  28  {-
  29  |   Error_TeApp_TyQuant_remaining (EType src ctx ss cs)
  30      -- ^ A 'TyQuant' remains to be instantiated.
  31  -}
  32  |   Error_TeApp_Term_not_applicable (EType src '[] ss cs)
  33  |   Error_TeApp_Type_mismatch (EType src '[] ss cs) (EType src '[] ss cs)
  34
  35 deriving instance
  36  ( Eq src
  37  , Eq_Token ss
  38  , Inj_Source (EType src '[] ss cs) src
  39  ) => Eq (Error_TeApp src ss cs)
  40 deriving instance
  41  ( Show src
  42  , Show_TyConst cs
  43  , Fixity_TyConst cs
  44  ) => Show (Error_TeApp src ss cs)
  45
  46 instance Inj_Error (Error_TeApp src ss cs) (Error_TeApp src ss cs) where
  47         inj_Error = id
  48 instance Inj_Error (Error_MGU src ss cs) (Error_TeApp src ss cs) where
  49         inj_Error = Error_TeApp_MGU
  50
  51 -- | Return the next free 'Var' considering all the 'KType's of given 'BinTree'.
  52 freeTyVarTreeKT :: BinTree (KType src ctx ss cs k) -> Var
  53 freeTyVarTreeKT t = foldr max 0 $ ofKT freeTyVar <$> t
  54
  55 -- | Term application: apply second given 'KTerm' to the first,
  56 -- applying embedded 'TeSym's if possible.
  57 teApp
  58  :: forall src ctx ss cs.
  59     Proj_TyConst cs (->)
  60  => Proj_TyConst cs (#>)
  61  => Proj_TyCon cs
  62  => Inj_Source (EType src '[] ss cs) src
  63  => Show_TyConst cs
  64  => KTerm src ctx ss cs
  65  -> KTerm src ctx ss cs
  66  -> Either (Error_TeApp src ss cs) (KTerm src ctx ss cs)
  67 teApp (KT fun) (KT arg) = go fun arg
  68         where
  69         go
  70          :: Term src ctx ss cs f
  71          -> Term src ctx ss cs a
  72          -> Either (Error_TeApp src ss cs)
  73                    (KTerm src ctx ss cs)
  74         go f@TyConst{} _a = Left $ Error_TeApp_Term_missing (EType $ unCtxTe f `source` EType (unCtxTe fun))
  75         go (TyApp _sb (TyApp _sa (TyConst _src' a2b) a2b_a) a2b_b) a
  76          | Just KRefl <- proj_TyConstKi @_ @(->) a2b
  77          = case eqTy a2b_a a of
  78                  Just Refl -> Right $ KT a2b_b
  79                  Nothing -> Left $ Error_TeApp_Type_mismatch (EType $ unCtxTe a2b_a) (EType $ unCtxTe a)
  80         go f@TyApp{} _a = Left $ Error_TeApp_Term_not_applicable (EType $ unCtxTe f `source` EType (unCtxTe fun))
  81         go f@TyVar{} _a = Left $ Error_TeApp_Term_missing (EType $ unCtxTe f `source` EType (unCtxTe fun))
  82         go t@(TyQuant src n kv f) a =
  83                 let v = freeTyVar t in
  84                 case f $ TyVar src kv v of
  85                  KT f' -> bindKT (polyTyVar n kv v) <$> go f' a
  86         go (Term (TyApp _sb (TyApp _sa (TyConst _src' a2b) a2b_a) a2b_b) (TeSym te_fun)) a
  87          | Just KRefl <- proj_TyConstKi @_ @(->) a2b
  88          = case a of
  89                  Term a' (TeSym te_arg) ->
  90                         case eqTy a2b_a a' of
  91                          Just Refl -> Right $ KT $ Term a2b_b (TeSym $ \ctx -> te_fun ctx `app` te_arg ctx)
  92                          Nothing -> Left $ Error_TeApp_Type_mismatch (EType $ unCtxTe a2b_a) (EType $ unCtxTe a')
  93                  _ -> Left $ Error_TeApp_Term_missing (EType $ unCtxTe a `source` EType (unCtxTe arg))
  94         go (Term x _te) _a = Left $ Error_TeApp_Term_not_applicable (EType $ unCtxTe x `source` EType (unCtxTe fun))
  95
  96 -- | Monomorphize a 'BinTree' of 'KT'.
  97 monoTreeKT :: BinTree (KT src ctx ss cs k) -> BinTree (KT src ctx ss cs k)
  98 monoTreeKT t =
  99         (`SS.evalState` freeTyVarTreeKT t) $
 100         traverse (monoTy `ofKT`) t
 101
 102 -- | Fold given 'BinTree' of 'KTerm' in order to compute
 103 -- a resulting 'KTerm', if possible.
 104 evalTreeKT
 105  :: Inj_Source (EType src '[] ss cs) src
 106  => Show_TyConst cs
 107  => Proj_TyConst cs (->)
 108  => Proj_TyConst cs (#>)
 109  => Proj_TyCon cs
 110  => BinTree (KTerm src ctx ss cs)
 111  -> Either (Error_TeApp src ss cs)
 112            ( MapTyVar src ctx ss cs
 113            , Maybe (KTerm src ctx ss cs) )
 114 evalTreeKT t =
 115         foldl' (\acc (KT arg) -> do
 116                 (mgu, may_fun) <- acc
 117                 case may_fun of
 118                  Nothing -> Right (mgu, Just (KT arg))
 119                  Just (KT fun) ->
 120                         case unTyFun fun of
 121                          Nothing -> inj_Error $ Error_TeApp_FunArg $ EType $ unCtxTe fun
 122                          Just (KT fun_arg, KT _fun_res) -> do
 123                                 mgu' <- inj_Error `left` mguTy mgu fun_arg arg
 124                                 let fun' = substTyVar mgu' fun
 125                                 let arg' = substTyVar mgu' arg
 126                                 KT res <- teApp fun' arg'
 127                                 Right (mgu', Just (KT res)))
 128          (Right (Map.empty, Nothing)) $
 129         monoTreeKT t
 130
 131 evalTe
 132  :: Source src
 133  => Proj_TyCon cs
 134  => Type src ctx ss cs h
 135  -> Maybe (TeSym ctx ss h)
 136 evalTe (Term _ty te) = Just te
 137 evalTe TyQuant{}     = Nothing
 138 evalTe TyConst{}     = Nothing
 139 evalTe TyVar{}       = Nothing
 140 evalTe TyFam{}       = Nothing
 141 evalTe TyApp{}       = Nothing