module Stack where

fn :: Int -> (a -> a) -> a -> a
fn 0 f x = x
fn n f x = fn (n - 1) f (f x)

suc :: Int -> Int
suc n = n + 1

exp1 :: Int -> Int -> Int
exp1 m n = fn m (fn n) suc 0

--

data Fun b = Unit (b -> b) | Rec (Fun b) (Fun b -> b -> b)

call :: Fun b -> b -> b
call (Unit f) x = f x
call (Rec env f) x = f env x

fn' :: Int -> Fun b -> b -> b
fn' 0 f x = x
fn' n f x = fn' (n - 1) f (call f x)

fn1 :: Int -> Fun b -> Fun b
fn1 n f = Rec f (fn' n)

exp2 :: Int -> Int -> Int
exp2 m n = call (fn' m (Unit (fn1 n)) (Unit suc)) 0

--

data Closure b where
  Exists :: a -> (a -> b -> b) -> Closure b

callC :: Closure b -> b -> b
callC (Exists x f) y = f x y

fnC :: Int -> Closure b -> b -> b
fnC 0 c x = x
fnC n c x = fnC (n - 1) c (callC c x)

fnC1 :: Int -> Closure b -> Closure b
fnC1 n c = Exists c (fnC n)

fnC1' :: Int -> () -> Closure b -> Closure b
fnC1' n () c = fnC1 n c

sucC :: () -> Int -> Int
sucC () n = n + 1

exp3 :: Int -> Int -> Int
exp3 m n = callC (fnC m (Exists () (fnC1' n)) (Exists () sucC)) 0

--

-- type Closure b c = ... | Fn (type of env) (type of env -> b -> c) | ...
-- [[\x.^n e]] = (fn, env) where
--   fn env x = [[e]]
--   env = "free vars in [[e]]"