|
2
|
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
|
|
5
|
8 varx : !$\mathbb{N}$!
|
|
|
9 vary : !$\mathbb{N}$!
|
|
2
|
10 open Env
|
|
|
11
|
|
5
|
12 plus-com : {l : Level} {t : Set l} !$\rightarrow$! Env !$\rightarrow$! (next : Env !$\rightarrow$! t) !$\rightarrow$! (exit : Env !$\rightarrow$! t) !$\rightarrow$! t
|
|
2
|
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
|
|
5
|
17 {-!$\#$! TERMINATING !$\#$!-}
|
|
|
18 plus-p : {l : Level} {t : Set l} !$\rightarrow$! (env : Env) !$\rightarrow$! (exit : Env !$\rightarrow$! t) !$\rightarrow$! t
|
|
|
19 plus-p env exit = plus-com env ( !$\lambda$! env !$\rightarrow$! plus-p env exit ) exit
|
|
2
|
20
|
|
5
|
21 plus : !$\mathbb{N}$! !$\rightarrow$! !$\mathbb{N}$! !$\rightarrow$! Env
|
|
|
22 plus x y = plus-p (record { varx = x ; vary = y }) (!$\lambda$! env !$\rightarrow$! env)
|
