module HazyAbstractElim (abstractElim, compileToSKI, prims, (!)) where

import qualified Data.Set as Set
import HazyParse

abstractElim :: [(VarId, Exp)] -> [(VarId, Exp)]
abstractElim eqs = [elimOne eq | eq <- eqs]

compileToSKI :: [(VarId, Exp)] -> [(VarId, Exp)]
compileToSKI eqs = [elimOneSKI eq | eq <- eqs]

infixl 0 !
(Lam f) ! x = f x

prims = let (-->) = (,) in
        [ "I" --> (Lam$ \x -> x)
        , "K" --> (Lam$ \x -> Lam$ \y -> x)
        , "S" --> (Lam$ \f -> Lam$ \g -> Lam$ \x -> f!x!(g!x))
        , "B" --> (Lam$ \f -> Lam$ \g -> Lam$ \x -> f!(g!x))
        , "C" --> (Lam$ \f -> Lam$ \g -> Lam$ \x -> f!x!g)
        , "S'" --> (Lam$ \c -> Lam$ \f -> Lam$ \g -> Lam $ \x -> c!(f!x)!(g!x))
        , "B*" --> (Lam$ \c -> Lam$ \f -> Lam$ \g -> Lam $ \x -> c!(f!(g!x)))
        , "C'" --> (Lam$ \c -> Lam$ \f -> Lam$ \g -> Lam $ \x -> c!(f!x)!g)
        ]
{-
        , "ADD_W" --> arith2 (+) , "SUB_W" --> arith2 (-)
        , "EQ_W" --> logical2 (==) , "NE_W" --> logical2 (/=)
        , "LE_W" --> logical2 (<=)
-}
{-
arith2 op = Lam $ \(Int a) -> Lam $ \(Int b) -> Int (op a b)
logical2 op = Lam $ \(Int a) -> Lam $ \(Int b) -> if op a b then true else false
true = Lam $ \t -> Lam $ \f -> t
false = Lam $ \t -> Lam $ \f -> f
-}

elimOneSKI (funid, exp) = (funid, varToFun $ ski exp)
elimOne (funid, exp) = (funid, varToFun $ t exp)

varToFun (Fun v) = (Fun v)
varToFun (Var v) = (Fun v)
varToFun (Ap x y) = Ap (varToFun x) (varToFun y)
varToFun (Lambda x y) = Lambda x (varToFun y)

i = Fun "I"
k term = (Fun "K") `Ap` term
bin name x y = (Fun name `Ap` x) `Ap` y
s = bin "S"
c = bin "C"
b = bin "B"

notFree v e = not (free v e)

free v e = free' (Set.empty) v e
free' bound v (Var x)
   | v == x         = v `Set.notMember` bound
   | otherwise      = False
free' bound v (Fun x)      = False
free' bound v (Ap e1 e2)   = (v `free` e1) || (v `free` e2)
free' bound v (Lambda x e) = free' (Set.insert x bound) v e

-- T[x] => x
ski (Fun x) = (Fun x)
-- T[x] => x
ski (Var x) = (Var x)
-- T[(E₁ E₂)] => (T[E₁] T[E₂])
ski (Ap e1 e2) = Ap (ski e1) (ski e2)
-- T[λx.E] => (K T[E]) (if x is not free in E)
ski (Lambda x e) | x `notFree` e  = k (ski e)
-- T[λx.x] => I
ski (Lambda x (Var f)) | x == f   = i
-- T[λx.λy.E] => T[λx.T[λy.E]] (if x is free in E)
ski (Lambda x ye@(Lambda y e)) | x `free` e  = ski (Lambda x (ski ye))
-- T[λx.(E₁ E₂)] => (S T[λx.E₁] T[λx.E₂])
ski (Lambda x (Ap e1 e2)) = s (ski (Lambda x e1)) (ski (Lambda x e2))

-- T[x] => x
t (Fun x) = (Fun x)
-- T[x] => x
t (Var x) = (Var x)
-- T[(E₁ E₂)] => (T[E₁] T[E₂])
t (Ap e1 e2) = Ap (t e1) (t e2)
-- T[λx.E] => (K T[E]) (if x is not free in E)
t (Lambda x e) | x `notFree` e  = k (t e)
-- T[λx.x] => I
t (Lambda x (Var f)) | x == f   = i
-- T[λx.λy.E] => T[λx.T[λy.E]] (if x is free in E)
t (Lambda x ye@(Lambda y e)) | x `free` e  = t (Lambda x (t ye))
-- T[λx.(E₁ E₂)] => (S T[λx.E₁] T[λx.E₂])
--t (Lambda x (Ap e1 e2)) = s (t (Lambda x e1)) (t (Lambda x e2))
t (Lambda x (Ap e1 e2))
   | x `free` e1 && x `free` e2    = s (t (Lambda x e1)) (t (Lambda x e2))
   | x `free` e1 && x `notFree` e2 = c (t (Lambda x e1)) (t e2)
   | x `notFree` e1 && x `free` e2 = b (t e1)            (t (Lambda x e2))