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