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-c : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
plus-c env exit = plus-p (vary env) env exit where
  plus-p : {l : Level} {t : Set l} → ℕ →  Env → (exit : Env → t) → t
  plus-p zero env exit = exit env
  plus-p (suc reducer) env exit = plus-p reducer record env{varx = (suc (varx env)) ; vary = reducer} exit

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

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