module whileTest where

open import Data.Nat
open import Data.Bool hiding (_≟_)
open import Data.Product
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import SET
import Level

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

PrimComm = Env → Env

Cond = Env → Bool

neg : (Env → Bool) → (Env → Bool)
neg x e = not (x e)
 
and : (Env → Bool) → (Env → Bool)  → (Env → Bool)
and x y e = (x e) ∧ (y e)

data Comm : Set where
  Skip  : Comm
  Abort : Comm
  PComm : PrimComm -> Comm
  Seq   : Comm -> Comm -> Comm
  If    : Cond -> Comm -> Comm -> Comm
  While : Cond -> Comm -> Comm

data HTProof : Cond -> Comm -> Cond -> Set (Level.suc (Level.suc Level.zero)) where
  PrimRule : {bPre : Cond} -> {pcm : PrimComm} -> {bPost : Cond} ->
             (pr :  Cond -> PrimComm -> Cond -> Set (Level.suc Level.zero)) ->
             HTProof bPre (PComm pcm) bPost
  SkipRule : (b : Cond) -> HTProof b Skip b
  AbortRule : (bPre : Cond) -> (bPost : Cond) ->
              HTProof bPre Abort bPost
  WeakeningRule : {bPre : Cond} -> {bPre' : Cond} -> {cm : Comm} ->
                {bPost' : Cond} -> {bPost : Cond} ->
                bPre ≡ bPre' ->
                HTProof bPre' cm bPost' ->
                bPost' ≡ bPost ->
                HTProof bPre cm bPost
  SeqRule : {bPre : Cond} -> {cm1 : Comm} -> {bMid : Cond} ->
            {cm2 : Comm} -> {bPost : Cond} ->
            HTProof bPre cm1 bMid ->
            HTProof bMid cm2 bPost ->
            HTProof bPre (Seq cm1 cm2) bPost
  IfRule : {cmThen : Comm} -> {cmElse : Comm} ->
           {bPre : Cond} -> {bPost : Cond} ->
           {b : Cond} ->
           HTProof (and bPre b) cmThen bPost ->
           HTProof (and bPre (neg b)) cmElse bPost ->
           HTProof bPre (If b cmThen cmElse) bPost
  WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} ->
              HTProof (and bInv b) cm bInv ->
              HTProof bInv (While b cm) (and bInv (neg b))
  Rule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} -> {w : Cond} ->
              HTProof w cm bInv ->
              HTProof bInv (While b cm) (and bInv (neg b))


lt : ℕ → ℕ → Bool
lt x y with x <? y
lt x y | yes p = true
lt x y | no ¬p = false

_-_ : ℕ → ℕ → ℕ
x - zero = x
zero - (suc _) = zero
(suc x) - (suc y) = x - y

_==_ : ℕ → ℕ → Bool
x == y with x ≟ y
(x == y) | yes p = true
(x == y) | no ¬p = false


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

{-# 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

test1 = interpret (record {vari = 0 ; varn = 0}) program

initCond : Env → Bool
initCond _ = true

termCond : Env → Bool
termCond env = (vari env) == 10

iff : Bool → Bool → Bool
iff true true = true
iff false false = true
iff _ _ = false

proposition1 : Cond → PrimComm → Cond → Env → Set
proposition1 pre cmd post = λ (env : Env) → {!!} -- iff (pre env) (post (cmd env))

proof1 : HTProof initCond program termCond
proof1 = SeqRule (PrimRule {!!} )
         (SeqRule (PrimRule {!!} )
         (Rule {!!}  (WhileRule ?)))