------------------------------------------------------------------------
-- The "bar theorem"
------------------------------------------------------------------------

module Semantics.BigStep.CompilerCorrectness.BarTheorem where

open import Syntax
open import Semantics.BigStep
open import VirtualMachine
import CompilerCorrectness as CC; open CC BigStep
import Bar; open Bar _⟶_

open import Data.List hiding (_∈_)
open import Data.Product
open import Data.Function using (_∘_)
open import Relation.Unary hiding (U)
open import Relation.Binary.PropositionalEquality

-- A generalisation of CompilerCorrectness.Matches.

data Matches⁺ (ops : Code) (s : Stack) {t : _} (e : Expr t) (i : Status)
       : Pred State where
  returns : ∀ {n} (↡ : e ⇓[ i ] nat n) → Matches⁺ ops s e i ⟨ ops , i , nat n ∷ s ⟩
  throws  :       (↯ : e ⇓[ i ] throw) → Matches⁺ ops s e i ⟪ i , s ⟫

-- Matches⁺ is actually a generalisation.

Matches⁺⇒Matches : ∀ {t} {e : Expr t} {i} →
                   Matches⁺ [] [] e i ⊆ λ s → e ⇓[ i ]Matches s
Matches⁺⇒Matches ._ (returns ↡) = returns ↡
Matches⁺⇒Matches ._ (throws ↯)  = throws ↯

-- Some abbreviations, used in the proof of the bar theorem.

_∋◁∞_ : Pred State → Pred State → Set1
P ∋◁∞ Q = ∀ {y} → y ∈ P → y ◁∞″ Q

_⟶◁∞_ : State → Pred State → Set1
_⟶◁∞_ x = _∋◁∞_ (_⟶_ x)

-- The bar theorem.

bar-thm : ∀ {t} (e : Expr t) {ops i s} →
          ⟨ comp e ops , i , s ⟩ ◁∞″ Matches⁺ ops s e i

bar-thm {t = t} ⌜ nat n ⌝ = ↓ later (, push) helper₁
  where
  helper₁ : ∀ {ops i s} →
            ⟨ push n ∷ ops , i , s ⟩ ⟶◁∞ Matches⁺ ops s {t} ⌜ nat n ⌝ i
  helper₁ push      = ↓ now (returns Val)
  helper₁ interrupt = ↓ now (throws Int)

bar-thm {t = t} ⌜ throw ⌝ = ↓ later (, throw) helper₁
  where
  helper₁ : ∀ {ops i s} →
            ⟨ throw ∷ ops , i , s ⟩ ⟶◁∞ Matches⁺ ops s {t} ⌜ throw ⌝ i
  helper₁ throw     = ↓ now (throws Val)
  helper₁ interrupt = ↓ now (throws Int)

bar-thm (x ⊕ y) = ◁∞′-trans (bar-thm x) helper₁
  where
  helper₆ : ∀ {ops m s} →
            ⟪ U , nat m ∷ s ⟫ ⟶◁∞ Matches⁺ ops s (x ⊕ y) U
  helper₆ nat = ↓ now (throws Int)

  helper₅ : ∀ {ops m n s} →
            ⟪ U , nat n ∷ nat m ∷ s ⟫ ⟶◁∞ Matches⁺ ops s (x ⊕ y) U
  helper₅ nat = ↓ later (, nat) helper₆

  helper₄ : ∀ {ops i m s} →
            x ⇓[ i ] nat m → y ↯[ i ] →
            ⟪ i , nat m ∷ s ⟫ ⟶◁∞ Matches⁺ ops s (x ⊕ y) i
  helper₄ x↡ y↯ nat = ↓ now (throws (Add₃ x↡ y↯))

  helper₃ : ∀ {ops i n m s} →
            x ⇓[ i ] nat m → y ⇓[ i ] nat n →
            ⟨ add ∷ ops , i , nat n ∷ nat m ∷ s ⟩ ⟶◁∞
            Matches⁺ ops s (x ⊕ y) i
  helper₃ x↡ y↡ add       = ↓ now (returns (Add₁ x↡ y↡))
  helper₃ _  _  interrupt = ↓ later (, nat) helper₅

  helper₂ : ∀ {ops i m s} →
            x ⇓[ i ] nat m →
            Matches⁺ (add ∷ ops) (nat m ∷ s) y i ∋◁∞
            Matches⁺ ops s (x ⊕ y) i
  helper₂ x↡ (returns y↡) = ↓ later (, add) (helper₃ x↡ y↡)
  helper₂ x↡ (throws y↯)  = ↓ later (, nat) (helper₄ x↡ y↯)

  helper₁ : ∀ {ops i s} →
            Matches⁺ (comp y (add ∷ ops)) s x i ∋◁∞
            Matches⁺ ops s (x ⊕ y) i
  helper₁ (throws  x↯) = ↓ now (throws (Add₂ x↯))
  helper₁ (returns x↡) = ◁∞′-trans (bar-thm y) (helper₂ x↡)

