module whileTest where

open import Data.Nat
open import Data.Bool


record Env : Set where
  field
    varn : ℕ
    vari : ℕ
open Env

data PrimComm  : Set where
  command : (Env → Env) → PrimComm
--  seti : (v : ℕ) → PrimComm (record  {varn = {!!} ; vari = {!!}} )

data Cond : Set where
  cond : (Env → Bool) → Cond 

open import Hoare Cond PrimComm {!!} {!!} {!!} Env {!!} {!!} {!!} {!!} {!!} {!!} {!!}

program : Comm
program = 
    Seq ( PComm (command (λ env → record env {varn = 10})))
    (Seq ( PComm (command (λ env → record env {vari = 0})))
    (While (cond (λ env → {!!} ))
      (Seq (PComm (command (λ env → record env {vari = ((vari env) + 1)} )))
        (PComm (command (λ env → record env {varn = ((varn env) + 1)} ))))))

-- {#- TERMINATION -#}
interpreter : Env → Comm → Env
interpreter env Skip = env
interpreter env Abort = env
interpreter env (PComm (command x)) = x env
interpreter env (Seq comm comm1) = interpreter (interpreter env comm) comm1
interpreter env (If (cond x) then else) with x env
... | true = interpreter env then
... | false = interpreter env else
interpreter env (While (cond x) comm) with x env
... | true = interpreter (interpreter env comm) (While (cond x) comm)
... | false = env


proof1 : HTProof {!!} program {!!}
proof1 = {!!}