[Proved completeness. Nils Anders Danielsson **20080429115545] addfile ./Completeness.agda hunk ./Completeness.agda 1 +------------------------------------------------------------------------ +-- The compiler and VM are complete with respect to the high-level +-- semantics +------------------------------------------------------------------------ + +module Completeness where + +open import Language +open import VirtualMachine +open import Data.List +open import Data.Star +open import Relation.Binary.PropositionalEquality +open import Logic + +------------------------------------------------------------------------ +-- Some lemmas + +[]≢∷ : forall {x xs} -> [] ≢ x ∷ xs +[]≢∷ () + +-- The compiler always returns a non-empty instruction sequence. + +code-nonempty : forall e ops -> [] ≢ comp e ops +code-nonempty (val n) ops = []≢∷ +code-nonempty throw 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 {e ops i s n} -> + e ⇓[ i ] val n -> + Star _⟶_ ⟨ comp e ops , i , s ⟩ ⟨ ops , i , val n ∷ s ⟩ + complete₁ Val = push ◅ ε + 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 + complete₁ (Block x) = set ◅ complete₁ x ◅◅ reset ◅ ε + complete₁ (Unblock x) = set ◅ complete₁ x ◅◅ reset ◅ ε + + complete₂ : forall {e ops i s} -> + e ⇑[ i ] -> Star _⟶_ ⟨ comp e ops , i , s ⟩ ⟪ i , s ⟫ + complete₂ Throw = throw ◅ ε + complete₂ (Add₂ x) = complete₂ x + complete₂ (Add₃ x y) = complete₁ x ◅◅ complete₂ y ◅◅ val ◅ ε + complete₂ (Seqn₁ x y) = complete₁ x ◅◅ pop ◅ complete₂ y + complete₂ (Seqn₂ x) = complete₂ x + complete₂ (Catch₂ x y) = mark ◅ complete₂ x ◅◅ han ◅ complete₂ y + complete₂ (Block x) = set ◅ complete₂ x ◅◅ int ◅ ε + complete₂ (Unblock x) = set ◅ complete₂ x ◅◅ int ◅ ε + complete₂ {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 {e ops i s} -> + ⟨ comp e ops , i , s ⟩ ⟶⋆ Target e ops i s +complete (returns ⇓) = complete₁ ⇓ +complete (throws ⇑) = complete₂ ⇑ hunk ./Everything.agda 13 +import Completeness