module Imperative-Hoare where

open import Data.Bool using (Bool; true; false; not; _∧_; _∨_; if_then_else_; T)
open import Data.Maybe
open import Data.Nat using (ℕ; zero; suc; _≤ᵇ_; _<ᵇ_; _+_; _≤_ ; z≤n ; s≤s)
import Data.Nat.Properties as P
open import Data.Product
open import Data.String using (String; _≟_)
open import Data.Sum
open import Data.Unit using (⊤; tt)
open import Data.Empty using (⊥; ⊥-elim)
open import Function using (_∘_; case_of_) renaming (case_return_of_ to case_ret_of_)
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; sym; subst; cong)

{-

syntax of the classical while language

e ::= c | x | e ⊕ e
b ::= e ∼ e | not b | b and b | b or b
s ::=
  skip |
  x := e |
  if b then s else s |
  while b do s |
  s ; s

-}

-- formal syntax of the While language

Ident = String

Op : Set → Set
Op A = A → A → A

BOp : Set → Set
BOp A = A → A → Bool

data Expr : Set where
  `#_ : (n : ℕ) → Expr
  `_  : (x : Ident) → Expr
  _⟨_⟩_ : (e₁ : Expr) → (⊕ : Op ℕ) → (e₂ : Expr) → Expr

data BExpr : Set where
  `not : (b : BExpr) → BExpr
  `and `or : (b₁ : BExpr) → (b₂ : BExpr) → BExpr
  _⟨_⟩_ : (e₁ : Expr) → (∼ : BOp ℕ) → (e₂ : Expr) → BExpr

data Stmt : Set where
  Skp : Stmt
  Ass : (x : Ident) → (e : Expr) → Stmt
  Ite : (b : BExpr) → (s₁ : Stmt) → (s₂ : Stmt) → Stmt
  Whl : (b : BExpr) → (s : Stmt) → Stmt
  Seq : (s₁ : Stmt) → (s₂ : Stmt) → Stmt

-- semantics I : small-step operational

{-
a configuration of the semantics comprises two parts
1. the values of the variables: the state - a mapping of variables to values
2. the current statement

Idea of the semantics:
transform the statement, one atomic statement at a time
and keep track of the state as it is transformed by each statement

the state is initialized to all zeroes
a program run corresponds to a sequence of configurations
-}

State = Ident → ℕ

update : Ident → ℕ → State → State
update x n σ y
  with x ≟ y
... | yes x≡y = n
... | no  _   = σ y

-- a denotational semantics for expressions

-- directly maps an expression to its denotation (i.e., a function from state to numbers)
-- need the state to look up the values of  variablee
-- (we could do it using small-step semantics, but it's not our focus today)
-- the bracket ⟦_⟧ usually enclose the syntactic phrase that is interpreted
-- the definition is *compositional*, that is,
--   the semantics of an expression is defined as a function of the semantics of its subexpressions.

𝓔⟦_⟧ : Expr → State → ℕ
𝓔⟦ `# n ⟧ σ = n
𝓔⟦ ` x ⟧ σ = σ x
𝓔⟦ e₁ ⟨ _⊕_ ⟩ e₂ ⟧ σ = 𝓔⟦ e₁ ⟧ σ ⊕ 𝓔⟦ e₂ ⟧ σ

𝓑⟦_⟧ : BExpr → State → Bool
𝓑⟦ `not b ⟧ σ = not (𝓑⟦ b ⟧ σ)
𝓑⟦ `and b b₁ ⟧ σ = 𝓑⟦ b ⟧ σ ∧ 𝓑⟦ b₁ ⟧ σ
𝓑⟦ `or b b₁ ⟧ σ = 𝓑⟦ b ⟧ σ ∨ 𝓑⟦ b₁ ⟧ σ
𝓑⟦ e₁ ⟨ _relop_ ⟩ e₂ ⟧ σ = 𝓔⟦ e₁ ⟧ σ relop 𝓔⟦ e₂ ⟧ σ

-- a small-step reduction relation for statements

-- data Maybe (A : Set) : Set where
--   nothing : Maybe A
--   just    : A → Maybe A

