------------------------------------------------------------------------
-- 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 : forall {n} ->
            e ⇓[ i ] nat n -> Matches⁺ ops s e i ⟨ ops , i , nat n ∷ s ⟩
  throws  : e ↯[ i ]       -> Matches⁺ ops s e i ⟪ i , s ⟫

-- Matches⁺ is actually a generalisation.

Matches⁺⇒Matches : forall {t} {e : Expr t} {i} ->
                   Matches⁺ [] [] e i ⊆ Matches e i
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 = forall {y} -> y ∈ P -> y ◁∞″ Q

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

-- The bar theorem.

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

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

bar-thm {t = t} ⌜ throw ⌝ ~ ↓ via (, throw) helper₁
  where
  helper₁ : forall {ops i s} ->
            ⟨ throw ∷ ops , i , s ⟩ ⟶◁∞ Matches⁺ ops s {t} ⌜ throw ⌝ i
  helper₁ throw     ~ ↓ directly (throws Val)
  helper₁ interrupt ~ ↓ directly (throws Int)

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

  helper₅ : forall {ops m n s} ->
            ⟪ U , nat n ∷ nat m ∷ s ⟫ ⟶◁∞ Matches⁺ ops s (x ⊕ y) U
  helper₅ nat ~ ↓ via (, nat) helper₆

  helper₄ : forall {ops i m s} ->
            x ⇓[ i ] nat m -> y ↯[ i ] ->
            ⟪ i , nat m ∷ s ⟫ ⟶◁∞ Matches⁺ ops s (x ⊕ y) i
  helper₄ x↡ y↯ nat ~ ↓ directly (throws (Add₃ x↡ y↯))

  helper₃ : forall {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       ~ ↓ directly (returns (Add₁ x↡ y↡))
  helper₃ _  _  interrupt ~ ↓ via (, nat) helper₅

  helper₂ : forall {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↡) ~ ↓ via (, add) (helper₃ x↡ y↡)
  helper₂ x↡ (throws y↯)  ~ ↓ via (, nat) (helper₄ x↡ y↯)

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

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

  helper₃ : forall {ops i m s} ->
            x ⇓[ i ] nat m ->
            Matches⁺ ops s y i ∋◁∞ Matches⁺ ops s (x >> y) i
  helper₃ x↡ (returns y↡) ~ ↓ directly (returns (Seqn₁ x↡ y↡))
  helper₃ x↡ (throws  y↯) ~ ↓ directly (throws  (Seqn₁ x↡ y↯))

  helper₂ : forall {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 ~ ↓ via (, nat) helper₄

  helper₁ : forall {ops i s} ->
            Matches⁺ (pop ∷ comp y ops) s x i ∋◁∞
            Matches⁺ ops s (x >> y) i
  helper₁ (throws  x↯) ~ ↓ directly (throws (Seqn₂ x↯))
  helper₁ (returns x↡) ~ ↓ via (, pop) (helper₂ x↡)

bar-thm (x catch y) ~ ↓ via (, mark) helper₁
  where
  helper₉ : forall {ops i s} ->
            x ↯[ i ] -> y ↯[ B ] ->
            ⟪ B , int i ∷ s ⟫ ⟶◁∞ Matches⁺ ops s (x catch y) i
  helper₉ x↯ y↯ int ~ ↓ directly (throws (Catch₂ x↯ y↯))

  helper₈ : forall {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 ~ ↓ directly (returns (Catch₂ x↯ y↡))

  helper₇ : forall {ops i s} ->
            x ↯[ i ] ->
            Matches⁺ (reset ∷ ops) (int i ∷ s) y B ∋◁∞
            Matches⁺ ops s (x catch y) i
  helper₇ x↯ (returns y↡) ~ ↓ via (, reset) (helper₈ x↯ y↡)
  helper₇ x↯ (throws  y↯) ~ ↓ via (, int)   (helper₉ x↯ y↯)

  helper₆ : forall {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₅ : forall {ops i s} ->
            x ↯[ i ] ->
            ⟪ i , han (comp y (reset ∷ ops)) ∷ s ⟫ ◁∞″
            Matches⁺ ops s (x catch y) i
  helper₅ x↯ ~ ↓ via (, han) (helper₆ x↯)

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

  helper₃ : forall {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    ~ ↓ directly (returns (Catch₁ x↡))
  helper₃ _  interrupt ~ ↓ via (, nat) helper₄

  helper₂ : forall {ops i s} ->
            Matches⁺ (unmark ∷ ops)
                     (han (comp y (reset ∷ ops)) ∷ s) x i ∋◁∞
            Matches⁺ ops s (x catch y) i
  helper₂ (returns x↡) ~ ↓ via (, unmark) (helper₃ x↡)
  helper₂ (throws  x↯) ~ helper₅ x↯

  helper₁ : forall {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 ~ ↓ directly (throws Int)

bar-thm (block x) ~ ↓ via (, set) helper₁
  where
  helper₄ : forall {ops i s} ->
            x ↯[ B ] ->
            ⟪ B , int i ∷ s ⟫ ⟶◁∞ Matches⁺ ops s (block x) i
  helper₄ x↯ int ~ ↓ directly (throws (Block x↯))

  helper₃ : forall {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 ~ ↓ directly (returns (Block x↡))

  helper₂ : forall {ops i s} ->
            Matches⁺ (reset ∷ ops) (int i ∷ s) x B ∋◁∞
            Matches⁺ ops s (block x) i
  helper₂ (returns x↡) ~ ↓ via (, reset) (helper₃ x↡)
  helper₂ (throws  x↯) ~ ↓ via (, int)   (helper₄ x↯)

  helper₁ : forall {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 ~ ↓ directly (throws Int)

bar-thm (unblock x) ~ ↓ via (, set) helper₁
  where
  helper₆ : forall {ops i s} ->
            x ↯[ U ] ->
            ⟪ U , int i ∷ s ⟫ ⟶◁∞ Matches⁺ ops s (unblock x) i
  helper₆ x↯ int ~ ↓ directly (throws (Unblock x↯))

  helper₅ : forall {ops i s} ->
            x ↯[ U ] ->
            ⟪ U , int i ∷ s ⟫ ◁∞″ (Matches⁺ ops s (unblock x) i)
  helper₅ x↯ ~ ↓ via (, int) (helper₆ x↯)

  helper₄ : forall {ops i m s} ->
            ⟪ U , nat m ∷ int i ∷ s ⟫ ⟶◁∞ Matches⁺ ops s (unblock x) i
  helper₄ nat ~ helper₅ Int

  helper₃ : forall {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     ~ ↓ directly (returns (Unblock x↡))
  helper₃ _  interrupt ~ ↓ via (, nat) helper₄

  helper₂ : forall {ops i s} ->
            Matches⁺ (reset ∷ ops) (int i ∷ s) x U ∋◁∞
            Matches⁺ ops s (unblock x) i
  helper₂ (returns x↡) ~ ↓ via (, reset) (helper₃ x↡)
  helper₂ (throws  x↯) ~ helper₅ x↯

  helper₁ : forall {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 ~ ↓ directly (throws Int)

bar-thm (loop x) ~ ↓ via (, loop) helper₁
  where
  helper₄ : forall {ops m s} ->
            ⟪ U , nat m ∷ s ⟫ ⟶◁∞ Matches⁺ ops s (loop x) U
  helper₄ nat ~ ↓ directly (throws Int)

  helper₃ : forall {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 ~ ↓ via (, nat) helper₄

  helper₂ : forall {ops i s} ->
            Matches⁺ (pop ∷ loop x ∷ ops) s x i ∋◁∞
            Matches⁺ ops s (loop x) i
  helper₂ (throws  x↯) ~ ↓ directly (throws (Loop (Seqn₂ x↯)))
  helper₂ (returns x↡) ~ ↓ via (, pop) (helper₃ x↡)

  helper₁ : forall {ops i s} ->
            ⟨ loop x ∷ ops , i , s ⟩ ⟶◁∞ Matches⁺ ops s (loop x) i
  helper₁ loop      ~ ◁∞′-trans (bar-thm x) helper₂
  helper₁ interrupt ~ ↓ directly (throws Int)

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