module CL where
import Fun hiding (fv)

infixl :@


  
-- combinatory logic terms
data CL = V Ident      -- variables
        | S | K | I  -- constants
        | CL :@ CL   -- application
          deriving (Eq,Show)


-- reductions
redex ::  [CL] -> [CL]
redex (I:p:es) = p:es
redex (K:p:q:es) = p:es
redex (S:p:q:r:es) = ((p :@ r) : (q :@ r) : es)
redex _ = error "weak head normal form"

whnf :: [CL] -> Bool
whnf (I:p:_)     = False
whnf (K:p:q:_)   = False
whnf (S:p:q:r:_) = False
whnf _           = True

unwind :: [CL] -> [CL]
unwind ((e1 :@ e2) : es) = unwind (e1 : e2 :es)
unwind es                = es

reduce :: [CL] -> [CL]
reduce es | whnf es' = es'
          | otherwise = reduce (redex es')
          where es' = unwind es


-- translate lambda terms to combinators
translate :: Term -> CL
translate (Var x)      = V x
translate (Lambda x e) = abstr x (translate e)
translate (App e1 e2)  = translate e1 :@ translate e2

-- variable abstraction
abstr :: Ident -> CL -> CL
abstr x (V x') | x==x' = I
abstr x e | x `notElem` fv e = K :@ e
abstr x (e1 :@ e2) = (S :@ abstr x e1) :@ abstr x e2


-- free variables of a CL term
fv :: CL -> [Ident]
fv (V x) = [x]
fv (e1 :@ e2) = fv e1 ++ fv e2
fv _ = []   -- all constants