module whiletest where

open import Data.Nat
open import Data.Bool
open import Function
open import Relation.Binary.PropositionalEquality

open import utilities hiding ( _/\_ )

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

-- Envのvariやvarnの代入を行う関数
PrimComm : Set
PrimComm = Env → Env

Cond : Set
Cond = (Env → Bool) 

-- ここから先のコメントがなかった

Axiom : Cond -> PrimComm -> Cond -> Set
Axiom pre comm post = ∀ (env : Env) →  (pre env) ⇒ ( post (comm env)) ≡ true

Tautology : Cond -> Cond -> Set
Tautology pre post = ∀ (env : Env) →  (pre env)  ⇒ (post env) ≡ true

_and_ :  Cond -> Cond -> Cond
x and y =  λ env → x env ∧ y env 

neg :  Cond -> Cond
neg x  =  λ env → not ( x env )

open import Hoare PrimComm Cond Axiom Tautology _and_ neg

-- 実装開始
-- ここでは実行停止の定義などはしていない
-- numにループ回数をいれる感じか
program : ℕ → Comm
program loop_num  =
  Seq ( PComm (λ env → record env {varn = loop_num}))
    $ Seq ( PComm (λ env → record env {vari = 0})) -- ここまで入力
    $ While (λ env → lt zero (varn env ) ) -- 大小比較をしている
      (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} ))
        $ PComm (λ env → record env {varn = ((varn env) - 1)} ))
        
-- 実行するための定義
-- この定義では停止しないのでTERMINATINGが必要
-- コマンドがdata型なので全部の場合の記述をする
{-# TERMINATING #-}
interpret : Env → Comm → Env
interpret env Skip = env
interpret env Abort = env
interpret env (PComm x) = x env
interpret env (Seq comm comm1) = interpret (interpret env comm) comm1
interpret env (If x then else) with x env
... | true = interpret env then
... | false = interpret env else
interpret env (While x comm) with x env
... | true = interpret (interpret env comm) (While x comm)
... | false = env

-- 実行
test : Env
test = interpret ( record { vari = 0 ; varn = 10 } ) (program 10)

-- 実行はできた
-- 事前、事後条件を検証していく。これができるとHoare Logicを名乗っても良い