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

--open import Data.Bool hiding ( _≟_ ) -- ; _≤?_ ; _≤_ ; _<_)
--open import Relation.Binary.PropositionalEquality
open import Agda.Builtin.Unit

record Env : Set (Suc Zero) where
  field
    varn : ℕ
    vari : ℕ
open Env

data _implies_  (A B : Set ) : Set (Suc Zero) where
    proof : ( A → B ) → A implies B

data whileTestState  : Set where
  s1 : whileTestState
  s2 : whileTestState
  sf : whileTestState

whileTestStateP : whileTestState → Env → ℕ → Set
whileTestStateP s1 env c10 = (vari env ≡ 0) ∧ (varn env ≡ c10)
whileTestStateP s2 env c10 = (varn env + vari env ≡ c10 )
whileTestStateP sf env c10 = (vari env ≡ c10)

record WhileTest {m : Level }  {t : Set m }  : Set (Suc m) where
  field
    env : Env
  whileInit :  {m : Level }  {t : Set m } → (c10 : ℕ) → (Env → t) → t
  whileInit c10 next = next (record {varn = c10 ; vari = 0 } )
  whileInit-imple : (c10 : ℕ) → whileInit c10 (λ env → ⊤ implies (whileTestStateP s1 env c10) )
  whileInit-imple c = proof ( λ _ → record { proj1 = refl ; proj2 = refl } )
  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

---

{-
whileTestStateP : whileTestState → Envc →  Set
whileTestStateP s1 env = (vari env ≡ 0) /\ (varn env ≡ c10 env)
whileTestStateP s2 env = (varn env + vari env ≡ c10 env)
whileTestStateP sf env = (vari env ≡ c10 env)

whileTestP : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : Envc → t) → t
whileTestP c10 next = next (record {varn = c10 ; vari = 0 ; c10 = c10 } )

whileTestPSem :  (c : ℕ) → whileTestP c ( λ env → ⊤ implies (whileTestStateP s1 env) )
whileTestPSem c = proof ( λ _ → record { pi1 = refl ; pi2 = refl } )
-}