open import Common.Types

module CC2.HeapContextPrecision 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.Sum using (_⊎_; inj₁; injβ‚‚)
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; trans; subst; substβ‚‚; sym)
open import Function using (case_of_)

open import Syntax hiding (_⨟_)
open import Common.Utils
open import CC2.Statics
open import Memory.Heap Term Value hiding (Addr; a⟦_⟧_)
open import Memory.HeapContext


data _βŠ‘*_ : (Ξ“ Ξ“β€² : Context) β†’ Set where

  βŠ‘*-βˆ… : [] βŠ‘* []

  βŠ‘*-∷ : βˆ€ {Ξ“ Ξ“β€² A Aβ€²} β†’ A βŠ‘ Aβ€² β†’ Ξ“ βŠ‘* Ξ“β€² β†’ (A ∷ Ξ“) βŠ‘* (Aβ€² ∷ Ξ“β€²)


βŠ‘*β†’βŠ‘ : βˆ€ {Ξ“ Ξ“β€² A Aβ€² x} β†’ Ξ“ βŠ‘* Ξ“β€² β†’ Ξ“ βˆ‹ x ⦂ A β†’ Ξ“β€² βˆ‹ x ⦂ Aβ€² β†’ A βŠ‘ Aβ€²
βŠ‘*β†’βŠ‘ {x = 0}     (βŠ‘*-∷ AβŠ‘Aβ€² Ξ“βŠ‘Ξ“β€²) refl refl = AβŠ‘Aβ€²
βŠ‘*β†’βŠ‘ {x = suc x} (βŠ‘*-∷ AβŠ‘Aβ€² Ξ“βŠ‘Ξ“β€²) Ξ“βˆ‹x  Ξ“β€²βˆ‹x = βŠ‘*β†’βŠ‘ Ξ“βŠ‘Ξ“β€² Ξ“βˆ‹x Ξ“β€²βˆ‹x


data _βŠ‘β‚•_ : (Ξ£ Ξ£β€² : HalfHeapContext) β†’ Set where

  βŠ‘-βˆ… : [] βŠ‘β‚• []

  βŠ‘-∷ : βˆ€ {Ξ£ Ξ£β€² T Tβ€² n} β†’ T βŠ‘α΅£ Tβ€² β†’ Ξ£ βŠ‘β‚• Ξ£β€² β†’ (⟨ n , T ⟩ ∷ Ξ£) βŠ‘β‚• (⟨ n , Tβ€² ⟩ ∷ Ξ£β€²)

_βŠ‘β‚˜_ : (Ξ£ Ξ£β€² : HeapContext) β†’ Set
⟨ Ξ£α΄Έ , Ξ£α΄΄ ⟩ βŠ‘β‚˜ ⟨ Ξ£α΄Έβ€² , Ξ£α΄΄β€² ⟩ = (Ξ£α΄Έ βŠ‘β‚• Ξ£α΄Έβ€²) Γ— (Ξ£α΄΄ βŠ‘β‚• Ξ£α΄΄β€²)

βŠ‘β‚˜-cons : βˆ€ {Ξ£ Ξ£β€² n β„“ T Tβ€²}
  β†’ T βŠ‘α΅£ Tβ€²
  β†’ Ξ£ βŠ‘β‚˜ Ξ£β€²
  β†’ cons-Ξ£ (a⟦ β„“ ⟧ n) T Ξ£ βŠ‘β‚˜ cons-Ξ£ (a⟦ β„“ ⟧ n) Tβ€² Ξ£β€²
βŠ‘β‚˜-cons {β„“ = low}  TβŠ‘Tβ€² ⟨ left , right ⟩ = ⟨ βŠ‘-∷ TβŠ‘Tβ€² left , right ⟩
βŠ‘β‚˜-cons {β„“ = high} TβŠ‘Tβ€² ⟨ left , right ⟩ = ⟨ left , βŠ‘-∷ TβŠ‘Tβ€² right ⟩

βŠ‘β‚•β†’βŠ‘-forward : βˆ€ {Ξ£ Ξ£β€² T n}
  β†’ Ξ£ βŠ‘β‚• Ξ£β€²
  β†’ find _β‰Ÿ_ Ξ£  n ≑ just T
    --------------------------------------
  β†’ βˆƒ[ Tβ€² ] (find _β‰Ÿ_ Ξ£β€² n ≑ just Tβ€²) Γ— (T βŠ‘α΅£ Tβ€²)
βŠ‘β‚•β†’βŠ‘-forward {⟨ nβ‚€ , T ⟩ ∷ _} {⟨ nβ‚€ , Tβ€² ⟩ ∷ _} {n = n} (βŠ‘-∷ TβŠ‘Tβ€² Ξ£βŠ‘Ξ£β€²) eq
  with n β‰Ÿ nβ‚€