data _—→_ : State × Stmt → State × Stmt → Set where

  Ass→ : ∀ {σ}{x}{e} →
        (σ , Ass x e) —→ (update x (𝓔⟦ e ⟧ σ) σ , Skp)

  Ite→₁ : ∀ {σ}{b}{s₁}{s₂} →
         𝓑⟦ b ⟧ σ ≡ true →
        (σ , Ite b s₁ s₂) —→ (σ , s₁)

  Ite→₂ : ∀ {σ}{b}{s₁}{s₂} →
         𝓑⟦ b ⟧ σ ≡ false →
        (σ , Ite b s₁ s₂) —→ (σ , s₂)

  Whl→ : ∀ {σ}{b}{s} →
       (σ , Whl b s) —→ (σ , Ite b (Seq s (Whl b s)) Skp)

  Seq→₁ : ∀ {σ σ′ s₁ s₁′ s₂} →
        (σ , s₁) —→ (σ′ , s₁′)
        ---------------------------------
      → (σ , Seq s₁ s₂) —→ (σ′ , Seq s₁′ s₂)

  Seq→₂ : ∀ {σ s₂}
      → (σ , Seq Skp s₂) —→ (σ , s₂)


-- denotationally

-- the denotation of a statement is a state transformer, i.e., a function State → State

𝓢′⟦_⟧ : Stmt → State → State
𝓢′⟦ Skp ⟧ σ = σ
𝓢′⟦ Ass x e ⟧ σ = update x (𝓔⟦ e ⟧ σ) σ
𝓢′⟦ Ite b s₁ s₂ ⟧ σ
  with 𝓑⟦ b ⟧ σ
... | true = 𝓢′⟦ s₁ ⟧ σ
... | false = 𝓢′⟦ s₂ ⟧ σ
𝓢′⟦ Whl b s ⟧ σ = {!!}
𝓢′⟦ Seq s₁ s₂ ⟧ = 𝓢′⟦ s₂ ⟧ ∘ 𝓢′⟦ s₁ ⟧

{-
cannot complete the case for while, because Agda does not let us use general recursion
which would be needed to define the semantics of while.
-}

{-
If we are not interested in diverging while programs, then we can get useful results by restricting
ourselves to arbitrary, finite numbers of unrolling of while statments.

Trick: instead of returning State, we return `ℕ → Maybe State`
Interpretation: The number bounds the number of iterations of any nesting of while loops in the program.
If we run out of iterations, then we return `nothing`.
-}

-- M : Set → Set
-- M A = ℕ → Maybe A

-- return : ∀ {A : Set} → A → M A
-- return x = λ i → just x

-- _⟫=_ : ∀ {A B : Set} → M A → (A → M B) → M B
-- (m ⟫= f) i
--   with m i
-- ... | nothing = nothing
-- ... | just a  = f a i

_⟫=_ : ∀ {A B : Set} → Maybe A → (A → Maybe B) → Maybe B
(m ⟫= f)
  with m
... | nothing = nothing
... | just a  = f a

-- 𝓢⟦ Skp ⟧ σ = return σ
-- 𝓢⟦ Ass x e ⟧ σ = return (update x (𝓔⟦ e ⟧ σ) σ)
-- 𝓢⟦ Ite b s s₁ ⟧ σ
--   with 𝓑⟦ b ⟧ σ
-- ... | true = 𝓢⟦ s ⟧ σ
-- ... | false = 𝓢⟦ s₁ ⟧ σ
-- 𝓢⟦ Whl b s ⟧ σ ℕ.zero = nothing
-- 𝓢⟦ s₀@(Whl b s) ⟧ σ (ℕ.suc i) = 𝓢⟦ Ite b (Seq s (Whl b s)) Skp ⟧ σ i
-- 𝓢⟦ Seq s₁ s₂ ⟧ σ = 𝓢⟦ s₁ ⟧ σ ⟫= 𝓢⟦ s₂ ⟧

