import Relation.Binary.PropositionalEquality as Eq
open import Data.Empty using (⊥)
open import Data.Fin using (Fin; suc; zero)
open import Data.Nat using (ℕ; suc; zero)
open import Data.Product using (∃-syntax; _×_; _,_)
open import Data.Unit using (⊤; tt)
open Eq using (_≡_; refl; sym; subst)
open import CBPV.Base.Semantics
open import CBPV.Base.SmallStep
open import CBPV.Base.Substitution
open import CBPV.Base.Terms
module CBPV.Base.Adequacy where
mutual
_~_ : Env n → Sub zero n → Set
ρ ~ σ = ∀ m → ρ m ≈v σ m
_≈v_ : ClosVal → Val zero → Set
unit ≈v unit = ⊤
clos⦅ ρ ,⟪ M ⟫⦆ ≈v V = ∃[ σ ] ρ ~ σ × V ≡ ⟪ M ⦅ σ ⦆c ⟫
⟨ W₁ , W₂ ⟩ ≈v ⟨ V₁ , V₂ ⟩ = W₁ ≈v V₁ × W₂ ≈v V₂
inl W ≈v inl V = W ≈v V
inr W ≈v inr V = W ≈v V
_ ≈v _ = ⊥
_≈c_ : ClosTerminal → Comp zero → Set
(return V₁) ≈c (return V₂) = V₁ ≈v V₂
clos⦅ ρ ,ƛ M ⦆ ≈c N = ∃[ σ ] ρ ~ σ × N ≡ (ƛ M) ⦅ σ ⦆c
clos⦅ ρ ,⟨ M₁ , M₂ ⟩⦆ ≈c N = ∃[ σ ] ρ ~ σ × N ≡ ⟨ M₁ , M₂ ⟩ ⦅ σ ⦆c
_ ≈c _ = ⊥
infix 4 _~_
infix 4 _≈v_
infix 4 _≈c_
~-ext : ρ ~ σ → W ≈v V → ρ ∷ᵨ W ~ V • σ
~-ext _ W≈V zero = W≈V
~-ext ρ~σ _ (suc m) = ρ~σ m
mutual
⇓-adequate-val : ρ ~ σ
→ ρ ⊢v V ⇓ W
→ W ≈v V ⦅ σ ⦆v
⇓-adequate-val ρ~σ (evalVar {m = m}) = ρ~σ m
⇓-adequate-val ρ~σ evalUnit = tt
⇓-adequate-val {σ = σ} ρ~σ evalThunk = σ , ρ~σ , refl
⇓-adequate-val ρ~σ (evalPair V₁⇓ V₂⇓) =
⇓-adequate-val ρ~σ V₁⇓ , ⇓-adequate-val ρ~σ V₂⇓
⇓-adequate-val ρ~σ (evalInl V⇓) = ⇓-adequate-val ρ~σ V⇓
⇓-adequate-val ρ~σ (evalInr V⇓) = ⇓-adequate-val ρ~σ V⇓
⇓-adequate : ρ ~ σ
→ ρ ⊢c M ⇓ T
→ ∃[ N ] M ⦅ σ ⦆c ⟶* N × T ≈c N
⇓-adequate {σ = σ} {M = M} ρ~σ evalAbs =
M ⦅ σ ⦆c , M ⦅ σ ⦆c ∎ , σ , ρ~σ , refl
⇓-adequate {σ = σ} ρ~σ (evalRet {V = V} V⇓) =
return V ⦅ σ ⦆v , (return V ⦅ σ ⦆v) ∎ , ⇓-adequate-val ρ~σ V⇓
⇓-adequate {σ = σ} ρ~σ (evalSeq {V = V} V⇓ M⇓)
with ⇓-adequate-val ρ~σ V⇓ | ⇓-adequate ρ~σ M⇓
... | unit≈V | N , M⟶ , T≈N
with V ⦅ σ ⦆v in eq
... | unit =
N , (βseq ⟶⟨ M⟶ ⟩) , T≈N
⇓-adequate {σ = σ} ρ~σ (evalApp {M′ = M′} {V} M⇓ V⇓ T′⇓)
with ⇓-adequate ρ~σ M⇓
... | N′ , M⟶ , (σ′ , ρ′~σ′ , refl)
with ⇓-adequate-val ρ~σ V⇓
... | W≈V
with ⇓-adequate (~-ext ρ′~σ′ W≈V) T′⇓ | β {M = M′ ⦅ exts σ′ ⦆c} {V = V ⦅ σ ⦆v}
... | N , T′⟶* , T≈N | step
rewrite sub-sub (exts σ′) (V ⦅ σ ⦆v • id) M′
| sym (subst-zero-exts-cons σ′ (V ⦅ σ ⦆v))
| sym (sub-sub (exts σ′) (subst-zero (V ⦅ σ ⦆v)) M′) =
N ,
⟶*-trans (⟶*-app-compatible M⟶) (step ⟶⟨ T′⟶* ⟩ ) ,
T≈N
⇓-adequate ρ~σ (evalForce V⇓ M⇓)
with ⇓-adequate-val ρ~σ V⇓
... | σ′ , ρ′~σ′ , eq
with ⇓-adequate ρ′~σ′ M⇓
... | N , M⟶* , T≈N
rewrite eq =
N , (βforceThunk ⟶⟨ M⟶* ⟩) , T≈N
⇓-adequate {σ = σ} ρ~σ (evalLetin {N = N} M⇓ N⇓)
with ⇓-adequate ρ~σ M⇓
... | retV , M⟶ , W≈V
with retV in eq
... | return V
with ⇓-adequate (~-ext ρ~σ W≈V) N⇓
... | N′ , N⟶ , T≈N′
rewrite sym (subst-zero-exts-cons σ V)
| sym (sub-sub (exts σ) (subst-zero V) N) =
N′ , ⟶*-trans (⟶*-letin-compatible M⟶) (βletin ⟶⟨ N⟶ ⟩) , T≈N′
⇓-adequate {σ = σ} ρ~σ (evalSplit {V = V} {M = M} V⇓ M⇓)
with V ⦅ σ ⦆v in eq | ⇓-adequate-val ρ~σ V⇓
... | ⟨ V₁ , V₂ ⟩ | W₁≈V₁ , W₂≈V₂
with ⇓-adequate (~-ext (~-ext ρ~σ W₁≈V₁) W₂≈V₂) M⇓
... | N , M⟶ , T≈N =
N ,
(βsplit ⟶⟨ subst (_⟶* N) subst-lemma M⟶ ⟩) ,
T≈N
where
subst-lemma : M ⦅ V₂ • V₁ • σ ⦆c ≡ (M ⦅ exts (exts σ) ⦆c) ⦅ V₂ • V₁ • id ⦆c
subst-lemma
rewrite sub-sub (exts (exts σ)) (V₂ • V₁ • id) M
| exts-seq-cons (exts σ) V₂ (V₁ • id)
| exts-seq-cons σ V₁ id
| sub-idR {σ = σ} = refl
⇓-adequate {σ = σ} ρ~σ (evalCaseInl {V = V} {M₁ = M₁} V⇓ M₁⇓)
with V ⦅ σ ⦆v in eq | ⇓-adequate-val ρ~σ V⇓
... | inl V | W≈V
with ⇓-adequate (~-ext ρ~σ W≈V) M₁⇓
... | N , M₁⟶ , T≈N
rewrite sym (subst-zero-exts-cons σ V)
| sym (sub-sub (exts σ) (subst-zero V) M₁) =
N , (βcaseInl ⟶⟨ M₁⟶ ⟩) , T≈N
⇓-adequate {σ = σ} ρ~σ (evalCaseInr {V = V} {M₂ = M₂} V⇓ M₂⇓)
with V ⦅ σ ⦆v in eq | ⇓-adequate-val ρ~σ V⇓
... | inr V | W≈V
with ⇓-adequate (~-ext ρ~σ W≈V) M₂⇓
... | N , M₂⟶ , T≈N
rewrite sym (subst-zero-exts-cons σ V)
| sym (sub-sub (exts σ) (subst-zero V) M₂) =
N , (βcaseInr ⟶⟨ M₂⟶ ⟩) , T≈N
⇓-adequate {σ = σ} {M = M} ρ~σ evalCpair =
M ⦅ σ ⦆c , M ⦅ σ ⦆c ∎ , σ , ρ~σ , refl
⇓-adequate ρ~σ (evalProjl M⇓ M₁⇓)
with ⇓-adequate ρ~σ M⇓
... | N′ , M⟶ , (σ′ , ρ′~σ′ , eq)
with ⇓-adequate ρ′~σ′ M₁⇓
... | N , M₁⟶ , T≈N
rewrite eq =
N , ⟶*-trans (⟶*-projl-compatible M⟶) (βprojl ⟶⟨ M₁⟶ ⟩) , T≈N
⇓-adequate ρ~σ (evalProjr M⇓ M₂⇓)
with ⇓-adequate ρ~σ M⇓
... | N′ , M⟶ , (σ′ , ρ′~σ′ , eq)
with ⇓-adequate ρ′~σ′ M₂⇓
... | N , M₂⟶ , T≈N
rewrite eq =
N , ⟶*-trans (⟶*-projr-compatible M⟶) (βprojr ⟶⟨ M₂⟶ ⟩) , T≈N
adequacy : ∅ᵨ ⊢c M ⇓ T
→ ∃[ N ] M ⟶* N × T ≈c N
adequacy {M = M} M⇓
with ⇓-adequate {σ = id} (λ ()) M⇓
... | lemma
rewrite sub-id M = lemma