|
1
|
1 module cbc-agda where
|
|
|
2
|
|
|
3 open import Data.Nat
|
|
|
4 open import Level renaming ( suc to succ ; zero to Zero )
|
|
|
5
|
|
|
6 record Env : Set where
|
|
|
7 field
|
|
|
8 varx : ℕ
|
|
|
9 vary : ℕ
|
|
|
10 open Env
|
|
|
11
|
|
|
12 plus-com : {l : Level} {t : Set l} → Env → (next : Env → t) → (exit : Env → t) → t
|
|
|
13 plus-com env next exit with vary env
|
|
|
14 ... | zero = exit (record { varx = varx env ; vary = vary env })
|
|
|
15 ... | suc y = next (record { varx = suc (varx env) ; vary = y })
|
|
|
16
|
|
|
17 {-# TERMINATING #-}
|
|
|
18 plus-p : {l : Level} {t : Set l} → (env : Env) → (exit : Env → t) → t
|
|
|
19 plus-p env exit = plus-com env ( λ env → plus-p env exit ) exit
|
|
|
20
|
|
|
21 plus : ℕ → ℕ → Env
|
|
|
22 plus x y = plus-p (record { varx = x ; vary = y }) (λ env → env)
|