... | no _ = βŠ‘β‚•β†’βŠ‘-forward Ξ£βŠ‘Ξ£β€² eq
... | yes refl with eq
... | refl = ⟨ _ , refl , TβŠ‘Tβ€² ⟩

βŠ‘β‚˜β†’βŠ‘-forward : βˆ€ {Ξ£ Ξ£β€² T n β„“Μ‚}
  β†’ Ξ£ βŠ‘β‚˜ Ξ£β€²
  β†’ let a = a⟦ β„“Μ‚ ⟧ n in
     lookup-Ξ£ Ξ£  a ≑ just T
  ------------------------------
  β†’ βˆƒ[ Tβ€² ] (lookup-Ξ£ Ξ£β€² a ≑ just Tβ€²) Γ— (T βŠ‘α΅£ Tβ€²)
βŠ‘β‚˜β†’βŠ‘-forward {β„“Μ‚ = low}  ⟨ Ξ£α΄ΈβŠ‘ , _ ⟩ Ξ£a≑T = βŠ‘β‚•β†’βŠ‘-forward Ξ£α΄ΈβŠ‘ Ξ£a≑T
βŠ‘β‚˜β†’βŠ‘-forward {β„“Μ‚ = high} ⟨ _ , Ξ£α΄΄βŠ‘ ⟩ Ξ£a≑T = βŠ‘β‚•β†’βŠ‘-forward Ξ£α΄΄βŠ‘ Ξ£a≑T

βŠ‘β‚•β†’βŠ‘-backward : βˆ€ {Ξ£ Ξ£β€² Tβ€² n}
  β†’ Ξ£ βŠ‘β‚• Ξ£β€²
  β†’ find _β‰Ÿ_ Ξ£β€² n ≑ just Tβ€²
    --------------------------------------
  β†’ βˆƒ[ T ] (find _β‰Ÿ_ Ξ£ n ≑ just T) Γ— (T βŠ‘α΅£ Tβ€²)
βŠ‘β‚•β†’βŠ‘-backward {⟨ nβ‚€ , T ⟩ ∷ _} {⟨ nβ‚€ , Tβ€² ⟩ ∷ _} {n = n} (βŠ‘-∷ TβŠ‘Tβ€² Ξ£βŠ‘Ξ£β€²) eq
  with n β‰Ÿ nβ‚€
... | no _ = βŠ‘β‚•β†’βŠ‘-backward Ξ£βŠ‘Ξ£β€² eq
... | yes refl with eq
... | refl = ⟨ _ , refl , TβŠ‘Tβ€² ⟩

βŠ‘β‚˜β†’βŠ‘-backward : βˆ€ {Ξ£ Ξ£β€² Tβ€² n β„“Μ‚}
  β†’ Ξ£ βŠ‘β‚˜ Ξ£β€²
  β†’ let a = a⟦ β„“Μ‚ ⟧ n in
     lookup-Ξ£ Ξ£β€² a ≑ just Tβ€²
  ------------------------------
  β†’ βˆƒ[ T ] (lookup-Ξ£ Ξ£ a ≑ just T) Γ— (T βŠ‘α΅£ Tβ€²)
βŠ‘β‚˜β†’βŠ‘-backward {β„“Μ‚ = low}  ⟨ Ξ£α΄ΈβŠ‘ , _ ⟩ Ξ£a≑T = βŠ‘β‚•β†’βŠ‘-backward Ξ£α΄ΈβŠ‘ Ξ£a≑T
βŠ‘β‚˜β†’βŠ‘-backward {β„“Μ‚ = high} ⟨ _ , Ξ£α΄΄βŠ‘ ⟩ Ξ£a≑T = βŠ‘β‚•β†’βŠ‘-backward Ξ£α΄΄βŠ‘ Ξ£a≑T

βŠ‘β‚˜β†’βŠ‘ : βˆ€ {Ξ£ Ξ£β€² T Tβ€² n β„“Μ‚}
  β†’ Ξ£ βŠ‘β‚˜ Ξ£β€²
  β†’ let a = a⟦ β„“Μ‚ ⟧ n in
     lookup-Ξ£ Ξ£  a ≑ just T
  β†’ lookup-Ξ£ Ξ£β€² a ≑ just Tβ€²
  β†’ T βŠ‘α΅£ Tβ€²
βŠ‘β‚˜β†’βŠ‘ {Ξ£} {Ξ£β€²} {T} {Tβ€²} {n} {β„“Μ‚} Ξ£βŠ‘Ξ£β€² eq eqβ€²
  with βŠ‘β‚˜β†’βŠ‘-forward {β„“Μ‚ = β„“Μ‚} Ξ£βŠ‘Ξ£β€² eq
... | ⟨ Tβ€³ , eqβ€³ , TβŠ‘Tβ€³ ⟩ with trans (sym eqβ€²) eqβ€³
... | refl = TβŠ‘Tβ€³