# Helpers
datatype 'a list {
  Cons ('a, 'a list),
  Empty,
}

datatype 'a maybe {
  Just 'a,
  Nothing,
}

# Lambda calculus term, nameless representation
datatype term {
  Var int
  Int int
  Abs term
  App (term, term)
}

# Result of the evaluation
datatype value {
  Int     int
  Closure (env, term)
}

alias env = value list

typecheck add_binding : value -> env -> env
def add_binding v env = Cons v env

typecheck lookup : int -> env -> value maybe
def lookup _ <Empty> = Nothing
  | lookup 0 <Cons x xs> = Just x
  | lookup n <Cons x xs> = lookup (subtract n 1) xs

typecheck eval : env -> term -> value
def eval e <Var idx> = match lookup idx e {
                         case <Just v>   -> v
                         case <Nothing>  -> abort "Variable out of scope"
                       }

  | eval e <Int x> = Int x
  | eval e <Abs t> = Closure e t
  | eval e <App t1 t2> =
      let def new_env = add_binding (eval e t2) e
      in eval new_env t1