[Attempted to prove completeness using the small-step semantics.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20081104164041
 + However, this proof appears to require considerably more work than
   the proof which uses the big-step semantics, so I have decided to
   abort this proof attempt.
] addfile ./Semantics/SmallStep/CompilerCorrectness/Completeness.agda
hunk ./Semantics/SmallStep/CompilerCorrectness/Completeness.agda 1
+------------------------------------------------------------------------
+-- Completeness
+------------------------------------------------------------------------
+
+-- Unfinished (and possibly bit-rotted) proof attempt. The proof which
+-- uses the big-step semantics is very simple, and this one is more
+-- complicated, so I don't see any point in spending more time on this
+-- proof. This file is retained just for illustrative purposes.
+
+module Semantics.SmallStep.CompilerCorrectness.Completeness where
+
+open import Syntax
+open import Semantics.SmallStep
+open import VirtualMachine
+import CompilerCorrectness as CC; open CC SmallStep
+open import Infinite
+
+open import Data.List
+open import Data.Star
+open import Data.Product
+open import Data.Sum
+open import Relation.Binary.PropositionalEquality
+
+------------------------------------------------------------------------
+-- Completeness
+
+Goal : Code -> Status -> Stack -> Value -> State
+Goal ops i s (nat n) = ⟨ ops , i , nat n ∷ s ⟩
+Goal ops i s throw   = ⟪ i , s ⟫
+
+block-lemma : forall {t i} {x : Exprˢ t} {v} ->
+              run (block x) ⟶⋆[ i ] done v ->
+              (i ≡ U × v ≡ throw) ⊎ (x ⟶⋆[ B ] done v)
+block-lemma (Blockˡ ⟶    ◅ …) with block-lemma …
+block-lemma (Blockˡ ⟶    ◅ …) | inj₁ eq = inj₁ eq
+block-lemma (Blockˡ ⟶    ◅ …) | inj₂ …′ = inj₂ (⟶ ◅ …′)
+block-lemma (Red (Int i) ◅ ε) = inj₁ (≡-refl , ≡-refl)
+block-lemma (Red (Int i) ◅ Red (Int ()) ◅ …)
+block-lemma (Red Block   ◅ ε) = inj₂ ε
+block-lemma (Red Block   ◅ Red (Int i) ◅ ε) = inj₁ (≡-refl , ≡-refl)
+block-lemma (Red Block   ◅ Red (Int _) ◅ Red (Int ()) ◅ …)
+
+unblock-lemma : forall {t i} {x : Exprˢ t} {v} ->
+                run (unblock x) ⟶⋆[ i ] done v -> x ⟶⋆[ U ] done v
+unblock-lemma (Unblockˡ ⟶  ◅ …) = ⟶ ◅ unblock-lemma …
+unblock-lemma (Red (Int i) ◅ …) = Red (Int i) ◅ …
+unblock-lemma (Red Unblock ◅ ε) = ε
+unblock-lemma (Red Unblock ◅ Red (Int i) ◅ ε) = Red (Int i) ◅ ε
+unblock-lemma (Red Unblock ◅ Red (Int _) ◅ Red (Int ()) ◅ …)
+
+lemma : forall {t} v {ops i s} ->
+        ⟨ comp {t} ⌜ v ⌝ ops , i , s ⟩ ⟶⋆ Goal ops i s v
+lemma (nat n) = push  ◅ ε
+lemma throw   = throw ◅ ε
+
+lemma₂ : forall {ops i i′ s} v ->
+         Goal (reset ∷ ops) i (int i′ ∷ s) v ⟶⋆ Goal ops i′ s v
+lemma₂ (nat n) = reset ◅ ε
+lemma₂ throw   = int ◅ ε
+
+-- complete : forall {t} {x : Exprˢ t} {ops i s} v ->
+--            x ⟶⋆[ i ] done v ->
+--            ⟨ comp (x ˢ⁻¹) ops , i , s ⟩ ⟶⋆ Goal ops i s v
+-- complete v        ε                 = lemma v
+-- complete v        (Red Val     ◅ ε) = lemma v
+-- complete v        (Red Loop    ◅ …) = loop ◅ complete v …
+-- complete .(nat _) (Red Add₁    ◅ ε) = push ◅ push ◅ add ◅ ε
+-- complete .throw   (Red Add₂    ◅ ε) = throw ◅ ε
+-- complete .throw   (Red Add₃    ◅ ε) = push ◅ throw ◅ nat ◅ ε
+-- complete v        (Red Seqn₁   ◅ …) = push ◅ pop ◅ complete v …
+-- complete .throw   (Red Seqn₂   ◅ ε) = throw ◅ ε
+-- complete .(nat _) (Red Catch₁  ◅ ε) = mark ◅ push ◅ unmark ◅ ε
+-- complete v        (Red Catch₂  ◅ ε) = mark ◅ throw ◅ han ◅ lemma v ◅◅ lemma₂ v
+-- complete v        (Red Block   ◅ ε) = set ◅ lemma v ◅◅ lemma₂ v
+-- complete v        (Red Unblock ◅ ε) = set ◅ lemma v ◅◅ lemma₂ v
+-- complete .throw   (Red ⟶ ◅ Red (Int _) ◅ ε) = {! !}
+-- complete v        (Red ⟶ ◅ Red (Int _) ◅ Red (Int ()) ◅ _)
+-- complete v        (Red (Int i) ◅ …) = {!interrupt ◅ ? !}
+-- complete v        (Addˡ     ⟶  ◅ …) = {!complete v !}
+-- complete v        (Addʳ     ⟶  ◅ …) = {! !}
+-- complete v        (Seqnˡ    ⟶  ◅ …) = {! !}
+-- complete v        (Catchˡ   ⟶  ◅ …) = {! !}
+-- complete v        (Catchʳ   ⟶  ◅ …) = {! !}
+-- complete v        (Blockˡ   ⟶  ◅ …) = {! !}
+-- complete v        (Unblockˡ ⟶  ◅ …) = {! !}
+
+complete : forall {t} (x : Exprˢ t) {ops i s} v ->
+           x ⟶⋆[ i ] done v ->
+           ⟨ comp (x ˢ⁻¹) ops , i , s ⟩ ⟶⋆ Goal ops i s v
+complete (run ⌜ v′ ⌝) v (Red Val     ◅ …) = {! !}
+complete (run ⌜ v′ ⌝) v (Red (Int i) ◅ …) = {! !}
+complete (run (loop y))    v      … = {! !}
+complete (run (x ⊕ y))     v      … = {! !}
+complete (run (x >> y))    v      … = {! !}
+complete (run (x catch y)) v      … = {! !}
+complete (run (block x))   v      … with block-lemma …
+complete (run (block x))   .throw … | inj₁ (≡-refl , ≡-refl) = interrupt ◅ ε
+complete (run (block x))   v      … | inj₂ …′                = set ◅ complete x v …′ ◅◅ lemma₂ v
+complete (run (unblock x)) v      … = set ◅ complete x v (unblock-lemma …) ◅◅ lemma₂ v
+complete (done v) .v     ε                 = lemma v
+complete (done v) .throw (Red (Int i) ◅ ε) = {!interrupt ◅ ? !}
+complete (done v) _      (Red (Int i) ◅ Red (Int ()) ◅ _)