Making NatSem compositional and denotational!

NatSem.agda

module Semwap.NatSem where

open import Prelude hiding (force)
open import Prelude.Extras.Eq
open import Prelude.Extras.Delay

import Level

open import Semwap.Expr


-- While language as extracted form Table  2.1
data While : Set where
  _:=_ : Var → Aexp → While
  skip : While
  _∶_ : While → While → While
  if'_then_else_ : Bexp → While → While → While
  while_run_ : Bexp → While → While

-- kinda abirtaty
infix 2 _:=_
-- ∶ is right assosiative
infixr 1 _∶_


-- The actual natural semantic function as extracted from Table 2.1
-- Here Delay gives us the possibility of reasoning about non termination
Domain : Size → Set
Domain i = State → Delay State i

open import Codata.Thunk hiding (extract; cofix)
open import Relation.Unary

module _ {p} (P : Size → Set p) where
  cofix : ∀[ Thunk P ⇒ P ] → ∀[ P ]
  cofix f = f aux module Cofix where
    aux = λ where .force → cofix f
    -- aux : Thunk P _
    -- aux .force = cofix f

mutual
  -- defined separately because of some technicalites with pattern matching
  -- lambdas
  natSemLoop : ∀ {i} → While → Thunk (λ j → State → Delay State j) i → State → Thunk (Delay State) i
  natSemLoop S rec s .force = ((Sₙₛ⟦ S ⟧ s) >>= force rec)
  natSemLoopAux : ∀ {i} → While → Thunk (λ j → State → Delay State j) i → State → Delay State i
  natSemLoopAux S rec s = later (natSemLoop S rec s)

  whileSem : Bexp → While → ∀[ Thunk Domain ⇒ Domain ]
  whileSem guard S rec s =
    if ℬ⟦ guard ⟧ s
    then natSemLoopAux S rec s
    else now s

  Sₙₛ⟦_⟧_ : ∀ {i} → While → State → Delay State i
  Sₙₛ⟦ x := a ⟧  s = now (s [ x ↦ (𝓐⟦ a ⟧ s) ])
  Sₙₛ⟦ skip ⟧ s = now s
  Sₙₛ⟦ w₁ ∶ w₂ ⟧  s =
    (Sₙₛ⟦ w₁ ⟧ s) >>= Sₙₛ⟦ w₂ ⟧_
  Sₙₛ⟦ if' guard then S₁ else S₂ ⟧ s =
    if ℬ⟦ guard ⟧ s
    then Sₙₛ⟦ S₁ ⟧ s
    else Sₙₛ⟦ S₂ ⟧ s
  Sₙₛ⟦ while guard run S ⟧ s = cofix Domain (whileSem guard S) s
    where

