module Semantics.BigStep.CompilerCorrectness.Completeness where
open import Syntax
open import Semantics.BigStep
open import VirtualMachine
import CompilerCorrectness as CC; open CC BigStep
open import Infinite
open import Data.Nat
open import Data.List
open import Data.Star
open import Data.Empty
open import Data.Product
open import Relation.Binary.PropositionalEquality
code-nonempty : ∀ {t} (e : Expr t) ops → [] ≢ comp e ops
code-nonempty ⌜ nat n ⌝ ops = λ()
code-nonempty ⌜ throw ⌝ ops = λ()
code-nonempty (loop x) ops = λ()
code-nonempty (x ⊕ y) ops = code-nonempty x _
code-nonempty (x >> y) ops = code-nonempty x _
code-nonempty (x catch y) ops = λ()
code-nonempty (block x) ops = λ()
code-nonempty (unblock x) ops = λ()
mutual
complete↡ : ∀ {t} {e : Expr t} {ops i s n} →
e ⇓[ i ] nat n →
⟨ comp e ops , i , s ⟩ ⟶⋆ ⟨ ops , i , nat n ∷ s ⟩
complete↡ Val = push ◅ ε
complete↡ (Loop l) = loop ◅ complete↡ l
complete↡ (Add₁ x y) = complete↡ x ◅◅ complete↡ y ◅◅ add ◅ ε
complete↡ (Seqn₁ x y) = complete↡ x ◅◅ pop ◅ complete↡ y
complete↡ (Catch₁ x) = mark ◅ complete↡ x ◅◅ unmark ◅ ε
complete↡ (Catch₂ x y) = mark ◅ complete↯ x ◅◅ han ◅ complete↡ y ◅◅
reset ◅ ε
complete↡ (Block x) = set ◅ complete↡ x ◅◅ reset ◅ ε
complete↡ (Unblock x) = set ◅ complete↡ x ◅◅ reset ◅ ε
complete↯ : ∀ {t} {e : Expr t} {ops i s} →
e ↯[ i ] → ⟨ comp e ops , i , s ⟩ ⟶⋆ ⟪ i , s ⟫
complete↯ Val = throw ◅ ε
complete↯ (Loop l) = loop ◅ complete↯ l
complete↯ (Add₂ x) = complete↯ x
complete↯ (Add₃ x y) = complete↡ x ◅◅ complete↯ y ◅◅ nat ◅ ε
complete↯ (Seqn₁ x y) = complete↡ x ◅◅ pop ◅ complete↯ y
complete↯ (Seqn₂ x) = complete↯ x
complete↯ (Catch₂ x y) = mark ◅ complete↯ x ◅◅ han ◅ complete↯ y ◅◅
int ◅ ε
complete↯ (Block x) = set ◅ complete↯ x ◅◅ int ◅ ε
complete↯ (Unblock x) = set ◅ complete↯ x ◅◅ int ◅ ε
complete↯ {e = e} {ops} {s = s} Int with inspect (comp e ops)
... | (_ ∷ _) with-≡ eq =
≡-subst (λ ops → Star _⟶_ ⟨ ops , U , s ⟩ ⟪ U , s ⟫) eq
(interrupt ◅ ε)
... | [] with-≡ eq = ⊥-elim (code-nonempty e ops eq)
complete₁ : ∀ {t} (e : Expr t) {i} → Complete₁ e i
complete₁ e (returns ↡) = term (complete↡ ↡) (matches-final (returns ↡))
complete₁ e (throws ↯) = term (complete↯ ↯) (matches-final (throws ↯))
complete⇑ : ∀ {t} {e : Expr t} {ops i s} →
e ⇑[ i ] → Infinite″ _⟶_ ⟨ comp e ops , i , s ⟩
complete⇑ (Loop l) ~ ↓ loop ◅∞ complete⇑ l
complete⇑ (Add₁ x) = complete⇑ x
complete⇑ (Add₂ x y) = complete↡ (proj₂ x) ◅◅∞′ complete⇑ y
complete⇑ (Seqn₁ x) = complete⇑ x
complete⇑ (Seqn₂ x y) = complete↡ (proj₂ x) ◅◅∞′ (↓ pop ◅∞ complete⇑ y)
complete⇑ (Catch₁ x) = ↓ mark ◅∞ complete⇑ x
complete⇑ (Catch₂ x y) = ↓ mark ◅∞ complete↯ x ◅◅∞′ (↓ han ◅∞ complete⇑ y)
complete⇑ (Block x) = ↓ set ◅∞ complete⇑ x
complete⇑ (Unblock x) = ↓ set ◅∞ complete⇑ x
complete₂ : ∀ {t} {e : Expr t} {i} → Complete₂ e i
complete₂ ⇑ = ∞″→∞ (complete⇑ ⇑)