------------------------------------------------------------------------
-- Completeness
------------------------------------------------------------------------

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

------------------------------------------------------------------------
-- Some lemmas

-- The compiler always returns a non-empty instruction sequence.

code-nonempty : forall {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 = \()

------------------------------------------------------------------------
-- Completeness

mutual

  complete↡ : forall {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↯ : forall {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₁ : forall {t} (e : Expr t) {i} -> Complete₁ e i
complete₁ e (returns ↡) = complete↡ ↡
complete₁ e (throws ↯)  = complete↯ ↯

complete⇑ : forall {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₂ : forall {t} {e : Expr t} {i} -> Complete₂ e i
complete₂ ⇑ = ∞″→∞ (complete⇑ ⇑)