|
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-c : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
|
|
|
13 plus-c env exit = plus-p (vary env) env exit where
|
|
|
14 plus-p : {l : Level} {t : Set l} → ℕ → Env → (exit : Env → t) → t
|
|
|
15 plus-p zero env exit = exit env
|
|
|
16 plus-p (suc reducer) env exit = plus-p reducer record env{varx = (suc (varx env)) ; vary = reducer} exit
|
|
|
17
|
|
|
18 {-# TERMINATING #-}
|
|
|
19 plus-c-term : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
|
|
|
20 plus-c-term env exit with vary env
|
|
|
21 ... | zero = exit (record { varx = varx env ; vary = vary env })
|
|
|
22 ... | suc y = plus-c-term (record { varx = suc (varx env) ; vary = y }) exit
|
|
|
23
|
|
|
24 plus : ℕ → ℕ → Env
|
|
|
25 plus x y = plus-c (record { varx = x ; vary = y }) (λ env → env)
|