bar-thm (x >> y) = ◁∞′-trans (bar-thm x) helper₁
  where
  helper₄ : ∀ {ops m s} →
            ⟪ U , nat m ∷ s ⟫ ⟶◁∞ Matches⁺ ops s (x >> y) U
  helper₄ nat = ↓ now (throws Int)

  helper₃ : ∀ {ops i m s} →
            x ⇓[ i ] nat m →
            Matches⁺ ops s y i ∋◁∞ Matches⁺ ops s (x >> y) i
  helper₃ x↡ (returns y↡) = ↓ now (returns (Seqn₁ x↡ y↡))
  helper₃ x↡ (throws  y↯) = ↓ now (throws  (Seqn₁ x↡ y↯))

  helper₂ : ∀ {ops i m s} →
            x ⇓[ i ] nat m →
            ⟨ pop ∷ comp y ops , i , nat m ∷ s ⟩ ⟶◁∞
            Matches⁺ ops s (x >> y) i
  helper₂ x↡ pop       = ◁∞′-trans (bar-thm y) (helper₃ x↡)
  helper₂ _  interrupt = ↓ later (, nat) helper₄

  helper₁ : ∀ {ops i s} →
            Matches⁺ (pop ∷ comp y ops) s x i ∋◁∞
            Matches⁺ ops s (x >> y) i
  helper₁ (throws  x↯) = ↓ now (throws (Seqn₂ x↯))
  helper₁ (returns x↡) = ↓ later (, pop) (helper₂ x↡)

bar-thm (x catch y) = ↓ later (, mark) helper₁
  where
  helper₉ : ∀ {ops i s} →
            x ↯[ i ] → y ↯[ B ] →
            ⟪ B , int i ∷ s ⟫ ⟶◁∞ Matches⁺ ops s (x catch y) i
  helper₉ x↯ y↯ int = ↓ now (throws (Catch₂ x↯ y↯))

  helper₈ : ∀ {ops i n s} →
            x ↯[ i ] → y ⇓[ B ] nat n →
            ⟨ reset ∷ ops , B , nat n ∷ int i ∷ s ⟩ ⟶◁∞
            Matches⁺ ops s (x catch y) i
  helper₈ x↯ y↡ reset = ↓ now (returns (Catch₂ x↯ y↡))

  helper₇ : ∀ {ops i s} →
            x ↯[ i ] →
            Matches⁺ (reset ∷ ops) (int i ∷ s) y B ∋◁∞
            Matches⁺ ops s (x catch y) i
  helper₇ x↯ (returns y↡) = ↓ later (, reset) (helper₈ x↯ y↡)
  helper₇ x↯ (throws  y↯) = ↓ later (, int)   (helper₉ x↯ y↯)

  helper₆ : ∀ {ops i s} →
            x ↯[ i ] →
            ⟪ i , han (comp y (reset ∷ ops)) ∷ s ⟫ ⟶◁∞
            Matches⁺ ops s (x catch y) i
  helper₆ x↯ han = ◁∞′-trans (bar-thm y) (helper₇ x↯)

  helper₅ : ∀ {ops i s} →
            x ↯[ i ] →
            ⟪ i , han (comp y (reset ∷ ops)) ∷ s ⟫ ◁∞″
            Matches⁺ ops s (x catch y) i
  helper₅ x↯ = ↓ later (, han) (helper₆ x↯)

  helper₄ : ∀ {ops m s} →
            ⟪ U , nat m ∷ han (comp y (reset ∷ ops)) ∷ s ⟫ ⟶◁∞
            Matches⁺ ops s (x catch y) U
  helper₄ nat = helper₅ Int

  helper₃ : ∀ {ops i m s} →
            x ⇓[ i ] nat m →
            ⟨ unmark ∷ ops , i ,
              nat m ∷ han (comp y (reset ∷ ops)) ∷ s ⟩ ⟶◁∞
            Matches⁺ ops s (x catch y) i
  helper₃ x↡ unmark    = ↓ now (returns (Catch₁ x↡))
  helper₃ _  interrupt = ↓ later (, nat) helper₄

  helper₂ : ∀ {ops i s} →
            Matches⁺ (unmark ∷ ops)
                     (han (comp y (reset ∷ ops)) ∷ s) x i ∋◁∞
            Matches⁺ ops s (x catch y) i
  helper₂ (returns x↡) = ↓ later (, unmark) (helper₃ x↡)
  helper₂ (throws  x↯) = helper₅ x↯

  helper₁ : ∀ {ops i s} →
            ⟨ mark (comp y (reset ∷ ops)) ∷
                comp x (unmark ∷ ops) , i , s ⟩ ⟶◁∞
            Matches⁺ ops s (x catch y) i
  helper₁ mark      = ◁∞′-trans (bar-thm x) helper₂
  helper₁ interrupt = ↓ now (throws Int)

