Eval.hs

module Eval ( evalSKI, evalLam ) where

import NamedLam
import Lam
import SKI

evalSKI :: SKI -> Lam
evalSKI (App t u) = evalSKI t :@: evalSKI u
evalSKI t = elabLam $ translate t
  where translate S = NLam ["f", "g", "x"] $ Var "f" `NApp` Var "x" `NApp` (Var "g" `NApp` Var "x")
        translate K = NLam ["x", "y"] $ Var "x"
        translate I = NLam ["x"] $ Var "x"

------------------------------------------------------------------------------------------------------

infixr $$ 
($$) :: SKI -> SKI -> SKI
t $$ u = App t u

call :: [SKI] -> SKI
call [x] = x
call (x:y:xs) = call (App x y : xs)

infixr |>
(|>) :: SKI -> SKI -> SKI
t |> u = call [S, K $$ t, u]

app :: SKI
app = I

comp :: SKI
comp = call [S, K $$ S, K]

-- TODO https://en.wikipedia.org/wiki/Combinatory_logic#Completeness_of_the_S-K_basis
evalLam :: Lam -> SKI
evalLam = go 0
  where go n (Bound i) = parg n (n - i)
        go n (Lam t) = go (n + 1) t
        go n (t :@: u) = pipe n (go n t) (go n u)

parg :: Int -> Int -> SKI
parg n p | n <= 0 || p <= 0 = error "parg: no positivo"
parg n p | n < p = error $  "parg: p fuera de rango (" ++ show n ++ " < " ++ show p ++ ")"
-- parg n p = relim (p - 1) (K $$) (relim (n - p) (K |>) I)
-- lo escribo asi para que quede mas lindo nomá
parg 1 1 = I
parg 2 1 = K
parg n 1 = K |> parg (n - 1) 1
parg n p = K $$ parg (n - 1) (p - 1)

pipe :: Int -> SKI -> SKI -> SKI
pipe n _ _ | n < 0 = error "pipe: negativo"
pipe 0 t u = t $$ u
pipe 1 t u = call [S, t, u]
pipe n t u = call [S , pipe' (n - 1) |> t, u]
  where pipe' 0 = I
        pipe' 1 = S
        pipe' (n +  1) = S |> (comp $$ pipe' n)

relim :: Int -> (a -> a) -> a -> a
relim i _ _ | i < 0 = error "relim: negativo"
relim 0 _ z = z
relim (n + 1) f z = f (relim n f z)