```------------------------------------------------------------------------
-- 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₃ _  _  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)
```