46 lines
1.5 KiB
Plaintext
46 lines
1.5 KiB
Plaintext
open import Lattice
|
||
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst)
|
||
open import Relation.Binary.Definitions using (Decidable)
|
||
open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
|
||
|
||
module Lattice.MapSet {a : Level} {A : Set a} (≡-dec-A : Decidable (_≡_ {a} {A})) where
|
||
|
||
open import Data.List using (List; map)
|
||
open import Data.Product using (_,_; proj₁)
|
||
open import Function using (_∘_)
|
||
|
||
open import Lattice.Unit using (⊤; tt) renaming (_≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_; isLattice to ⊤-isLattice)
|
||
import Lattice.Map
|
||
|
||
private module UnitMap = Lattice.Map ≡-dec-A ⊤-isLattice
|
||
open UnitMap
|
||
using (Map; Expr; ⟦_⟧)
|
||
renaming
|
||
( Expr-Provenance to Expr-Provenanceᵐ
|
||
)
|
||
open UnitMap
|
||
using
|
||
( _⊆_; _≈_; ≈-equiv; _⊔_; _⊓_; _∪_ ; _∩_ ; `_; empty; forget
|
||
; isUnionSemilattice; isIntersectSemilattice; isLattice; lattice
|
||
; Provenance
|
||
; ⊔-preserves-∈k₁
|
||
; ⊔-preserves-∈k₂
|
||
)
|
||
renaming (_∈k_ to _∈_) public
|
||
open Provenance public
|
||
|
||
MapSet : Set a
|
||
MapSet = Map
|
||
|
||
to-List : MapSet → List A
|
||
to-List = map proj₁ ∘ proj₁
|
||
|
||
insert : A → MapSet → MapSet
|
||
insert k = UnitMap.insert k tt
|
||
|
||
singleton : A → MapSet
|
||
singleton k = UnitMap.insert k tt empty
|
||
|
||
Expr-Provenance : ∀ (k : A) (e : Expr) → k ∈ ⟦ e ⟧ → Provenance k tt e
|
||
Expr-Provenance k e k∈e = let (tt , (prov , _)) = Expr-Provenanceᵐ k e k∈e in prov
|