------------------------------------------------------------------------
-- 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 : ∀ {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 : ∀ {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 : ∀ {t} v {ops i s} →
        ⟨ comp {t} ⌜ v ⌝ ops , i , s ⟩ ⟶⋆ Goal ops i s v
lemma (nat n) = push  ◅ ε
lemma throw   = throw ◅ ε

lemma₂ : ∀ {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 : ∀ {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 : ∀ {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 ()) ◅ _)