-- The natural semantic relation as defined in chapter 2. The relations says
-- that ⟨ S 、 s ⟩⇾ s' is valid if S executed with s terminates and the final
-- state is s' Here we encode it by saying that there exists a proof of
-- termination and the results is equivalent to s'
-- ⟨_⸴_⟩⇾_ : While → State → State → Set
-- ⟨_⸴_⟩⇾_ S s s' =
--  Σ (natSem S s ⇓) (λ d → Delay.extract d ≡ s')

record ⟨_,_⟩⇾_ (S : While) (s : State) (s' : State) : Set where
  inductive
  constructor nsTuple_
  field
     nsTuple' :  Σ (Sₙₛ⟦ S ⟧ s ⇓) (λ d → extract d ≡ s')
open ⟨_,_⟩⇾_ {{...}} public

-- Utilies on Natural semantics tuple

-- Also Theorem 2.9
-- The resulting value of two semantic tuples with the same statement and
-- starting state are unique
result-sem-unique :
  {S : While} {s s' s'' : State}
  → ⟨ S , s ⟩⇾ s' → ⟨ S , s ⟩⇾ s''
  → s' ≡ s''
result-sem-unique {S} (nsTuple (Sₗ⇓ , S⇾s')) (nsTuple (Sᵣ⇓ , S⇾s''))
  rewrite ⇓-unique Sₗ⇓ Sᵣ⇓ = (sym S⇾s') ⟨≡⟩ S⇾s''

-- result-sem-unique' :
--   {S : While} {s s' s'' : State}
--   → ⟨ S , s ⟩⇾ s' ≡ ⟨ S , s ⟩⇾ s''
-- result-sem-unique' {skip} {s} = refl

-- Semantic rules as defined in Table 2.1
[assₙₛ] : ∀ {x a s} → ⟨ (x := a) , s ⟩⇾ (s [ x ↦ 𝓐⟦ a ⟧ s ])
[assₙₛ] {x} {a} {s} =
  nsTuple
    ( now (s [ x ↦ (𝓐⟦ a ⟧ s) ])
    , refl
    )


[skipₙₛ] : ∀ {s} →  ⟨ skip , s ⟩⇾ s
[skipₙₛ] {s} = nsTuple (now s , refl)

[compₙₛ] :
  ∀ {S₁ S₂ s s' s''}
  → (⟨ S₁ , s ⟩⇾ s') → (⟨ S₂ , s' ⟩⇾ s'')
  → ⟨ S₁ ∶ S₂ , s ⟩⇾ s''
[compₙₛ] {S₁} {S₂} {s} {s'} {s''}
         (nsTuple ( S₁⇓ , S₁⇾s' ))
         (nsTuple ( S₂⇓ , S₂⇾s'' ))
  rewrite (sym S₁⇾s')
  =
   nsTuple
   ( bind-⇓ S₁⇓ S₂⇓
   , (extract (bind-⇓ S₁⇓ S₂⇓)
   ≡⟨ extract-bind S₁⇓ S₂⇓ ⟩
     extract S₂⇓
   ≡⟨ S₂⇾s'' ⟩
     s''
   ∎))

[ifₙₛᵗᵗ] :
  ∀ {S₁ S₂ s s' b}
  → (ℬ⟦ b ⟧ s ≡ true) → ⟨ S₁ , s ⟩⇾ s'
  → ⟨ if' b then S₁ else S₂ , s ⟩⇾ s'
[ifₙₛᵗᵗ] {S₁} {S₂} {s} {s'} {b} ℬ⟦b⟧s≡true (nsTuple (S₁⇓ , S₁⇾s'))
  rewrite (sym (cong (if_then Sₙₛ⟦ S₁ ⟧ s else Sₙₛ⟦ S₂ ⟧ s) ℬ⟦b⟧s≡true)) =
  nsTuple (S₁⇓ , S₁⇾s')

[ifₙₛᶠᶠ] :
  ∀ {S₁ S₂ s s' b}
  → (ℬ⟦ b ⟧ s ≡ false)
  → ⟨ S₂ , s ⟩⇾ s'
  → ⟨ if' b then S₁ else S₂ , s ⟩⇾ s'
[ifₙₛᶠᶠ] {S₁} {S₂} {s} {s'} {b} ℬ⟦b⟧s≡false (nsTuple (S₂⇓ , S₂⇾s'))
  rewrite (sym (cong (if_then Sₙₛ⟦ S₁ ⟧ s else Sₙₛ⟦ S₂ ⟧ s) ℬ⟦b⟧s≡false)) =
   nsTuple ( S₂⇓ , S₂⇾s')

[whileₙₛᵗᵗ] :
  ∀ {b S s s' s''}
  → (ℬ⟦ b ⟧ s ≡ true)
  → ⟨ S , s ⟩⇾ s'
  → ⟨ while b run S , s' ⟩⇾ s''
  → ⟨ while b run S , s ⟩⇾ s''
[whileₙₛᵗᵗ] {b} {S} {s} {s'} {s''} ℬ⟦b⟧s≡true (nsTuple (S⇓ , S⇾s')) (nsTuple (WS⇓ , WS⇾s''))
  rewrite (sym S⇾s')
    =
    solve (later (bind-⇓ S⇓ WS⇓))
          ( extract {d = inner-recur} (later (bind-⇓ S⇓ WS⇓))
           ≡⟨ extract-bind S⇓ WS⇓ ⟩
             extract WS⇓
           ≡⟨ WS⇾s'' ⟩
             s''
            ∎
           )
  where
    inner-recur : Delay State ∞
    inner-recur = (natSemLoopAux S (Cofix.aux Domain (whileSem b S)) s)
    reduction : (if ℬ⟦ b ⟧ s then inner-recur else now s) ≡ inner-recur
    reduction = cong (if_then inner-recur else now s) ℬ⟦b⟧s≡true
    solve : (inner-recur⇓ : inner-recur ⇓)
          → extract inner-recur⇓ ≡ s''
          → ⟨ while b run S , s ⟩⇾ s''
    solve ir⇓ gives-s'' rewrite (sym reduction) = nsTuple ( ir⇓ , gives-s'')

-- [whileₙₛᶠᶠ] :
--   ∀ {S s b}
--   → (ℬ⟦ b ⟧ s ≡ false)
--   → ⟨ while b run S , s ⟩⇾ s
-- [whileₙₛᶠᶠ] {S} {s} {b} ℬ⟦b⟧s≡false =
--     solve (now s)
--           refl
--   where
--     inner-recur : Delay State ∞
--     inner-recur = later (natSemLoop b S s)
--     reduction : (if ℬ⟦ b ⟧ s then inner-recur else now s) ≡ now s
--     reduction = cong (if_then inner-recur else now s) ℬ⟦b⟧s≡false
--     solve : (inner-recur⇓ : now s ⇓)
--           → extract inner-recur⇓ ≡ s
--           → ⟨ while b run S , s ⟩⇾ s
--     solve ir⇓ gives-s'' rewrite (sym reduction) = nsTuple ( ir⇓ , gives-s'')

-- private
--   x y z : Var
--   x = 0
--   y = 1
--   z = 2

-- _ : ⟨ (x := 𝕟 1) , ε ⟩⇾ (ε [ x ↦ 1 ])
-- _ = [assₙₛ]


-- module _ where
--   private
--     s₀ s₁ s₂ s₃ : State
--     s₀ = (ε [ x ↦ 5 ]) [ y ↦ 7 ]
--     s₁ = s₀ [ z ↦ 5 ]
--     s₂ = s₁ [ x ↦ 7 ]
--     s₃ = s₂ [ y ↦ 5 ]

--   ex-2-1 : ⟨ ((z := 𝕧 x ∶ x := 𝕧 y) ∶ y := 𝕧 z) , s₀ ⟩⇾ s₃
--   ex-2-1 = [compₙₛ] ([compₙₛ] [assₙₛ] [assₙₛ]) [assₙₛ]


-- module _ where
--   private
--     s₀  : State
--     s₀ = ε [ x ↦ 3 ]

--   ex-2-2 : ⟨ (y := 𝕟 1 ∶ while !' (𝕧 x ==' 𝕟 1) run (y := 𝕧 y *' 𝕧 x ∶ x := 𝕧 x -' 𝕟 1)) , s₀ ⟩⇾ (s₀ [ y ↦ 6 ] [ x ↦ 1 ])
--   ex-2-2 = [compₙₛ] [assₙₛ]
--                    ([whileₙₛᵗᵗ] refl
--                               ([compₙₛ] [assₙₛ] [assₙₛ])
--                               ([whileₙₛᵗᵗ] refl
--                                          ([compₙₛ] [assₙₛ] [assₙₛ])
--                                          ([whileₙₛᶠᶠ] refl)))


-- module _ where
--   private
--     s₀ : State
--     s₀ = ε [ x ↦ 17 ] [ y ↦ 5 ]

--   ex-2-3 : ⟨ (z := 𝕟 0 ∶ while 𝕧 y <=' 𝕧 x run (z := 𝕧 z +' 𝕟 1 ∶ x := 𝕧 x -' 𝕧 y)) , s₀ ⟩⇾ _
--   ex-2-3 = [compₙₛ] [assₙₛ]
--                     ([whileₙₛᵗᵗ]
--                       refl
--                       ([compₙₛ] [assₙₛ] [assₙₛ])
--                       ([whileₙₛᵗᵗ]
--                         refl
--                         ([compₙₛ] [assₙₛ] [assₙₛ])
--                         ([whileₙₛᵗᵗ]
--                           refl
--                           ([compₙₛ] [assₙₛ] [assₙₛ])
--                           ([whileₙₛᶠᶠ] refl))))

-- -- Semantic equivalence

-- record _≡ₙₛ_ (S₁ S₂ : While) : Set where
--   constructor ns-eq
--   field
--     S₁⇒S₂ : ((s s' : State) → ⟨ S₁ , s ⟩⇾ s' → ⟨ S₂ , s ⟩⇾ s')
--     S₂⇒S₁ : ((s s' : State) → ⟨ S₂ , s ⟩⇾ s' → ⟨ S₁ , s ⟩⇾ s')


-- ≡ₙₛ-refl : {S : While} → (S ≡ₙₛ S)
-- ≡ₙₛ-refl =
--   ns-eq (λ s s' t → t) (λ s s' t → t)

-- ≡ₙₛ-sym : {S₁ S₂ : While} → S₁ ≡ₙₛ S₂ → S₂ ≡ₙₛ S₁
-- ≡ₙₛ-sym (ns-eq to from) = ns-eq from to

-- ≡ₙₛ-trans : {S₁ S₂ S₃ : While} → S₁ ≡ₙₛ S₂ → S₂ ≡ₙₛ S₃ → S₁ ≡ₙₛ S₃
-- ≡ₙₛ-trans (ns-eq to from) (ns-eq to' from') =
--   ns-eq (λ s s' S₁ → to' s s' (to s s' S₁))
--         (λ s s' S₃ → from s s' (from' s s' S₃))

-- -- ≡ₙₛ-cong {S₁ S₂ S₃ : While} (f :  → S₁ ≡ₙₛ S₂ → S₂ ≡ₙₛ S₃ → S₁ ≡ₙₛ S₃
-- --  If we know that a ⟨ while b run S , s ⟩⇾ s'' holds and that the boolean
-- -- guard is true in s then we can extract the proofs used to construct said
-- -- statement. That is, there exists a state `s'` such that `⟨ S , s ⟩⇾ s'` and
-- -- `⟨ while b run S , s' ⟩⇾ s''`
-- [whileₙₛᵗᵗ]-elim :
--   {b : Bexp} {S : While} {s s'' : State}
--   → ⟨ while b run S , s ⟩⇾ s'' → ℬ⟦ b ⟧ s ≡ true
--   → Σ State (λ s' → (⟨ S , s ⟩⇾ s') × ⟨ while b run S , s' ⟩⇾ s'')
-- [whileₙₛᵗᵗ]-elim {b} {S} {s} {s''} (nsTuple (WS⇓ , WS→s'')) ℬ⟦b⟧s≡true
--   rewrite ℬ⟦b⟧s≡true =
--   s'
--   , ((nsTuple (Sₙₛ⟦S⟧s⇓ , refl))
--   , (solve))
--   where
--     bind⇓ : bind (Sₙₛ⟦ S ⟧ s) (Sₙₛ⟦ while b run S ⟧_) ⇓
--     bind⇓ with inspect WS⇓
--     ...| (later d , _)  = d
--     Sₙₛ⟦S⟧s⇓ : Sₙₛ⟦ S ⟧ s ⇓
--     Sₙₛ⟦S⟧s⇓ = bind-⇓-injₗ bind⇓
--     s' : State
--     s' = extract Sₙₛ⟦S⟧s⇓

--     extract-bind⇓≡s'' : extract bind⇓ ≡ s''
--     extract-bind⇓≡s'' with inspect WS⇓ | inspect WS→s''
--     ...| (later d , ingraph WS⇓≡later) | (WS→s'' , _)
--       rewrite WS⇓≡later = WS→s''

--     Sₙₛ⟦while⟧s'⇓ : Sₙₛ⟦ while b run S ⟧ s' ⇓
--     Sₙₛ⟦while⟧s'⇓ = bind-⇓-injᵣ {d = (Sₙₛ⟦_⟧_ S s)} bind⇓

--     extract-Sₙₛ⟦while⟧s'⇓≡s'' : extract Sₙₛ⟦while⟧s'⇓ ≡ extract bind⇓
--     extract-Sₙₛ⟦while⟧s'⇓≡s'' =
--       extract-bind-⇓-injᵣ≡extract-bind-⇓ {d = (Sₙₛ⟦_⟧_ S s)} bind⇓
--     solve : _
--     solve with inspect (ℬ⟦ b ⟧ s')
--     ...| (false , ingraph ℬ⟦b⟧s'≡false) =
--          nsTuple ( Sₙₛ⟦while⟧s'⇓ , (trans extract-Sₙₛ⟦while⟧s'⇓≡s'' extract-bind⇓≡s''))
--     ...| (true , ingraph ℬ⟦b⟧s'≡true) =
--          nsTuple (bind-⇓-injᵣ {d = (Sₙₛ⟦_⟧_ S s)} bind⇓
--                  , (trans extract-Sₙₛ⟦while⟧s'⇓≡s'' extract-bind⇓≡s''))


-- [ifₙₛᵗᵗ]-elim :
--   {b : Bexp} {S₁ S₂ : While} {s s' : State}
--   → ⟨ if' b then S₁ else S₂ , s ⟩⇾ s' → ℬ⟦ b ⟧ s ≡ true
--   → ⟨ S₁ , s ⟩⇾ s'
-- [ifₙₛᵗᵗ]-elim {b} {S₁} {S₂} {s} {s'} (nsTuple (if⇓ , if→s')) ℬ⟦b⟧s≡true
--   rewrite ℬ⟦b⟧s≡true = nsTuple (if⇓ , if→s')

-- [ifₙₛᶠᶠ]-elim :
--   {b : Bexp} {S₁ S₂ : While} {s s' : State}
--   → ⟨ if' b then S₁ else S₂ , s ⟩⇾ s' → ℬ⟦ b ⟧ s ≡ true
--   → ⟨ S₁ , s ⟩⇾ s'
-- [ifₙₛᶠᶠ]-elim {b} {S₁} {S₂} {s} {s'} (nsTuple (if⇓ , if→s')) ℬ⟦b⟧s≡true
--   rewrite ℬ⟦b⟧s≡true = nsTuple (if⇓ , if→s')

-- [compₙₛ]-elim :
--   {S₁ S₂ : While} {s s'' : State}
--   → ⟨ S₁ ∶ S₂ , s ⟩⇾ s''
--   → Σ State (λ s' → ⟨ S₁ , s ⟩⇾ s' × ⟨ S₂ , s' ⟩⇾ s'')
-- [compₙₛ]-elim {S₁} {S₂} {s} {s''} (nsTuple (C⇓ , C⇾s'')) =
--   s'
--   , nsTuple (S₁⇓ , refl)
--   , (nsTuple ((bind-⇓-injᵣ {d = (Sₙₛ⟦ S₁ ⟧ s)} C⇓)
--              , trans (extract-bind-⇓-injᵣ≡extract-bind-⇓ {d = (Sₙₛ⟦ S₁ ⟧ s)} C⇓) C⇾s'')
--     )
--   where
--     S₁⇓ : Sₙₛ⟦ S₁ ⟧ s ⇓
--     S₁⇓ = bind-⇓-injₗ C⇓
--     s' : State
--     s' = extract S₁⇓


-- lem-2-5 : (b : Bexp) (S : While)
--         → (while b run S) ≡ₙₛ (if' b then (S ∶ while b run S) else skip)
-- lem-2-5 b S =
--   record { S₁⇒S₂ = while-to-unfold
--          ; S₂⇒S₁ = unfold-to-while
--          }
--   where
--     lhs = while b run S
--     rhs = if' b then (S ∶ while b run S) else skip
--     while-to-unfold : (s s'' : State) → ⟨ lhs , s ⟩⇾ s'' → ⟨ rhs , s ⟩⇾ s''
--     while-to-unfold s s'' (nsTuple (S⇓ , S→s''))
--       with inspect (ℬ⟦ b ⟧ s)
--     ...| (false , ingraph ℬ⟦b⟧s≡false)
--       rewrite ℬ⟦b⟧s≡false
--       rewrite (sym (cong (λ z → if z then (bind (Sₙₛ⟦ S ⟧ s) (λ s₁ → if ℬ⟦ b ⟧ s₁ then later (natSemLoop b S s₁) else now s₁)) else (now s)) ℬ⟦b⟧s≡false)) =

--         nsTuple (S⇓ , S→s'')
--     ...| (true , ingraph ℬ⟦b⟧s≡true ) =
--          let (s' , STuple , WhileTuple) = [whileₙₛᵗᵗ]-elim (nsTuple (S⇓ , S→s''))  ℬ⟦b⟧s≡true
--          in [ifₙₛᵗᵗ] ℬ⟦b⟧s≡true ([compₙₛ] STuple WhileTuple)

--     unfold-to-while : (s s'' : State) → ⟨ rhs , s ⟩⇾ s'' → ⟨ lhs , s ⟩⇾ s''
--     unfold-to-while s s'' (nsTuple (S⇓ , S→s''))
--       with inspect (ℬ⟦ b ⟧ s)
--     ...| (false , ingraph ℬ⟦b⟧s≡false)
--          rewrite ℬ⟦b⟧s≡false
--          rewrite trans (sym S→s'') (extract-now S⇓)  =
--            [whileₙₛᶠᶠ] ℬ⟦b⟧s≡false
--     ...| (true , ingraph ℬ⟦b⟧s≡true)
--          rewrite ℬ⟦b⟧s≡true =
--          let (s' , bodyTuple , whileTuple ) = [compₙₛ]-elim {S₁ = S}
--                                                             (nsTuple (S⇓ , S→s''))
--          in [whileₙₛᵗᵗ] ℬ⟦b⟧s≡true
--                        bodyTuple
--                        whileTuple


-- ex-2-6 : {S₁ S₂ S₃ : While} → (S₁ ∶ S₂ ∶ S₃) ≡ₙₛ ((S₁ ∶ S₂) ∶ S₃)
-- ex-2-6 {S₁} {S₂} {S₃} =
--   ns-eq (λ s s''' ⟨S₁∶S₂∶S₃,s⟩⇾s''' →
--            let (s' , ⟨S₁,s⟩⇾s' , ⟨S₂∶S₃,s'⟩⇾s''') = [compₙₛ]-elim ⟨S₁∶S₂∶S₃,s⟩⇾s'''
--                (s'' , ⟨S₂,s'⟩⇾s'' , ⟨S₃,s''⟩⇾s''') = [compₙₛ]-elim ⟨S₂∶S₃,s'⟩⇾s'''
--            in [compₙₛ] ([compₙₛ] ⟨S₁,s⟩⇾s' ⟨S₂,s'⟩⇾s'') ⟨S₃,s''⟩⇾s'''
--         )
--         (λ s s''' ⟨[S₁∶S₂]∶S₃,s⟩⇾s''' →
--            let (s' , ⟨S₁∶S₂,s⟩⇾s'' , ⟨S₃,s''⟩⇾s''') = [compₙₛ]-elim ⟨[S₁∶S₂]∶S₃,s⟩⇾s'''
--                (s'' , ⟨S₁,s⟩⇾s' , ⟨S₂,s'⟩⇾s'') = [compₙₛ]-elim ⟨S₁∶S₂,s⟩⇾s''
--            in [compₙₛ] ⟨S₁,s⟩⇾s' ([compₙₛ] ⟨S₂,s'⟩⇾s'' ⟨S₃,s''⟩⇾s''')
--         )

-- -- For later
-- ex-2-13 : {S₁ S₂ : While} → S₁ ≡ₙₛ S₂ → ((s : State) → Sₙₛ⟦ S₁ ⟧ s ≡ Sₙₛ⟦ S₂ ⟧ s)
-- ex-2-13  (ns-eq to from) = {!!}

-- --≡ₙₛ-refl : {S : While} {s s' : State} → (⟨ S , s ⟩⇾ s' ≡ ⟨ S , s ⟩⇾ s')
-- --≡ₙₛ-refl = refl