module Lambda where

--import Control.Arrow
import Control.Monad (liftM2)
import Control.Monad.Instances -- for e.g. (->)
import Data.Char
import Data.List
import Debug.Trace

data LambdaExp =
	Lambda Id LambdaExp
	| App LambdaExp LambdaExp
	| Var Id
	| Inc
	| Num Int
	deriving (Eq,Show)

type Id = Int

-- This is where magic is happening.
apply (Lambda n x) y = replace n y x
apply (App x y) z = apply (apply x y) z
apply Inc (Num x) = x `seq` Num (x+1)
apply Inc x = apply Inc (eval x)
apply (Var id) y = error "apply variable - not good"
apply (Num x) y = App (church x) y

eval (App x y) = eval (apply x y)
eval x = x

-- replace: Replace n with x in y
-- Essentially, this is beta-reduction. To be on the safe side, variables in |x|
-- should be renamed if they collide with variables in |y|.

-- Inner lambdas that has the same variable bind harder, i.e. the new scope
-- shadows the old variable, and nothing is replaced within

replace n x y@(Var m)
	| n == m = x
	| True = (Var m)
replace n x y@(Lambda m exp)
	| n == m = y
	| True = Lambda m (replace n x exp)
replace n x (App a b) = App (replace n x a) (replace n x b)
replace n x y = y

-- The classical S combinator, (\f g x -> f x (g x))
-- s = \f g x -> f x (g x)
-- s = \f -> \g x -> f x (g x)
-- s = \f -> \g -> \x -> (f x) (g x)
-- s = \0 -> \1 -> \2 -> App (App 0 2) (App 1 2)

sComb =
  Lambda 0 $ Lambda 1 $ Lambda 2 $
	App (App (Var 0) (Var 2)) (App (Var 1) (Var 2))

-- Fokker's X combinator, x = (\f -> (f s) (\x _ _ -> x)), expressed as a
-- LambdaExp:

xComb = Lambda 0 $
   App
      (App (Var 0) sComb)
      (Lambda 0 $ Lambda 1 $ Lambda 2 $ Var 0)

-- The church numeral 256 apparently has a quite small representation as:

-- ((lambda (n) (n n))
-- 	((lambda (n) (n n))
-- 		(lambda (f x)
-- 			(f (f x)))))

church 0 = (Lambda 0 (Lambda 1 (Var 1)))

-- church n = (\f -> (f (church n-1)))
-- succ = λn.λf.λx. f (n f x)

-- plus = λn.λm.λf.λx. n (m f x)

-- TODO: It should be possible to make this generate lambda expressions of size
-- logn, by e.g. using the binary representation of the number
-- rather than n = 1+n', you'd have n = (2 ^ m) + n'
church n = let n' = (church (n-1)) in --n' `seq`
	(App
		(Lambda 0 (Lambda 1 (Lambda 2
			(App (Var 1) (App (App (Var 0) (Var 1)) (Var 2))))))
		n')
churchEof = Num 256

unchurch (Num i) = i
unchurch x = case eval (App (App x Inc) (Num 0)) of
	Num i -> i
	_ -> error $ "Lambda expression "++ {-(show x) ++-} " is not a number"

funcar x = apply x (Lambda 0 (Lambda 1 (Var 0)))
funcdr x = apply x (Lambda 0 (Lambda 1 (Var 1)))

emptyInput = Lambda 0 churchEof

runWithInput inp x = getOutput $ App x inp

getOutput x = liftM2 (:) (chr . unchurch . funcar) (getOutput . funcdr) x