]> Git — Sourcephile - haskell/symantic.git/blob - symantic/Language/Symantic/Compiling/Beta.hs
Improve handling of metadata in grammars.
[haskell/symantic.git] / 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 -}