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