module CC.ProxyEliminationErasure where

open import Data.Nat
open import Data.Unit using (⊀; tt)
open import Data.Bool using (true; false) renaming (Bool to 𝔹)
open import Data.List
open import Data.Product using (_Γ—_; βˆƒ-syntax; proj₁; projβ‚‚) renaming (_,_ to ⟨_,_⟩)
open import Data.Maybe
open import Relation.Nullary using (Β¬_; Dec; yes; no)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Binary.PropositionalEquality using (_≑_; refl; sym; trans; subst; substβ‚‚)
open import Function using (case_of_)

open import Common.Utils
open import Common.Types
open import CC.CCStatics
open import CC.WellTyped
open import CC.ProxyElimination
open import CC.Erasure


elim-fun-proxy-erase : βˆ€ {A B C D gc₁ gcβ‚‚ g₁ gβ‚‚} {M}
  β†’ βˆ€ {c : Cast (⟦ gc₁ ⟧ A β‡’ B of g₁) β‡’ (⟦ gcβ‚‚ ⟧ C β‡’ D of gβ‚‚)}
  β†’ βˆ€ V W (i : Inert c) pc
  β†’ M ≑ elim-fun-proxy V W i pc
  β†’ Β¬ Err M
    ----------------------------------------------------
  β†’ erase M ≑ erase (V Β· W)
elim-fun-proxy-erase V W (I-fun c I-label I-label) pc refl Β¬err with c
... | cast (⟦ l pc₁ ⟧ A β‡’ B of l ℓ₁) (⟦ l pcβ‚‚ ⟧ C β‡’ D of gβ‚‚) p _ = refl
... | cast (⟦ l pc₁ ⟧ A β‡’ B of l ℓ₁) (⟦ ⋆     ⟧ C β‡’ D of gβ‚‚) p _
  with pc β‹Ž ℓ₁ β‰Ό? pc₁
...   | yes _ = refl
...   | no  _ = contradiction E-error Β¬err

elim-ref-proxy-erase : βˆ€ {A B g₁ gβ‚‚} {N} {_≔_}
  β†’ βˆ€ {c : Cast Ref A of g₁ β‡’ Ref B of gβ‚‚}
  β†’ βˆ€ V M (i : Inert c)
  β†’ RefAssign _≔_
  β†’ N ≑ elim-ref-proxy V M i _≔_
  β†’ Β¬ Err N
    ----------------------------------------------------
  β†’ erase N ≑ erase (V ≔ M)
elim-ref-proxy-erase V M (I-ref c I-label I-label) static refl Β¬err with c
... | cast (Ref (S of l ℓ₁) of l β„“) (Ref (T of l β„“β‚‚) of g) p _ = refl
... | cast (Ref (S of l ℓ₁) of l β„“) (Ref (T of ⋆   ) of g) p _
  with β„“ β‰Ό? ℓ₁
...   | yes _ = refl
...   | no  _ = contradiction E-error Β¬err
elim-ref-proxy-erase V M (I-ref c I-label I-label) checked refl Β¬err with c
... | cast (Ref (S of l ℓ₁) of l β„“) (Ref (T of l β„“β‚‚) of g) p _ = refl
... | cast (Ref (S of l ℓ₁) of l β„“) (Ref (T of ⋆   ) of g) p _
  with β„“ β‰Ό? ℓ₁
...   | yes _ = refl
...   | no  _ = contradiction E-error Β¬err
elim-ref-proxy-erase V M (I-ref c I-label I-label) unchecked refl Β¬err with c
... | cast (Ref (S of l ℓ₁) of l β„“) (Ref (T of l β„“β‚‚) of g) p _ = refl
... | cast (Ref (S of l ℓ₁) of l β„“) (Ref (T of ⋆   ) of g) p _
  with β„“ β‰Ό? ℓ₁
...   | yes _ = refl
...   | no  _ = contradiction E-error Β¬err