{-# LANGUAGE GADTs #-}
-- | Interpreter to beta-reduce static lambdas
-- introduced only because of the compiling machinery
-- (hence preserving lambdas put by the user).
module Language.Symantic.Transforming.Beta where
import Language.Symantic.Transforming.Trans
import Language.Symantic.Compiling.Term
-- * Type 'BetaT'
-- | The annotation here is if a lambda is known statically,
-- and so can be applied if given an argument,
-- Moreover, it only does this beta-reduction if the lambda
-- has been introduced by the compiling phase
-- (which happens when a symantic method is a function
-- between 'term's instead of being only a 'term')
-- (i.e. 'lam1' is used, not 'lam')
data BetaT term a where
BetaT_Unk :: term a -> BetaT term a
BetaT_Lam1 :: (BetaT term a -> BetaT term b) -> BetaT term (a -> b)
instance Sym_Lambda term => Trans (BetaT term) where
type UnT (BetaT term) = term
trans = BetaT_Unk
unTrans (BetaT_Unk t) = t
unTrans (BetaT_Lam1 f) = lam1 $ unTrans . f . trans
-- | 'lam1' adds annotations, 'app' uses it
instance Sym_Lambda term => Sym_Lambda (BetaT term) where
lam1 = BetaT_Lam1 -- NOTE: only 'lam1' introduces 'BetaT_Lam1', not 'lam'.
app (BetaT_Lam1 f) = f
app f = trans2 app f
let_ x f = trans $ let_ (unTrans x) (unTrans . f . trans)
-- | Transformer
betaT :: Trans (BetaT term) => BetaT term a -> term a
betaT = unTrans