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 : @$\mathbb{N}$@
    vari : @$\mathbb{N}$@
open Env

record WhileTest {m : Level }  {t : Set m }  : Set (Suc m) where
  field
    env : Env
  whileInit : (c10 : @$\mathbb{N}$@) @$\rightarrow$@ (Env @$\rightarrow$@ t) @$\rightarrow$@ t
  whileInit c10 next = next (record {varn = c10 ; vari = 0 } )
  whileLoop : Env @$\rightarrow$@ (Code : Env @$\rightarrow$@ t) @$\rightarrow$@ t
  whileLoop env next = whileLoop1 (varn env) env where
      whileLoop1 : @$\mathbb{N}$@ @$\rightarrow$@ Env @$\rightarrow$@ t
      whileLoop1 zero env =  next env
      whileLoop1 (suc t ) env = 
          whileLoop1 t (record env {varn = t ; vari = (vari env) + 1}) 
  whileTest : (c10 : @$\mathbb{N}$@) @$\rightarrow$@ (Env @$\rightarrow$@ t) @$\rightarrow$@ t
  whileTest c10 next = whileInit c10 $ @$\lambda$@ env @$\rightarrow$@ whileLoop env next

open WhileTest

createWhileTest : {m : Level} {t : Set m }  @$\rightarrow$@ WhileTest {m} {t}
createWhileTest  = record { env = record { varn = 0; vari = 0 } }

test2 : @$\mathbb{N}$@
test2 = whileTest createWhileTest 10 $ @$\lambda$@ e @$\rightarrow$@ vari e