{-# 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