module cbc-agda where

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

record Env : Set where
  field
    varx : !$\mathbb{N}$!
    vary : !$\mathbb{N}$!
open Env

plus-com : {l : Level} {t : Set l} !$\rightarrow$! Env !$\rightarrow$! (next : Env !$\rightarrow$! t) !$\rightarrow$! (exit : Env !$\rightarrow$! t) !$\rightarrow$! 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} !$\rightarrow$! (env : Env) !$\rightarrow$! (exit : Env !$\rightarrow$! t) !$\rightarrow$! t
plus-p env exit = plus-com env ( !$\lambda$! env !$\rightarrow$! plus-p env exit ) exit

plus : !$\mathbb{N}$! !$\rightarrow$! !$\mathbb{N}$! !$\rightarrow$! Env
plus x y = plus-p (record { varx = x ; vary = y }) (!$\lambda$! env !$\rightarrow$! env)