symantic/Language/Symantic/Transforming/Beta.hs

   1 {-# LANGUAGE GADTs #-}
   2 -- | Interpreter to beta-reduce static lambdas
   3 -- introduced only because of the compiling machinery
   4 -- (hence preserving lambdas put by the user).
   5 module Language.Symantic.Transforming.Beta where
   6
   7 import Language.Symantic.Transforming.Trans
   8 import Language.Symantic.Compiling.Term
   9
  10 -- * Type 'BetaT'
  11 -- | The annotation here is if a lambda is known statically,
  12 -- and so can be applied if given an argument,
  13 -- Moreover, it only does this beta-reduction if the lambda
  14 -- has been introduced by the compiling phase
  15 -- (which happens when a symantic method is a function
  16 -- between 'term's instead of being only a 'term')
  17 -- (i.e. 'lam1' is used, not 'lam')
  18 data BetaT term a where
  19         BetaT_Unk :: term a -> BetaT term a
  20         BetaT_Lam1 :: (BetaT term a -> BetaT term b) -> BetaT term (a -> b)
  21
  22 instance Sym_Lambda term => Trans (BetaT term) where
  23         type UnT (BetaT term) = term
  24         trans = BetaT_Unk
  25         unTrans (BetaT_Unk t) = t
  26         unTrans (BetaT_Lam1 f) = lam1 $ unTrans . f . trans
  27
  28 -- | 'lam1' adds annotations, 'app' uses it
  29 instance Sym_Lambda term => Sym_Lambda (BetaT term) where
  30         lam1 = BetaT_Lam1 -- NOTE: only 'lam1' introduces 'BetaT_Lam1', not 'lam'.
  31         app (BetaT_Lam1 f) = f
  32         app f = trans2 app f
  33         let_ x f = trans $ let_ (unTrans x) (unTrans . f . trans)
  34
  35 -- | Transformer
  36 betaT :: Trans (BetaT term) => BetaT term a -> term a
  37 betaT = unTrans