|
1
|
1 whileTestP : {l : Level} {t : Set l} @$\rightarrow$@ (c10 : @$\mathbb{N}$@) @$\rightarrow$@ (Code : Envc @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
2 whileTestP c10 next = next (record {c10 = c10 ; varn = c10 ; vari = 0 })
|
|
|
3
|
|
|
4 whileLoopP' : {l : Level} {t : Set l} @$\rightarrow$@ Envc @$\rightarrow$@ (next : Envc @$\rightarrow$@ t) @$\rightarrow$@ (exit : Envc @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
5 whileLoopP' record { c10 = c10 ; varn = zero ; vari = vari } _ exit = exit record { c10 = c10 ; varn = zero ; vari = vari }
|
|
|
6 whileLoopP' record { c10 = c10 ; varn = suc varn1 ; vari = vari } next _ = next (record {c10 = c10 ; varn = varn1 ; vari = suc vari })
|
|
|
7
|
|
|
8 {-@$\#$@ TERMINATING @$\#$@-}
|
|
|
9 loopP : {l : Level} {t : Set l} @$\rightarrow$@ Envc @$\rightarrow$@ (exit : Envc @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
10 loopP env exit = whileLoopP' env (@$\lambda$@ env @$\rightarrow$@ loopP env exit ) exit
|
|
|
11
|
|
|
12 whileTestPCall : (c10 : @$\mathbb{N}$@ ) @$\rightarrow$@ Envc
|
|
|
13 whileTestPCall c10 = whileTestP {_} {_} c10 (@$\lambda$@ env @$\rightarrow$@ loopP env (@$\lambda$@ env @$\rightarrow$@ env))
|
|
|
14
|
|
|
15 -- whileTestPCall 10
|
|
|
16 -- record { c10 = 10 ; varn = 0 ; vari = 10 }
|
