Mercurial > hg > Papers > 2023 > soto-master

comparison Paper/src/agda/cbc-agda.agda @ 1:a72446879486

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Init paper
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Thu, 12 Jan 2023 20:28:50 +0900
parents
children
comparison
equal deleted inserted replaced
0:8df537cb6a18 1:a72446879486
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)