module CC.BigStepErased 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 hiding ([_])
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.Binary.PropositionalEquality using (_β‘_; refl)
open import Common.Utils
open import Common.Types
open import CC.CCStatics
open import Memory.Heap Term Value
infix 2 _β£_β’_ββ_β£_
data _β£_β’_ββ_β£_ : HalfHeap β StaticLabel β (M V : Term) β HalfHeap β Set
ββ-value : β {ΞΌ ΞΌβ² pc M V} β ΞΌ β£ pc β’ M ββ V β£ ΞΌβ² β Value V
data _β£_β’_ββ_β£_ where
ββ-val : β {ΞΌ pc V}
β Value V
β ΞΌ β£ pc β’ V ββ V β£ ΞΌ
ββ-app : β {ΞΌ ΞΌβ ΞΌβ ΞΌβ pc pcβ² L M N V W A}
β ΞΌ β£ pc β’ L ββ Ζβ¦ pcβ² β§ A Λ N of low β£ ΞΌβ
β ΞΌβ β£ pc β’ M ββ V β£ ΞΌβ
β ΞΌβ β£ pc β’ N [ V ] ββ W β£ ΞΌβ
β ΞΌ β£ pc β’ L Β· M ββ W β£ ΞΌβ
ββ-app-β : β {ΞΌ ΞΌβ ΞΌβ pc L M V}
β ΞΌ β£ pc β’ L ββ β β£ ΞΌβ
β ΞΌβ β£ pc β’ M ββ V β£ ΞΌβ
β ΞΌ β£ pc β’ L Β· M ββ β β£ ΞΌβ
ββ-if-true : β {ΞΌ ΞΌβ ΞΌβ pc L M N V A}
β ΞΌ β£ pc β’ L ββ $ true of low β£ ΞΌβ
β ΞΌβ β£ pc β’ M ββ V β£ ΞΌβ
β ΞΌ β£ pc β’ if L A M N ββ V β£ ΞΌβ
ββ-if-false : β {ΞΌ ΞΌβ ΞΌβ pc L M N V A}
β ΞΌ β£ pc β’ L ββ $ false of low β£ ΞΌβ
β ΞΌβ β£ pc β’ N ββ V β£ ΞΌβ
β ΞΌ β£ pc β’ if L A M N ββ V β£ ΞΌβ
ββ-if-β : β {ΞΌ ΞΌβ pc L M N A}
β ΞΌ β£ pc β’ L ββ β β£ ΞΌβ
β ΞΌ β£ pc β’ if L A M N ββ β β£ ΞΌβ
ββ-let : β {ΞΌ ΞΌβ ΞΌβ pc M N V W}
β ΞΌ β£ pc β’ M ββ V β£ ΞΌβ
β ΞΌβ β£ pc β’ N [ V ] ββ W β£ ΞΌβ
β ΞΌ β£ pc β’ `let M N ββ W β£ ΞΌβ
ββ-ref? : β {ΞΌ ΞΌβ pc M V n}
β (βV : ΞΌ β£ pc β’ M ββ V β£ ΞΌβ)
β n β‘ length ΞΌβ
β pc βΌ low
β ΞΌ β£ pc β’ ref?β¦ low β§ M ββ addr (aβ¦ low β§ n) of low β£ β¨ n , V & ββ-value βV β© β· ΞΌβ
ββ-ref?-β : β {ΞΌ ΞΌβ pc M V}
β (βV : ΞΌ β£ pc β’ M ββ V β£ ΞΌβ)
β ΞΌ β£ pc β’ ref?β¦ high β§ M ββ β β£ ΞΌβ
ββ-ref : β {ΞΌ ΞΌβ pc M V n}
β (βV : ΞΌ β£ pc β’ M ββ V β£ ΞΌβ)
β n β‘ length ΞΌβ
β ΞΌ β£ pc β’ refβ¦ low β§ M ββ addr (aβ¦ low β§ n) of low β£ β¨ n , V & ββ-value βV β© β· ΞΌβ
ββ-ref-β : β {ΞΌ ΞΌβ pc M V}
β (βV : ΞΌ β£ pc β’ M ββ V β£ ΞΌβ)
β ΞΌ β£ pc β’ refβ¦ high β§ M ββ β β£ ΞΌβ
ββ-deref : β {ΞΌ ΞΌβ pc M V v n}
β ΞΌ β£ pc β’ M ββ addr (aβ¦ low β§ n) of low β£ ΞΌβ
β find _β_ ΞΌβ n β‘ just (V & v)
β ΞΌ β£ pc β’ ! M ββ V β£ ΞΌβ
ββ-deref-β : β {ΞΌ ΞΌβ pc M}
β ΞΌ β£ pc β’ M ββ β β£ ΞΌβ
β ΞΌ β£ pc β’ ! M ββ β β£ ΞΌβ
ββ-assign? : β {ΞΌ ΞΌβ ΞΌβ pc L M V n}
β ΞΌ β£ pc β’ L ββ addr (aβ¦ low β§ n) of low β£ ΞΌβ
β (βV : ΞΌβ β£ pc β’ M ββ V β£ ΞΌβ)
β pc βΌ low
β ΞΌ β£ pc β’ L :=? M ββ $ tt of low β£ β¨ n , V & ββ-value βV β© β· ΞΌβ
ββ-assign?-β : β {ΞΌ ΞΌβ ΞΌβ pc L M V}
β ΞΌ β£ pc β’ L ββ β β£ ΞΌβ
β ΞΌβ β£ pc β’ M ββ V β£ ΞΌβ
β ΞΌ β£ pc β’ L :=? M ββ $ tt of low β£ ΞΌβ
ββ-assign : β {ΞΌ ΞΌβ ΞΌβ pc L M V n}
β ΞΌ β£ pc β’ L ββ addr (aβ¦ low β§ n) of low β£ ΞΌβ
β (βV : ΞΌβ β£ pc β’ M ββ V β£ ΞΌβ)
β ΞΌ β£ pc β’ L := M ββ $ tt of low β£ β¨ n , V & ββ-value βV β© β· ΞΌβ
ββ-assign-β : β {ΞΌ ΞΌβ ΞΌβ pc L M V}
β ΞΌ β£ pc β’ L ββ β β£ ΞΌβ
β ΞΌβ β£ pc β’ M ββ V β£ ΞΌβ
β ΞΌ β£ pc β’ L := M ββ $ tt of low β£ ΞΌβ
ββ-value (ββ-val v) = v
ββ-value (ββ-app _ _ βV) = ββ-value βV
ββ-value (ββ-app-β _ _) = V-β
ββ-value (ββ-if-true _ βV) = ββ-value βV
ββ-value (ββ-if-false _ βV) = ββ-value βV
ββ-value (ββ-if-β βV) = V-β
ββ-value (ββ-let _ βV) = ββ-value βV
ββ-value (ββ-ref? _ _ _) = V-addr
ββ-value (ββ-ref?-β _) = V-β
ββ-value (ββ-ref _ _) = V-addr
ββ-value (ββ-ref-β _) = V-β
ββ-value (ββ-deref {v = v} _ _) = v
ββ-value (ββ-deref-β _) = V-β
ββ-value (ββ-assign? _ _ _) = V-const
ββ-value (ββ-assign?-β _ _) = V-const
ββ-value (ββ-assign _ _) = V-const
ββ-value (ββ-assign-β _ _) = V-const
VββV : β {ΞΌ ΞΌβ² pc V W}
β ΞΌ β£ pc β’ V ββ W β£ ΞΌβ²
β Value V
β V β‘ W Γ ΞΌ β‘ ΞΌβ²
VββV (ββ-val _) v = β¨ refl , refl β©
ββ-trans : β {ΞΌ ΞΌβ ΞΌβ pc M V W}
β ΞΌ β£ pc β’ M ββ V β£ ΞΌβ
β ΞΌβ β£ pc β’ V ββ W β£ ΞΌβ
β ΞΌ β£ pc β’ M ββ W β£ ΞΌβ
ββ-trans MβV VβW with VββV VβW (ββ-value MβV)
... | β¨ refl , refl β© = MβV
ββ-app-β-inv : β {ΞΌ ΞΌβ² pc V W}
β ΞΌ β£ pc β’ β Β· V ββ W β£ ΞΌβ²
β Value V
β W β‘ β Γ ΞΌ β‘ ΞΌβ²
ββ-app-β-inv (ββ-app-β βββ VβV) v
with VββV βββ V-β | VββV VβV v
... | β¨ refl , refl β© | β¨ refl , refl β© = β¨ refl , refl β©
ββ-app-inv : β {ΞΌ ΞΌβ² pc pcβ² N V W A}
β ΞΌ β£ pc β’ Ζβ¦ pcβ² β§ A Λ N of low Β· V ββ W β£ ΞΌβ²
β Value V
β ΞΌ β£ pc β’ N [ V ] ββ W β£ ΞΌβ²
ββ-app-inv (ββ-app ΖNβΖN VβV Nβ¦Vβ§βW) v
with VββV ΖNβΖN V-Ζ | VββV VβV v
... | β¨ refl , refl β© | β¨ refl , refl β© = Nβ¦Vβ§βW
ββ-assign-β-inv : β {ΞΌ ΞΌβ² pc M V}
β ΞΌ β£ pc β’ β := M ββ V β£ ΞΌβ²
β V β‘ $ tt of low Γ β[ W ] (ΞΌ β£ pc β’ M ββ W β£ ΞΌβ²)
ββ-assign-β-inv (ββ-assign-β βββ MβW)
with VββV βββ V-β
... | β¨ refl , refl β© = β¨ refl , _ , MβW β©
ββ-assign-inv : β {ΞΌ ΞΌβ² pc M V n}
β ΞΌ β£ pc β’ (addr aβ¦ low β§ n of low) := M ββ V β£ ΞΌβ²
β V β‘ $ tt of low Γ β[ W ] β[ w ] β[ ΞΌβ³ ] (ΞΌ β£ pc β’ M ββ W β£ ΞΌβ³) Γ (ΞΌβ² β‘ β¨ n , W & w β© β· ΞΌβ³)
ββ-assign-inv (ββ-assign aβa MβW)
with VββV aβa V-addr
... | β¨ refl , refl β© = β¨ refl , _ , ββ-value MβW , _ , MβW , refl β©
ββ-assign?-β-inv : β {ΞΌ ΞΌβ² pc M V}
β ΞΌ β£ pc β’ β :=? M ββ V β£ ΞΌβ²
β V β‘ $ tt of low Γ β[ W ] (ΞΌ β£ pc β’ M ββ W β£ ΞΌβ²)
ββ-assign?-β-inv (ββ-assign?-β βββ MβW)
with VββV βββ V-β
... | β¨ refl , refl β© = β¨ refl , _ , MβW β©
ββ-assign?-inv : β {ΞΌ ΞΌβ² pc M V n}
β ΞΌ β£ pc β’ (addr aβ¦ low β§ n of low) :=? M ββ V β£ ΞΌβ²
β V β‘ $ tt of low Γ pc βΌ low Γ β[ W ] β[ w ] β[ ΞΌβ³ ] (ΞΌ β£ pc β’ M ββ W β£ ΞΌβ³) Γ (ΞΌβ² β‘ β¨ n , W & w β© β· ΞΌβ³)
ββ-assign?-inv (ββ-assign? aβa MβW pcβΌlow)
with VββV aβa V-addr
... | β¨ refl , refl β© = β¨ refl , pcβΌlow , _ , ββ-value MβW , _ , MβW , refl β©
ββ-deref-β-inv : β {ΞΌ ΞΌβ² pc V}
β ΞΌ β£ pc β’ ! β ββ V β£ ΞΌβ²
β V β‘ β Γ ΞΌ β‘ ΞΌβ²
ββ-deref-β-inv (ββ-deref-β βββ) with VββV βββ V-β
... | β¨ refl , refl β© = β¨ refl , refl β©
ββ-deref-inv : β {ΞΌ ΞΌβ² pc V n}
β ΞΌ β£ pc β’ ! (addr aβ¦ low β§ n of low) ββ V β£ ΞΌβ²
β (β[ v ] find _β_ ΞΌ n β‘ just (V & v)) Γ ΞΌ β‘ ΞΌβ²
ββ-deref-inv (ββ-deref {v = v} aβa eq) with VββV aβa V-addr
... | β¨ refl , refl β© = β¨ β¨ v , eq β© , refl β©