DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Some early refactors of FiniteValueMap

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-03-02 15:18:10 -08:00
parent 03cdc65a7b
commit fbbcd72037
1 changed files with 34 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

40
Lattice/FiniteValueMap.agda
View File

@ -4,7 +4,8 @@
open import Lattice open import Lattice
open import Equivalence open import Equivalence
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst) open import Relation.Binary.PropositionalEquality as Eq
using (_≡_; refl; sym; trans; cong; subst)
open import Relation.Binary.Definitions using (Decidable) open import Relation.Binary.Definitions using (Decidable)
open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_) open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
open import Function.Definitions using (Inverseˡ; Inverseʳ) open import Function.Definitions using (Inverseˡ; Inverseʳ)
@ -27,18 +28,45 @@ open import Data.List.Relation.Unary.All using (All)
open import Data.List.Relation.Unary.Any using (Any; here; there) open import Data.List.Relation.Unary.Any using (Any; here; there)
open import Relation.Nullary using (¬_) open import Relation.Nullary using (¬_)
open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB using (subset-impl; locate; forget; _∈_; Map-functional; Expr-Provenance; _∩_; _∪_; `_; in₁; in₂; bothᵘ; single; ⊔-combines) open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB
using
( subset-impl
; locate; forget
; _∈_
; Map-functional
; Expr-Provenance
; _∩_; _∪_; `_
; in₁; in₂; bothᵘ; single
; ⊔-combines
)
open import Lattice.FiniteMap A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB public open import Lattice.FiniteMap A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB public
module IterProdIsomorphism where module IterProdIsomorphism where
open import Data.Unit using (⊤; tt) open import Data.Unit using (⊤; tt)
open import Lattice.Unit using () renaming (_≈_ to _≈ᵘ_; _⊔_ to _⊔ᵘ_; _⊓_ to _⊓ᵘ_; ≈-dec to ≈ᵘ-dec; isLattice to isLatticeᵘ; ≈-equiv to ≈ᵘ-equiv; fixedHeight to fixedHeightᵘ) open import Lattice.Unit using ()
open import Lattice.IterProd _≈₂_ _≈ᵘ_ _⊔₂_ _⊔ᵘ_ _⊓₂_ _⊓ᵘ_ lB isLatticeᵘ as IP using (IterProd) renaming
open IsLattice lB using () renaming (≈-trans to ≈₂-trans; ≈-sym to ≈₂-sym; FixedHeight to FixedHeight₂) ( _≈_ to _≈ᵘ_
; _⊔_ to _⊔ᵘ_
; _⊓_ to _⊓ᵘ_
; ≈-dec to ≈ᵘ-dec
; isLattice to isLatticeᵘ
; ≈-equiv to ≈ᵘ-equiv
; fixedHeight to fixedHeightᵘ
)
open import Lattice.IterProd _≈₂_ _≈ᵘ_ _⊔₂_ _⊔ᵘ_ _⊓₂_ _⊓ᵘ_ lB isLatticeᵘ
as IP
using (IterProd)
open IsLattice lB using ()
renaming
( ≈-trans to ≈₂-trans
; ≈-sym to ≈₂-sym
; FixedHeight to FixedHeight₂
)
from : ∀ {ks : List A} → FiniteMap ks → IterProd (length ks) from : ∀ {ks : List A} → FiniteMap ks → IterProd (length ks)
from {[]} (([] , _) , _) = tt from {[]} (([] , _) , _) = tt
from {k ∷ ks'} (((k' , v) ∷ fm' , push _ uks') , refl) = (v , from ((fm' , uks'), refl)) from {k ∷ ks'} (((k' , v) ∷ fm' , push _ uks') , refl) =
(v , from ((fm' , uks'), refl))
to : ∀ {ks : List A} → Unique ks → IterProd (length ks) → FiniteMap ks to : ∀ {ks : List A} → Unique ks → IterProd (length ks) → FiniteMap ks
to {[]} _ ⊤ = (([] , empty) , refl) to {[]} _ ⊤ = (([] , empty) , refl)