bar-thm (block x) = ↓ later (, set) helper₁
  where
  helper₄ : ∀ {ops i s} →
            x ↯[ B ] →
            ⟪ B , int i ∷ s ⟫ ⟶◁∞ Matches⁺ ops s (block x) i
  helper₄ x↯ int = ↓ now (throws (Block x↯))

  helper₃ : ∀ {ops i m s} →
            x ⇓[ B ] nat m →
            ⟨ reset ∷ ops , B , nat m ∷ int i ∷ s ⟩ ⟶◁∞
            Matches⁺ ops s (block x) i
  helper₃ x↡ reset = ↓ now (returns (Block x↡))

  helper₂ : ∀ {ops i s} →
            Matches⁺ (reset ∷ ops) (int i ∷ s) x B ∋◁∞
            Matches⁺ ops s (block x) i
  helper₂ (returns x↡) = ↓ later (, reset) (helper₃ x↡)
  helper₂ (throws  x↯) = ↓ later (, int)   (helper₄ x↯)

  helper₁ : ∀ {ops i s} →
            ⟨ set B ∷ comp x (reset ∷ ops) , i , s ⟩ ⟶◁∞
            Matches⁺ ops s (block x) i
  helper₁ set       = ◁∞′-trans (bar-thm x) helper₂
  helper₁ interrupt = ↓ now (throws Int)

bar-thm (unblock x) = ↓ later (, set) helper₁
  where
  helper₆ : ∀ {ops i s} →
            x ↯[ U ] →
            ⟪ U , int i ∷ s ⟫ ⟶◁∞ Matches⁺ ops s (unblock x) i
  helper₆ x↯ int = ↓ now (throws (Unblock x↯))

  helper₅ : ∀ {ops i s} →
            x ↯[ U ] →
            ⟪ U , int i ∷ s ⟫ ◁∞″ (Matches⁺ ops s (unblock x) i)
  helper₅ x↯ = ↓ later (, int) (helper₆ x↯)

  helper₄ : ∀ {ops i m s} →
            ⟪ U , nat m ∷ int i ∷ s ⟫ ⟶◁∞ Matches⁺ ops s (unblock x) i
  helper₄ nat = helper₅ Int

  helper₃ : ∀ {ops i m s} →
            x ⇓[ U ] nat m →
            ⟨ reset ∷ ops , U , nat m ∷ int i ∷ s ⟩ ⟶◁∞
            Matches⁺ ops s (unblock x) i
  helper₃ x↡ reset     = ↓ now (returns (Unblock x↡))
  helper₃ _  interrupt = ↓ later (, nat) helper₄

  helper₂ : ∀ {ops i s} →
            Matches⁺ (reset ∷ ops) (int i ∷ s) x U ∋◁∞
            Matches⁺ ops s (unblock x) i
  helper₂ (returns x↡) = ↓ later (, reset) (helper₃ x↡)
  helper₂ (throws  x↯) = helper₅ x↯

  helper₁ : ∀ {ops i s} →
            ⟨ set U ∷ comp x (reset ∷ ops) , i , s ⟩ ⟶◁∞
            Matches⁺ ops s (unblock x) i
  helper₁ set       = ◁∞′-trans (bar-thm x) helper₂
  helper₁ interrupt = ↓ now (throws Int)

bar-thm (loop x) = ↓ later (, loop) helper₁
  where
  helper₄ : ∀ {ops m s} →
            ⟪ U , nat m ∷ s ⟫ ⟶◁∞ Matches⁺ ops s (loop x) U
  helper₄ nat = ↓ now (throws Int)

  helper₃ : ∀ {ops i m s} →
            x ⇓[ i ] nat m →
            ⟨ pop ∷ loop x ∷ ops , i , nat m ∷ s ⟩ ⟶◁∞
            Matches⁺ ops s (loop x) i
  helper₃ x↡ pop       ~ bar-thm (loop x)
  helper₃ _  interrupt = ↓ later (, nat) helper₄

  helper₂ : ∀ {ops i s} →
            Matches⁺ (pop ∷ loop x ∷ ops) s x i ∋◁∞
            Matches⁺ ops s (loop x) i
  helper₂ (throws  x↯) = ↓ now (throws (Loop (Seqn₂ x↯)))
  helper₂ (returns x↡) = ↓ later (, pop) (helper₃ x↡)

  helper₁ : ∀ {ops i s} →
            ⟨ loop x ∷ ops , i , s ⟩ ⟶◁∞ Matches⁺ ops s (loop x) i
  helper₁ loop      = ◁∞′-trans (bar-thm x) helper₂
  helper₁ interrupt = ↓ now (throws Int)

bar-theorem : ∀ {t} (e : Expr t) {ops i s} →
              ⟨ comp e ops , i , s ⟩ ◁∞ Matches⁺ ops s e i
bar-theorem e = ∞″→∞ (bar-thm e)