𝓢⟦_⟧ : Stmt → ℕ → State → Maybe State
𝓢⟦ s           ⟧ zero    σ = nothing
𝓢⟦ Skp         ⟧ (suc i) σ = just σ
𝓢⟦ Ass x e     ⟧ (suc i) σ = just (update x (𝓔⟦ e ⟧ σ) σ)
𝓢⟦ Ite b s₁ s₂ ⟧ (suc i) σ with 𝓑⟦ b ⟧ σ
...                           | true  = 𝓢⟦ s₁ ⟧ i σ
...                           | false = 𝓢⟦ s₂ ⟧ i σ
𝓢⟦ Whl b s     ⟧ (suc i) σ = 𝓢⟦ Ite b (Seq s (Whl b s)) Skp ⟧ i σ
𝓢⟦ Seq s₁ s₂   ⟧ (suc i) σ = 𝓢⟦ s₁ ⟧ i σ ⟫= 𝓢⟦ s₂ ⟧ i

----------------------------------------------------------------------
-- verification of while programs
-- using Hoare calculus

{-
Hoare calculus is a logical calculus with judgments of the form

{ P } s { Q }        (a "Hoare triple")

P - a precondition, a logical formula
Q - a postcondition, a logical formula
s - a statement

Intended meaning:
If we run s in a state σ such that P σ (σ satisfies the precondition)
and s terminates in state σ′, then Q σ′ (σ' satisfies the postcondition)

-}

Pred : Set → Set₁
Pred A = A → Set

_⇒_ : ∀ {A : Set } → Pred A → Pred A → Set
P ⇒ Q = ∀ a → P a → Q a



data ⟪_⟫_⟪_⟫ : Pred State → Stmt → Pred State → Set₁ where
  H-Skp : ∀ {P} →
    ⟪ P ⟫ Skp ⟪ P ⟫
  H-Ass : ∀ {Q x e} →
    ⟪ (λ σ → Q (update x (𝓔⟦ e ⟧ σ) σ)) ⟫ (Ass x e) ⟪ Q ⟫
  H-Ite : ∀ {P Q b s₁ s₂} →
    ⟪ (λ σ → P σ × 𝓑⟦ b ⟧ σ ≡ true ) ⟫ s₁ ⟪ Q ⟫ →
    ⟪ (λ σ → P σ × 𝓑⟦ b ⟧ σ ≡ false) ⟫ s₂ ⟪ Q ⟫ →
    ⟪ P ⟫ (Ite b s₁ s₂) ⟪ Q ⟫
  H-Whl : ∀ {P b s} →
    ⟪ (λ σ → P σ × 𝓑⟦ b ⟧ σ ≡ true) ⟫ s ⟪ P ⟫ →
    ⟪ P ⟫ (Whl b s) ⟪ (λ σ → P σ × 𝓑⟦ b ⟧ σ ≡ false) ⟫
  H-Seq : ∀ {P Q R s₁ s₂} →
    ⟪ P ⟫ s₁ ⟪ Q ⟫ →
    ⟪ Q ⟫ s₂ ⟪ R ⟫ →
    ⟪ P ⟫ (Seq s₁ s₂) ⟪ R ⟫
  H-Wea : ∀ {P₁ P₂ Q₁ Q₂ s} →
    P₁ ⇒ P₂ → ⟪ P₂ ⟫ s ⟪ Q₁ ⟫ → Q₁ ⇒ Q₂ →
    ⟪ P₁ ⟫ s ⟪ Q₂ ⟫

module Example where
  prog : Stmt                                     -- ⟪ x <= 5 ⟫
  prog = Whl ((` "x") ⟨ _<ᵇ_ ⟩ (`# 5) )           --   while x < 5 { x = x + 1 }
           (Ass "x" ((`# 1) ⟨ _+_ ⟩ (` "x")))     -- ⟪ x = 5 ⟫

  hoare : ⟪ (λ σ → (σ "x" ≤ᵇ 5) ≡ true) ⟫
            prog
          ⟪ (λ σ → σ "x" ≡ 5) ⟫
  hoare = H-Wea (λ σ x → x)
                (H-Whl {P = λ σ → (σ "x" ≤ᵇ 5) ≡ true}
                  (H-Wea (λ a (x≤5 , x<5) → x<5)
                         H-Ass
                         λ a x → x))
                {!!}

lem' : ∀ i σ σ′ → 𝓢⟦ Skp ⟧ i σ ≡ just σ′ → σ ≡ σ′
lem' (suc i) σ σ′ refl = refl

hoare-soundness : ∀ {P Q s} →
  ⟪ P ⟫ s ⟪ Q ⟫ →
  ∀ σ → P σ → ∀ i → ∀ σ′ → 𝓢⟦ s ⟧ i σ ≡ just σ′ → Q σ′
hoare-soundness H-Skp          σ Pσ (suc i) .σ refl = Pσ
hoare-soundness H-Ass          σ Pσ (suc i) σ′ refl = Pσ
hoare-soundness (H-Ite {b = b} H₁ H₂)  σ Pσ (suc i) σ′ eq with 𝓑⟦ b ⟧ σ in eq-b
...                                                          | true  = hoare-soundness H₁ σ (Pσ , eq-b) i σ′ eq
...                                                          | false = hoare-soundness H₂ σ (Pσ , eq-b) i σ′ eq
hoare-soundness (H-Whl {b = b} {s = s} H)      σ Pσ (suc (suc i)) σ′ eq
 with 𝓑⟦ b ⟧ σ in eq-b
... | false rewrite sym (lem' i σ σ′ eq) = Pσ , eq-b
... | true
 with i
... | suc i
 with 𝓢⟦ s ⟧ i σ in eq-s
... | just σ′′
 with hoare-soundness H σ (Pσ , eq-b) i σ′′ eq-s
... | Pσ′′
 = hoare-soundness (H-Whl H) σ′′ Pσ′′ i σ′ eq
hoare-soundness (H-Seq {s₁ = s₁} {s₂ = s₂} H₁ H₂)  σ Pσ (suc i) σ′ eq₂
 with 𝓢⟦ s₁ ⟧ i σ in eq₁
... | just σ′′ = let Pσ′′ = hoare-soundness H₁ σ Pσ i σ′′ eq₁
                 in hoare-soundness H₂ σ′′ Pσ′′ i σ′ eq₂
hoare-soundness (H-Wea pre H post) σ Pσ (suc i) σ′ eq = post σ′ (hoare-soundness H σ (pre σ Pσ) (suc i) σ′ eq)

soundness : ∀ {σ₁ s₁ σ₂ s₂} →
  (σ₁ , s₁) —→ (σ₂ , s₂) →
  ∀ i → 𝓢⟦ s₁ ⟧ i σ₁ ≡ 𝓢⟦ s₂ ⟧ i σ₂
soundness r i = {!!}

data _⇓_ : State × Stmt → State → Set where
  step : ∀ {σ}{σ′}{σ″}{s}{s′} →
    (σ , s) —→ (σ′ , s′) →
    (σ′ , s′) ⇓ σ″ →
    (σ , s) ⇓ σ″
  done : ∀ {σ} →
    (σ , Skp) ⇓ σ

completeness : ∀ {i} {s}{σ}{σ′} →
  𝓢⟦ s ⟧ i σ ≡ just σ′ →
  (σ , s) ⇓ σ′
completeness {i = i} {s = s} eq = {!!}



































𝓢-suc : ∀ {i j} σ s σ' →
  i ≤ j →
  𝓢⟦ s ⟧ i σ ≡ just σ' →
  𝓢⟦ s ⟧ j σ ≡ just σ'
𝓢-suc {i = i} {j = j} σ s σ' i≤j eq = {!!}

n≤sn : ∀ {i} → i ≤ suc i
n≤sn = P.≤-step P.≤-refl

lem : ∀ s i σ →
  𝓢⟦ s ⟧ i σ ≡ nothing ⊎ 𝓢⟦ s ⟧ i σ ≡ 𝓢⟦ s ⟧ (suc i) σ
lem s i σ with 𝓢⟦ s ⟧ i σ in eq
... | nothing = inj₁ refl
... | just σ' = inj₂ (sym (𝓢-suc σ s σ' n≤sn eq))



combine-⇓ : ∀ {s₁}{s₂}{σ}{σ″}{σ′} → (σ , s₁) ⇓ σ″ → (σ″ , s₂) ⇓ σ′ → (σ , Seq s₁ s₂) ⇓ σ′
combine-⇓ (step x s₁⇓) s₂⇓ = step (Seq→₁ x) (combine-⇓ s₁⇓ s₂⇓)
combine-⇓ done s₂⇓         = step Seq→₂ s₂⇓