module UTLC where 

import Iso
import Games 
import BasicGames

-- /Exp/
data Exp = Var Nat | Lam Exp | App Exp Exp 
-- /End/
           deriving Show



-- /expGame/
expGame :: Nat -> Game Exp 
expGame 0 = appLamG 0
expGame n = 
  Split (Iso ask bld) (rangeGame 0 (n-1)) (appLamG n)
  where ask (Var i)   = Left i
        ask e         = Right e 
        bld (Left i)  = Var i
        bld (Right e) = e        
-- /End/

-- /appLamGame/
appLamG n = 
 Split (Iso ask bld) (prodGame (expGame n) (expGame n)) 
                     (expGame (n+1))
 where ask (App e1 e2)    = Left (e1,e2) 
       ask (Lam e)        = Right e
       bld (Left (e1,e2)) = App e1 e2
       bld (Right e)      = Lam e
-- /End/

exI = Lam (Var 0)
exK = Lam (Lam (Var 1))
ex = App exI exK