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
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⁺⇒Matches : ∀ {t} {e : Expr t} {i} →
Matches⁺ [] [] e i ⊆ λ s → e ⇓[ i ]Matches s
Matches⁺⇒Matches ._ (returns ↡) = returns ↡
Matches⁺⇒Matches ._ (throws ↯) = throws ↯
_∋◁∞_ : Pred State → Pred State → Set1
P ∋◁∞ Q = ∀ {y} → y ∈ P → y ◁∞″ Q
_⟶◁∞_ : State → Pred State → Set1
_⟶◁∞_ x = _∋◁∞_ (_⟶_ x)
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)