AbsElim.hs

module AbsElim where

  import qualified SKI
  import qualified Lam

  infixl :@:
  data T = S | K | I | Bound Int | Lam T | T :@: T

  fromLam :: Lam.Lam -> T
  fromLam (Lam.Bound i) = Bound i
  fromLam (Lam.Lam t) = Lam (fromLam t)
  fromLam (Lam.(:@:) t u) = fromLam t :@: fromLam u

  toSKI :: T -> SKI.SKI
  toSKI S = SKI.S
  toSKI K = SKI.K
  toSKI I = SKI.I
  toSKI (t :@: u) = SKI.App (toSKI t) (toSKI u)
  toSKI t = error "toSKI: termino " ++ show t ++ " no traducible"

  absElim :: T -> T
  absElim (Bound i) = Bound i
  absElim (t :@: u) = absElim t :@: absElim u
  absElim (Lam t) | not (occurs 0 t) = K :@: absElim t
  absElim (Lam (Bound 0)) = I
  absElim (Lam (Lam t)) = absElim (Lam $ absElim (Lam t))
  absElim (Lam (t :@: u)) = S :@: absElim (Lam t) :@: absElim (Lam u)
    where occurs n (Bound i) = n == i
          occurs n (Lam t) = occurs (n + 1) t
          occurs n (t :@: u) = occurs n t || occurs n u
          occurs _ _ = False