{-# LANGUAGE DoRec #-}

module Main where
import Prelude hiding(fst, snd, succ)
import System.Vacuum.OpenGL.Client
import Data.IORef

-- * Removing syntactic sugar

-- | Choice can be represented by choosing the proper parameter as a continuation
true :: a -> a -> a
true  = \ x y -> x

false :: a -> a -> a
false = \ x y -> y

if_ c t e = c t e

ex1 :: Char
ex1 = if_ true  'a'  'b'

-- | A product can be represented by a function which \"remembers\" ist components, and returns them to a continuation
pair :: a -> b -> (a -> b -> r) -> r
pair x y = \c -> c x y

fst p = p (\ x y -> x)
snd p = p (\ x y -> y)

ex2 = fst (pair 'a' (3::Int))

-- ** Scott encoding (does not type check!)
-- We  now we combine both approaches and get the so-called Scott encoding

data Nat = Zero | Succ Nat

{-
zero   = \z c -> z
succ x = \z c -> c x

one = succ zero
two = succ one

plus x y = x y (\xm1 -> succ (plus xm1 y))

four = plus two two
-}

-- | In order to observe the computed integer value we map it onto a conventional integer
{-

foldnat z s n = n z (\p -> s (foldnat  z s p))

ex4 = foldnat 0 (+1) four

-}

-- ** Church encoding
-- We represent values by their partially applied, flipped fold function. The value n is represented by a 
-- a function which appies its first argument n times to it second

nat2churchnat Zero     = \ s z  -> z
nat2churchnat (Succ x) = \ s z  -> s (nat2churchnat x s z)

zero      = \ f x -> x
one       = \ f x -> f x
two       = \ f x -> f ( f x)
succ    n = \ f x -> f (n f x)
plus  m n = \ f x -> n f (m f x)
times m n = \ f x -> m (n f) x

church2Int n = n (+1) 0

-- ** Let-expressions
-- Non-recursive let-expresion can be mapped onto function applications

-- ** Recursion
-- Unfortunately we cannot represent a fixedpoint combinators in a well-typed way
-- (\ f -> (\x -> f (x x)) (\x -> f (x x))) g
-- -> 
-- (\x -> g (x x)) (\x -> g (x x))
-- -> 
-- g ((\x -> g (x x)) (\x -> g (x x)))
-- ->
-- g (g ((\x -> g (x x)) (\x -> g (x x))))
--
-- -> g (g ( g( g( ...))))

-- hence we resort to defining a single recursive function which we use to represent all other recursive functions

fix :: (a -> a) -> a
fix f = let fixf = f (fixf) in fixf

-- ** Mutial recursion
--  let f = \x -> ... g ...
--      g = \y -> ... f ...
--
-- is mapped onto
--
--  let fg = fix (\fg -> (\x -> ... (snd fg) ...
--                       ,\y -> ... (fst fg) ...
--                       )
--

-- * How to use the module vacccuum-opengl
{-
 $ vacuum-opengl-server &
 vacuum-opengl server started - press ESC to exit. 
 listening on port 55961
 
 $ ghci
 Prelude> :m + System.Vacuum.OpenGL 
 Prelude System.Vacuum.OpenGL> view [1..5]
 Prelude System.Vacuum.OpenGL> view $ zip "foobar" [1..6]
 Prelude System.Vacuum.OpenGL> :m + Data.Set
 Prelude System.Vacuum.OpenGL Data.Set> view $ fromList [1..10]
-}
 
-- * SKI combinators

infixl 9 :@:

-- | Lambda expressions can be mapped onto variable free expressinos, 
--   consisting only of call to the basic combinators `S`, `K` and `I`.

data SKI = S  | K | I
         | SKI :@: SKI
         | Var String
         | Y 
         -- | for optimising purposes we add a few extra combinators
         | B 
         | C
         -- | and even a few more
         | S' | B' | C'
         deriving (Show)

-- | step_SKI performs a single evaluation step
step_SKI (S :@: f :@: g        :@: x) = (f  :@: x) :@: (g :@: x)
step_SKI (K :@: y              :@: x) = y
step_SKI (I                    :@: x) = x
step_SKI (Var s                     ) = Var s  -- we leave global variables untouched
step_SKI (Y                    :@: x) = let r = x :@: r in r
step_SKI (B        :@: f :@: g :@: x) = f         :@: (g :@: x)
step_SKI (C        :@: f :@: g :@: x) = (f :@: x) :@:  g
step_SKI (S' :@: c :@: f :@: g :@: x) = c :@: (f :@: x) :@: (g :@: x)
step_SKI (B' :@: c :@: f :@: g :@: x) = c :@: (f      ) :@: (g :@: x)
step_SKI (C' :@: c :@: f :@: g :@: x) = c :@: (f :@: x) :@:  g
step_SKI (l  :@:                   r) = step_SKI l :@: r       


-- | The type `Lambda` represents a lambda expression
data Lambda = V String
            | App Lambda Lambda
            | L String Lambda

 
-- | l2ski compiles a `lambda`-expression into SKI form
l2ski :: Lambda -> SKI
l2ski (App   l r)    = l2ski l :@: l2ski r
l2ski (V     s    )  = Var  s
l2ski (L v body)     = abstract v (l2ski body)

abstract :: String -> SKI -> SKI
abstract v (Var s) | s == v     = I
                   | otherwise  = K :@: Var s
abstract v (f :@: a) = S :@: (abstract v f) :@: (abstract v a)  -- (\v. f a) -> S (\v.f) (\v.a)
abstract v c         = K :@: c

optimise  (l :@: r) = optimise' (optimise l :@: optimise r)
optimise' (S :@: (B :@: c :@: f) :@:  g ) = optimise' (S' :@: c :@: f :@: g)
optimise' (S :@: (K :@: l) :@: (K :@: r)) = K :@: (l :@: r)
optimise' (S :@: (      l) :@: (K :@: r)) = C :@:  l :@: r 
optimise' (S :@: (K :@: l) :@:        r ) = B :@:  l :@: r

--  the S', B' and C' we leave as an exercise

-- | The function `demo` performs a single outermost reduction step and shows the resulting graph on the server
--   keep in mind that sharing of expressions is not visible since it gets lost during reduction
demo :: SKI -> IO ()
demo t = do print t
            view t            
            getLine
            demo (step_SKI t)

add    = V "add"
x      = V "x"
v      = V "3"

t = (L "x" (add `App` x `App`x)) `App` (add `App` v `App` v)   


infixl 9 `App` 

data SKIr =  IORef SKIr :@@: IORef SKIr
          |  Varr String

app f a = newIORef (f `App` a)

ski2skir
  :: IO (IORef SKIr) -> IO (IORef SKIr) -> IO (IORef SKIr) -> 
     IO (IORef SKIr) -> IO (IORef SKIr) -> IO (IORef SKIr)
     -> SKI
     -> IO (IORef SKIr)

ski2skir s k i y b c t = toGraph t
 where toGraph S = s
       toGraph K = k
       toGraph I = i
       toGraph Y = y
       toGraph B = b
       toGraph C = c
       toGraph (f :@: a) = do fr <- toGraph f
                              fa <- toGraph a
                              newIORef (fr :@@: fa)                            
       toGraph (Var  s)  = newIORef (Varr s)

-- Exercise: implement the reducer for SKIBCY expressions which implements the shared evaluation by overwriting applications
-- with their result.