module Turner where

-- Turner's abstraction algorithm as defined by Simon PJ
-- (with properties added)

infixl 9 :@

data Var = V0 | V1
  deriving (Show, Eq)

data Exp = Exp :@ Exp | L Var Exp | V Var | F Comb
  deriving (Show, Eq)

data Comb = I | K | B | C | S | C' | B' | S'
  deriving (Show, Eq)

compile (f :@ x) = compile f :@ compile x
compile (L v e) = abstr v (compile e)
compile e = e

abstr v (f :@ x) = opt (F S :@ abstr v f :@ abstr v x)
abstr v (V w) | v == w = F I
abstr v e = F K :@ e

opt (F S :@ (F K :@ p) :@ (F K :@ q)) = F K :@ (p :@ q)
opt (F S :@ (F K :@ p) :@ F I) = p
opt (F S :@ (F K :@ p) :@ (F B :@ q :@ r)) = F B' :@ p :@ q :@ r
opt (F S :@ (F K :@ p) :@ q) = F B :@ p :@ q
opt (F S :@ (F B :@ p :@ q) :@ (F K :@ r)) = F C' :@ p :@ q :@ r
opt (F S :@ p :@ (F K :@ q)) = F C :@ p :@ q
opt (F S :@ (F B :@ p :@ q) :@ r) = F S' :@ p :@ q :@ r
opt e = e

-- Combinator reduction

simp (F I :@ a) = Just a
simp (F K :@ a :@ b) = Just a
simp (F S :@ f :@ g :@ x) = Just $ f :@ x :@ (g :@ x)
simp (F B :@ f :@ g :@ x) = Just $ f :@ (g :@ x)
simp (F C :@ f :@ g :@ x) = Just $ f :@ x :@ g
simp (F B' :@ k :@ f :@ g :@ x) = Just $ k :@ (f :@ (g :@ x))
simp (F C' :@ k :@ f :@ g :@ x) = Just $ k :@ (f :@ x) :@ g
simp (F S' :@ k :@ f :@ g :@ x) = Just $ k :@ (f :@ x) :@ (g :@ x)
simp e = Nothing

simplify e =
  case simp e of
    Nothing -> case e of
                 f :@ g -> simplify f :@ simplify g
                 _ -> e
    Just e' -> simplify e'

-- Properties

infixr 0 -->
False --> _ = True
True --> x = x

prop_abstr (v, e) = simplify (abstr v e :@ V v) == e