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