LambdaIFCStar/src/CC2/HeapContextPrecision.agda at master · Gradual-Typing/LambdaIFCStar · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
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″