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 betaTerm ::
  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 betaTerm (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 `eqType` ta of
  25                  Nothing -> Left $ Error_Beta_Type_mismatch (TypeVT a2b_a) (TypeVT ta)
  26                  Just Refl ->
  27                         Right $
  28                         case (proveConstraint qf, proveConstraint qa) of
  29                          -- NOTE: remove provable Constraints to keep those smaller.
  30                          (Just Dict, Just Dict) -> TermT $ Term @_ @_ @_ @_ @(_ #> _) (noConstraintLen (lenVars a2b_b)) a2b_b $
  31                                 TeSym $ \c -> te_fun c `app` te_arg c
  32                          (Just Dict, Nothing) -> TermT $ Term @_ @_ @_ @_ @(_ #> _) qa a2b_b $
  33                                 TeSym $ \c -> te_fun c `app` te_arg c
  34                          (Nothing, Just Dict) -> TermT $ Term @_ @_ @_ @_ @(_ #> _) qf a2b_b $
  35                                 TeSym $ \c -> te_fun c `app` te_arg c
  36                          (Nothing, Nothing)     -> TermT $ Term @_ @_ @_ @_ @(_ #> _) (qf # qa) a2b_b $
  37                                 TeSym $ \c -> te_fun c `app` te_arg c
  38          _ -> Left $ Error_Beta_Term_not_a_function $ TypeVT (qf #> tf)
  39
  40 -- | Collapse given 'BinTree' of 'TermVT's to compute a resulting 'TermVT', if possible.
  41 betaTerms ::
  42  Inj_Source (TypeVT src) src =>
  43  Constable (->) =>
  44  BinTree (TermVT src ss es) ->
  45  Either (Error_Beta src) (TermVT src ss es)
  46 betaTerms t =
  47         collapseBT (\acc ele -> do
  48                 TermVT (Term qf tf te_fun) <- acc
  49                 TermVT (Term qa ta te_arg) <- ele
  50                 let (tf', ta') = appendVars tf ta
  51                 let (qf', qa') = appendVars qf qa
  52                 case unTyFun tf' of
  53                  Nothing -> Left $ Error_Beta_Term_not_a_function $ TypeVT tf'
  54                  Just (af, _rf) -> do
  55                         mgu <-
  56                                 (Error_Beta_Unify `left`) $
  57                                 case (unQualsTy af, unQualsTy ta') of
  58                                  (TypeK af', TypeK ta'') -> unifyType mempty af' ta''
  59                         let qf'' = subst mgu qf'
  60                         let qa'' = subst mgu qa'
  61                         let tf'' = subst mgu tf'
  62                         let ta'' = subst mgu ta'
  63                         TermT (Term qr tr te_res) <- betaTerm (Term qf'' tf'' te_fun) (Term qa'' ta'' te_arg)
  64                         normalizeVarsTy (qr #> tr) $ \(TyApp _ (TyApp _ _c qr') tr') ->
  65                                 Right $ TermVT $ Term qr' tr' te_res
  66          ) (Right <$> t)
  67
  68 -- * Type 'Error_Beta'
  69 data Error_Beta src
  70  =   Error_Beta_Term_not_a_function (TypeVT src)
  71  |   Error_Beta_Type_mismatch (TypeVT src) (TypeVT src)
  72  |   Error_Beta_Unify (Error_Unify src)
  73      -- ^ Cannot unify the expected 'Type' of the argument of the function,
  74      -- with the 'Type' of the argument.
  75  deriving (Eq, Show)
  76
  77 instance Inj_Error (Error_Beta src) (Error_Beta src) where
  78         inj_Error = id
  79 instance Inj_Error (Error_Unify src) (Error_Beta src) where
  80         inj_Error = Error_Beta_Unify