symantic/Language/Symantic/Compiling/Beta.hs

   1 -- | Beta-reduction of 'Term's.
   2 module Language.Symantic.Compiling.Beta where
   3
   4 import Control.Arrow (left)
   5 import qualified Data.Kind as K
   6
   7 import Language.Symantic.Grammar
   8 import Language.Symantic.Typing
   9 import Language.Symantic.Compiling.Term
  10
  11 -- | Term application: apply second given 'TermT' to the first,
  12 -- applying embedded 'TeSym's, or return an error.
  13 betaTe ::
  14  forall src ss es vs fun arg.
  15  Inj_Source (TypeVT src) src =>
  16  Constable (->) =>
  17  Term src ss es vs (fun::K.Type) ->
  18  Term src ss es vs (arg::K.Type) ->
  19  Either (Error_Beta src) (TermT src ss es vs)
  20 betaTe (Term qf tf (TeSym te_fun)) (Term qa ta (TeSym te_arg)) =
  21         case tf of
  22          TyApp _ (TyApp _ a2b a2b_a) a2b_b
  23           | Just HRefl <- proj_ConstKiTy @(K (->)) @(->) a2b ->
  24                 case a2b_a `eqTy` ta of
  25                  Nothing -> Left $ Error_Beta_Type_mismatch (TypeVT a2b_a) (TypeVT ta)
  26                  Just Refl ->
  27                         Right $ TermT $ Term @_ @_ @_ @_ @(_ #> _) (qf # qa) a2b_b
  28                          (TeSym $ \c -> te_fun c `app` te_arg c)
  29          _ -> Left $ Error_Beta_Term_not_a_function $ TypeVT (qf #> tf)
  30
  31 -- | Collapse given 'BinTree' of 'TermVT's to compute a resulting 'TermVT', if possible.
  32 betasTe ::
  33  Inj_Source (TypeVT src) src =>
  34  Constable (->) =>
  35  BinTree (TermVT src ss es) ->
  36  Either (Error_Beta src) (TermVT src ss es)
  37 betasTe t =
  38         collapseBT (\acc ele -> do
  39                 TermVT (Term qf tf te_fun) <- acc
  40                 TermVT (Term qa ta te_arg) <- ele
  41                 let (tf', ta') = appendVars tf ta
  42                 let (qf', qa') = appendVars qf qa
  43                 case unTyFun tf' of
  44                  Nothing -> Left $ Error_Beta_Term_not_a_function $ TypeVT tf'
  45                  Just (af, _rf) -> do
  46                         mgu <-
  47                                 (Error_Beta_Unify `left`) $
  48                                 case (unQualsTy af, unQualsTy ta') of
  49                                  (TypeK af', TypeK ta'') -> mguTy mempty af' ta''
  50                         let qf'' = subst mgu qf'
  51                         let qa'' = subst mgu qa'
  52                         let tf'' = subst mgu tf'
  53                         let ta'' = subst mgu ta'
  54                         TermT (Term qr tr te_res) <- betaTe (Term qf'' tf'' te_fun) (Term qa'' ta'' te_arg)
  55                         normalizeVarsTy (qr #> tr) $ \(TyApp _ (TyApp _ _c qr') tr') ->
  56                                 Right $ TermVT $ Term qr' tr' te_res
  57          ) (Right <$> t)
  58
  59 -- * Type 'Error_Beta'
  60 data Error_Beta src
  61  =   Error_Beta_Term_not_a_function (TypeVT src)
  62  |   Error_Beta_Type_mismatch (TypeVT src) (TypeVT src)
  63  |   Error_Beta_Unify (Error_Unify src)
  64      -- ^ Cannot unify the expected 'Type' of the argument of the function,
  65      -- with the 'Type' of the argument.
  66  deriving (Eq, Show)
  67
  68 instance Inj_Error (Error_Beta src) (Error_Beta src) where
  69         inj_Error = id
  70 instance Inj_Error (Error_Unify src) (Error_Beta src) where
  71         inj_Error = Error_Beta_Unify
  72
  73 {-
  74 (<<*>>) :: Monad m => m (a -> m b) -> m a -> m b
  75 (<<*>>) f a = f >>= (a >>=)
  76 infixl 4 <<*>>
  77 {-# INLINE (<<*>>) #-}
  78 -}