module plfa.part2.Imperative where

open import Data.Bool using (Bool; true; false; not; _∧_; _∨_; if_then_else_; T)
open import Data.Maybe
open import Data.Nat using (ℕ)
open import Data.Product
open import Data.String
open import Data.Sum
open import Data.Unit using (⊤; tt)
open import Data.Empty using (⊥; ⊥-elim)
open import Function using (_∘_)
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; sym; subst)

{-

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 × Maybe Stmt → Set where

  Skp→ : ∀ {σ} → (σ , Skp) —→ (σ , nothing)

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

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

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


  -- while b s == if b then (s ; while b s) else skip


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

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

  Seq→₂ : ∀ {σ σ′ s₁ s₂} →
        (σ , s₁) —→ (σ′ , nothing)
        ---------------------------------
      → (σ , Seq s₁ s₂) —→ (σ′ , just 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

-- now: denotation of a statement is `State → M State`

𝓢⟦_⟧ : Stmt → State → M State
𝓢⟦ 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) = if (𝓑⟦ b ⟧ σ) then (𝓢⟦ s ⟧ σ ⟫= (λ σ _ → 𝓢⟦ s₀ ⟧ σ i)) i else (just σ)
𝓢⟦ Seq s₁ s₂ ⟧ σ = 𝓢⟦ s₁ ⟧ σ ⟫= 𝓢⟦ s₂ ⟧

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

data ⟪_⟫_⟪_⟫ : Pred State → Stmt → Pred State → Set₁ where

-- hoare-soundness