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  , Fixity_TyConst cs
  41  ) => Show (Error_TeApp src cs)
  42
  43 instance Inj_Error (Error_TeApp src cs) (Error_TeApp src cs) where
  44         inj_Error = id
  45 instance Inj_Error (Error_MGU src cs) (Error_TeApp src cs) where
  46         inj_Error = Error_TeApp_MGU
  47
  48 -- | Return the next free 'Var' considering all the 'KType's of given 'BinTree'.
  49 freeTyVarTreeKT :: BinTree (KType src cs k) -> Var
  50 freeTyVarTreeKT t = foldr max 0 $ ofKT freeTyVar <$> t
  51
  52 -- | Term application: apply second given 'KTerm' to the first,
  53 -- applying embedded 'TeSym's if possible.
  54 teApp
  55  :: forall src cs.
  56     Proj_TyConst cs (->)
  57  => Proj_TyConst cs (#>)
  58  => Proj_TyCon cs
  59  => Inj_Source (EType src cs) src
  60  => Show_TyConst cs
  61  => KTerm src cs
  62  -> KTerm src cs
  63  -> Either (Error_TeApp src cs) (KTerm src cs)
  64 teApp (KT fun) (KT arg) = go fun arg
  65         where
  66         go
  67          :: Term src cs f
  68          -> Term src cs a
  69          -> Either (Error_TeApp src cs) (KTerm src cs)
  70         go f@TyConst{} _a = Left $ Error_TeApp_Term_missing (EType $ f `source` EType fun)
  71         go (TyApp _sb (TyApp _sa (TyConst _src' a2b) a2b_a) a2b_b) a
  72          | Just KRefl <- proj_TyConstKi @_ @(->) a2b
  73          = case eqTy a2b_a a of
  74                  Just Refl -> Right $ KT a2b_b
  75                  Nothing -> Left $ Error_TeApp_Type_mismatch (EType a2b_a) (EType a)
  76         go f@TyApp{} _a = Left $ Error_TeApp_Term_not_applicable (EType $ f `source` EType fun)
  77         go f@TyVar{} _a = Left $ Error_TeApp_Term_missing (EType $ f `source` EType fun)
  78         go t@(TyQuant src n kv f) a =
  79                 let v = freeTyVar t in
  80                 case f $ TyVar src kv v of
  81                  KT f' -> bindKT (polyTyVar n kv v) <$> go f' a
  82         go (Term (TeSym te_fun) (TyApp _sb (TyApp _sa (TyConst _src' a2b) a2b_a) a2b_b)) a
  83          | Just KRefl <- proj_TyConstKi @_ @(->) a2b
  84          = case a of
  85                  Term (TeSym te_arg) a' ->
  86                         case eqTy a2b_a a' of
  87                          Just Refl -> Right $ KT $ Term (TeSym $ sym_app te_fun te_arg) a2b_b
  88                          Nothing -> Left $ Error_TeApp_Type_mismatch (EType a2b_a) (EType a')
  89                  _ -> Left $ Error_TeApp_Term_missing (EType $ a `source` EType arg)
  90         go (Term _te x) _a = Left $ Error_TeApp_Term_not_applicable (EType $ x `source` EType fun)
  91
  92 -- | Monomorphize a 'BinTree' of 'KT'.
  93 monoTreeKT :: BinTree (KT src cs k) -> BinTree (KT src cs k)
  94 monoTreeKT t =
  95         (`SS.evalState` freeTyVarTreeKT t) $
  96         traverse (monoTy `ofKT`) t
  97
  98 -- | Fold given 'BinTree' of 'KTerm' in order to compute
  99 -- a resulting 'KTerm', if possible.
 100 evalTreeKT
 101  :: Inj_Source (EType src cs) src
 102  => Show_TyConst cs
 103  => Proj_TyConst cs (->)
 104  => Proj_TyConst cs (#>)
 105  => Proj_TyCon cs
 106  => BinTree (KTerm src cs)
 107  -> Either (Error_TeApp src cs) (MapTyVar src cs, Maybe (KTerm src cs))
 108 evalTreeKT t =
 109         foldl (\acc (KT arg) -> do
 110                 (mgu, may_fun) <- acc
 111                 case may_fun of
 112                  Nothing -> Right (mgu, Just (KT arg))
 113                  Just (KT fun) ->
 114                         case unTyFun fun of
 115                          Nothing -> inj_Error $ Error_TeApp_FunArg $ EType fun
 116                          Just (KT fun_arg, KT _fun_res) -> do
 117                                 mgu' <- inj_Error `left` mguTy mgu fun_arg arg
 118                                 let fun' = substTyVar mgu' fun
 119                                 let arg' = substTyVar mgu' arg
 120                                 KT res <- teApp fun' arg'
 121                                 Right (mgu', Just (KT res)))
 122          (Right (Map.empty, Nothing)) $
 123         monoTreeKT t
 124
 125 evalTe
 126  :: Source src
 127  => Proj_TyCon cs
 128  => Type src cs h
 129  -> Maybe (TeSym h)
 130 evalTe (Term te _ty) = Just te
 131 evalTe TyQuant{}     = Nothing
 132 evalTe TyConst{}     = Nothing
 133 evalTe TyVar{}       = Nothing
 134 evalTe TyApp{}       = Nothing