module UTLC where
import Iso
import Games
import BasicGames
data Exp = Var Nat | Lam Exp | App Exp Exp
deriving Show
expGame :: Nat -> Game Exp
expGame 0 = appLamG 0
expGame n =
Split (Iso ask bld) (rangeGame 0 (n1)) (appLamG n)
where ask (Var i) = Left i
ask e = Right e
bld (Left i) = Var i
bld (Right e) = e
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
exI = Lam (Var 0)
exK = Lam (Lam (Var 1))
ex = App exI exK