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)