Mercurial > hg > Papers > 2021 > soto-thesis
view paper/src/agda/hoare-while1.agda @ 4:bf1f62556b81
add while_test_init_imple
author | soto |
---|---|
date | Thu, 11 Feb 2021 17:03:31 +0900 |
parents | |
children |
line wrap: on
line source
module hoare-while1 where open import Level renaming (suc to Suc ; zero to Zero ) module WhileTest where open import Relation.Binary.PropositionalEquality open import Relation.Binary.Core open import Data.Nat hiding (compare) open import Data.Maybe open import Data.List open import Function open import logic record Env : Set (Suc Zero) where field varn : ℕ vari : ℕ open Env record WhileTest {m : Level } {t : Set m } : Set (Suc m) where field env : Env whileInit : (c10 : ℕ) → (Env → t) → t whileInit c10 next = next (record {varn = c10 ; vari = 0 } ) whileLoop : Env → (Code : Env → t) → t whileLoop env next = whileLoop1 (varn env) env where whileLoop1 : ℕ → Env → t whileLoop1 zero env = next env whileLoop1 (suc t ) env = whileLoop1 t (record env {varn = t ; vari = (vari env) + 1}) whileTest : (c10 : ℕ) → (Env → t) → t whileTest c10 next = whileInit c10 $ λ env → whileLoop env next open WhileTest createWhileTest : {m : Level} {t : Set m } → WhileTest {m} {t} createWhileTest = record { env = record { varn = 0; vari = 0 } } test2 : ℕ test2 = whileTest createWhileTest 10 $ λ e → vari e