module cbc-agda where

open import Data.Nat
open import Level renaming ( suc to succ ; zero to Zero )

record Env : Set where
  field
    varx : ℕ
    vary : ℕ
open Env

plus-com : {l : Level} {t : Set l} → Env → (next : Env → t) → (exit : Env → t) → t
plus-com env next exit with vary env
... | zero  = exit (record { varx = varx env ; vary = vary env })
... | suc y = next (record { varx = suc (varx env) ; vary = y })

{-# TERMINATING #-}
plus-p : {l : Level} {t : Set l} → (env : Env) → (exit : Env → t) → t
plus-p env exit = plus-com env ( λ env → plus-p env exit ) exit

plus : ℕ → ℕ → Env
plus x y = plus-p (record { varx = x ; vary = y }) (λ env → env)