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

Compare commits

base: DanilaFe:45f2babfa390ad860d7ecd11bd5bf9de85dd79cd
Branches Tags
DanilaFe:main
..
compare: DanilaFe:a55c786a51dca21c9688384d05e0e89966403900
Branches Tags
DanilaFe:main

No commits in common. "45f2babfa390ad860d7ecd11bd5bf9de85dd79cd" and "a55c786a51dca21c9688384d05e0e89966403900" have entirely different histories.
45f2babfa3 ... a55c786a51

6 changed files with 68 additions and 342 deletions
Show Stats Expand all files Collapse all files

11
Lattice.agda
View File

@ -145,14 +145,3 @@ record Lattice {a} (A : Set a) : Set (lsuc a) where
isLattice : IsLattice A _≈_ _⊔_ _⊓_
open IsLattice isLattice public
record FiniteHeightLattice {a} (A : Set a) : Set (lsuc a) where
field
height : ℕ
_≈_ : A → A → Set a
_⊔_ : A → A → A
_⊓_ : A → A → A
isFiniteHeightLattice : IsFiniteHeightLattice A height _≈_ _⊔_ _⊓_
open IsFiniteHeightLattice isFiniteHeightLattice public

78
Lattice/FiniteMap.agda
View File

@ -1,78 +0,0 @@
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 _⊔ℓ_)
open import Data.List using (List)
module Lattice.FiniteMap {a b : Level} (A : Set a) (B : Set b)
(_≈₂_ : B → B → Set b)
(_⊔₂_ : B → B → B) (_⊓₂_ : B → B → B)
(≡-dec-A : Decidable (_≡_ {a} {A}))
(lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB as Map
using (Map; ⊔-equal-keys; ⊓-equal-keys)
renaming
( _≈_ to _≈ᵐ_
; _⊔_ to _⊔ᵐ_
; _⊓_ to _⊓ᵐ_
; ≈-equiv to ≈ᵐ-equiv
; ≈-⊔-cong to ≈ᵐ-⊔ᵐ-cong
; ⊔-assoc to ⊔ᵐ-assoc
; ⊔-comm to ⊔ᵐ-comm
; ⊔-idemp to ⊔ᵐ-idemp
; ≈-⊓-cong to ≈ᵐ-⊓ᵐ-cong
; ⊓-assoc to ⊓ᵐ-assoc
; ⊓-comm to ⊓ᵐ-comm
; ⊓-idemp to ⊓ᵐ-idemp
; absorb-⊔-⊓ to absorb-⊔ᵐ-⊓ᵐ
; absorb-⊓-⊔ to absorb-⊓ᵐ-⊔ᵐ
)
open import Data.Product using (_×_; _,_; Σ; proj₁ ; proj₂)
open import Equivalence
module _ (ks : List A) where
FiniteMap : Set (a ⊔ℓ b)
FiniteMap = Σ Map (λ m → Map.keys m ≡ ks)
_≈_ : FiniteMap → FiniteMap → Set (a ⊔ℓ b)
_≈_ (m₁ , _) (m₂ , _) = m₁ ≈ᵐ m₂
_⊔_ : FiniteMap → FiniteMap → FiniteMap
_⊔_ (m₁ , km₁≡ks) (m₂ , km₂≡ks) = (m₁ ⊔ᵐ m₂ , trans (sym (⊔-equal-keys {m₁} {m₂} (trans (km₁≡ks) (sym km₂≡ks)))) km₁≡ks)
_⊓_ : FiniteMap → FiniteMap → FiniteMap
_⊓_ (m₁ , km₁≡ks) (m₂ , km₂≡ks) = (m₁ ⊓ᵐ m₂ , trans (sym (⊓-equal-keys {m₁} {m₂} (trans (km₁≡ks) (sym km₂≡ks)))) km₁≡ks)
≈-equiv : IsEquivalence FiniteMap _≈_
≈-equiv = record
{ ≈-refl = λ {(m , _)} → IsEquivalence.≈-refl ≈ᵐ-equiv {m}
; ≈-sym = λ {(m₁ , _)} {(m₂ , _)} → IsEquivalence.≈-sym ≈ᵐ-equiv {m₁} {m₂}
; ≈-trans = λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} → IsEquivalence.≈-trans ≈ᵐ-equiv {m₁} {m₂} {m₃}
}
isUnionSemilattice : IsSemilattice FiniteMap _≈_ _⊔_
isUnionSemilattice = record
{ ≈-equiv = ≈-equiv
; ≈-⊔-cong = λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} {(m₄ , _)} m₁≈m₂ m₃≈m₄ → ≈ᵐ-⊔ᵐ-cong {m₁} {m₂} {m₃} {m₄} m₁≈m₂ m₃≈m₄
; ⊔-assoc = λ (m₁ , _) (m₂ , _) (m₃ , _) → ⊔ᵐ-assoc m₁ m₂ m₃
; ⊔-comm = λ (m₁ , _) (m₂ , _) → ⊔ᵐ-comm m₁ m₂
; ⊔-idemp = λ (m , _) → ⊔ᵐ-idemp m
}
isIntersectSemilattice : IsSemilattice FiniteMap _≈_ _⊓_
isIntersectSemilattice = record
{ ≈-equiv = ≈-equiv
; ≈-⊔-cong = λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} {(m₄ , _)} m₁≈m₂ m₃≈m₄ → ≈ᵐ-⊓ᵐ-cong {m₁} {m₂} {m₃} {m₄} m₁≈m₂ m₃≈m₄
; ⊔-assoc = λ (m₁ , _) (m₂ , _) (m₃ , _) → ⊓ᵐ-assoc m₁ m₂ m₃
; ⊔-comm = λ (m₁ , _) (m₂ , _) → ⊓ᵐ-comm m₁ m₂
; ⊔-idemp = λ (m , _) → ⊓ᵐ-idemp m
}
isLattice : IsLattice FiniteMap _≈_ _⊔_ _⊓_
isLattice = record
{ joinSemilattice = isUnionSemilattice
; meetSemilattice = isIntersectSemilattice
; absorb-⊔-⊓ = λ (m₁ , _) (m₂ , _) → absorb-⊔ᵐ-⊓ᵐ m₁ m₂
; absorb-⊓-⊔ = λ (m₁ , _) (m₂ , _) → absorb-⊓ᵐ-⊔ᵐ m₁ m₂
}

107
Lattice/IterProd.agda
View File

@ -1,107 +0,0 @@
open import Lattice
module Lattice.IterProd {a} {A B : Set a}
(_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a)
(_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B)
(_⊓₁_ : A → A → A) (_⊓₂_ : B → B → B)
(lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
open import Agda.Primitive using (lsuc)
open import Data.Nat using (ℕ; suc; _+_)
open import Data.Product using (_×_)
open import Utils using (iterate)
open IsLattice lA renaming (FixedHeight to FixedHeight₁)
open IsLattice lB renaming (FixedHeight to FixedHeight₂)
IterProd : ℕ → Set a
IterProd k = iterate k (λ t → A × t) B
-- To make iteration more convenient, package the definitions in Lattice
-- records, perform the recursion, and unpackage.
private module _ where
BLattice : Lattice B
BLattice = record
{ _≈_ = _≈₂_
; _⊔_ = _⊔₂_
; _⊓_ = _⊓₂_
; isLattice = lB
}
IterProdLattice : ∀ {k : ℕ} → Lattice (IterProd k)
IterProdLattice {0} = BLattice
IterProdLattice {suc k'} = record
{ _≈_ = _≈_
; _⊔_ = _⊔_
; _⊓_ = _⊓_
; isLattice = isLattice
}
where
Right : Lattice (IterProd k')
Right = IterProdLattice {k'}
open import Lattice.Prod
_≈₁_ (Lattice._≈_ Right)
_⊔₁_ (Lattice._⊔_ Right)
_⊓₁_ (Lattice._⊓_ Right)
lA (Lattice.isLattice Right)
module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
(h₁ h₂ : ℕ)
(fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where
private module _ where
record FiniteHeightAndDecEq (A : Set a) : Set (lsuc a) where
field
height : ℕ
_≈_ : A → A → Set a
_⊔_ : A → A → A
_⊓_ : A → A → A
isFiniteHeightLattice : IsFiniteHeightLattice A height _≈_ _⊔_ _⊓_
≈-dec : IsDecidable _≈_
open IsFiniteHeightLattice isFiniteHeightLattice public
BFiniteHeightLattice : FiniteHeightAndDecEq B
BFiniteHeightLattice = record
{ height = h₂
; _≈_ = _≈₂_
; _⊔_ = _⊔₂_
; _⊓_ = _⊓₂_
; isFiniteHeightLattice = record
{ isLattice = lB
; fixedHeight = fhB
}
; ≈-dec = ≈₂-dec
}
IterProdFiniteHeightLattice : ∀ {k : ℕ} → FiniteHeightAndDecEq (IterProd k)
IterProdFiniteHeightLattice {0} = BFiniteHeightLattice
IterProdFiniteHeightLattice {suc k'} = record
{ height = h₁ + FiniteHeightAndDecEq.height Right
; _≈_ = _≈_
; _⊔_ = _⊔_
; _⊓_ = _⊓_
; isFiniteHeightLattice = isFiniteHeightLattice
≈₁-dec (FiniteHeightAndDecEq.≈-dec Right)
h₁ (FiniteHeightAndDecEq.height Right)
fhA (IsFiniteHeightLattice.fixedHeight (FiniteHeightAndDecEq.isFiniteHeightLattice Right))
; ≈-dec = ≈-dec ≈₁-dec (FiniteHeightAndDecEq.≈-dec Right)
}
where
Right = IterProdFiniteHeightLattice {k'}
open import Lattice.Prod
_≈₁_ (FiniteHeightAndDecEq._≈_ Right)
_⊔₁_ (FiniteHeightAndDecEq._⊔_ Right)
_⊓₁_ (FiniteHeightAndDecEq._⊓_ Right)
lA (FiniteHeightAndDecEq.isLattice Right)
module _ (k : ℕ) where
open FiniteHeightAndDecEq (IterProdFiniteHeightLattice {k}) using (fixedHeight) public
-- Expose the computed definition in public.
module _ (k : ℕ) where
open Lattice.Lattice (IterProdLattice {k}) public

163
Lattice/Map.agda
View File

@ -19,7 +19,6 @@ open import Data.List.Relation.Unary.Any using (Any; here; there) -- TODO: re-ex
open import Data.Product using (_×_; _,_; Σ; proj₁ ; proj₂)
open import Data.Empty using (⊥; ⊥-elim)
open import Equivalence
open import Utils using (Unique; push; empty; Unique-append; All¬-¬Any; All-x∈xs)
open IsLattice lB using () renaming
( ≈-refl to ≈₂-refl; ≈-sym to ≈₂-sym; ≈-trans to ≈₂-trans
@ -29,13 +28,35 @@ open IsLattice lB using () renaming
; absorb-⊔-⊓ to absorb-⊔₂-⊓₂; absorb-⊓-⊔ to absorb-⊓₂-⊔₂
)
private module ImplKeys where
keys : List (A × B) → List A
keys = map proj₁
keys : List (A × B) → List A
keys = map proj₁
data Unique {c} {C : Set c} : List C → Set c where
empty : Unique []
push : ∀ {x : C} {xs : List C}
→ All (λ x' → ¬ x ≡ x') xs
→ Unique xs
→ Unique (x ∷ xs)
Unique-append : ∀ {c} {C : Set c} {x : C} {xs : List C} →
¬ MemProp._∈_ x xs → Unique xs → Unique (xs ++ (x ∷ []))
Unique-append {c} {C} {x} {[]} _ _ = push [] empty
Unique-append {c} {C} {x} {x' ∷ xs'} x∉xs (push x'≢ uxs') =
push (help x'≢) (Unique-append (λ x∈xs' → x∉xs (there x∈xs')) uxs')
where
x'≢x : ¬ x' ≡ x
x'≢x x'≡x = x∉xs (here (sym x'≡x))
help : {l : List C} → All (λ x'' → ¬ x' ≡ x'') l → All (λ x'' → ¬ x' ≡ x'') (l ++ (x ∷ []))
help {[]} _ = x'≢x ∷ []
help {e ∷ es} (x'≢e ∷ x'≢es) = x'≢e ∷ help x'≢es
All¬-¬Any : ∀ {p c} {C : Set c} {P : C → Set p} {l : List C} → All (λ x → ¬ P x) l → ¬ Any P l
All¬-¬Any {l = x ∷ xs} (¬Px ∷ _) (here Px) = ¬Px Px
All¬-¬Any {l = x ∷ xs} (_ ∷ ¬Pxs) (there Pxs) = All¬-¬Any ¬Pxs Pxs
private module _ where
open MemProp using (_∈_)
open ImplKeys
unique-not-in : ∀ {k : A} {v : B} {l : List (A × B)} →
¬ (All (λ k' → ¬ k ≡ k') (keys l) × (k , v) ∈ l)
@ -87,7 +108,6 @@ private module ImplRelation where
private module ImplInsert (f : B → B → B) where
open import Data.List using (map)
open MemProp using (_∈_)
open ImplKeys
private
_∈k_ : A → List (A × B) → Set a
@ -133,20 +153,6 @@ private module ImplInsert (f : B → B → B) where
... | yes k∈kl rewrite insert-keys-∈ {v = v} k∈kl = u
... | no k∉kl rewrite sym (insert-keys-∉ {v = v} k∉kl) = Unique-append k∉kl u
union-subset-keys : ∀ {l₁ l₂ : List (A × B)} →
All (λ k → k ∈k l₂) (keys l₁) →
keys l₂ ≡ keys (union l₁ l₂)
union-subset-keys {[]} _ = refl
union-subset-keys {(k , v) ∷ l₁'} (k∈kl₂ ∷ kl₁'⊆kl₂)
rewrite union-subset-keys kl₁'⊆kl₂ =
insert-keys-∈ k∈kl₂
union-equal-keys : ∀ {l₁ l₂ : List (A × B)} →
keys l₁ ≡ keys l₂ → keys l₁ ≡ keys (union l₁ l₂)
union-equal-keys {l₁} {l₂} kl₁≡kl₂
with subst (λ l → All (λ k → k ∈ l) (keys l₁)) kl₁≡kl₂ (All-x∈xs (keys l₁))
... | kl₁⊆kl₂ = trans kl₁≡kl₂ (union-subset-keys {l₁} {l₂} kl₁⊆kl₂)
union-preserves-Unique : ∀ (l₁ l₂ : List (A × B)) →
Unique (keys l₂) → Unique (keys (union l₁ l₂))
union-preserves-Unique [] l₂ u₂ = u₂
@ -360,29 +366,6 @@ private module ImplInsert (f : B → B → B) where
let (k∈kl₁ , k∈kxs) = restrict-needs-both k∈l₁xs
in (k∈kl₁ , there k∈kxs)
restrict-subset-keys : ∀ {l₁ l₂ : List (A × B)} →
All (λ k → k ∈k l₁) (keys l₂) →
keys l₂ ≡ keys (restrict l₁ l₂)
restrict-subset-keys {l₁} {[]} _ = refl
restrict-subset-keys {l₁} {(k , v) ∷ l₂'} (k∈kl₁ ∷ kl₂'⊆kl₁)
with ∈k-dec k l₁
... | no k∉kl₁ = ⊥-elim (k∉kl₁ k∈kl₁)
... | yes _ rewrite restrict-subset-keys {l₁} {l₂'} kl₂'⊆kl₁ = refl
restrict-equal-keys : ∀ {l₁ l₂ : List (A × B)} →
keys l₁ ≡ keys l₂ →
keys l₁ ≡ keys (restrict l₁ l₂)
restrict-equal-keys {l₁} {l₂} kl₁≡kl₂
with subst (λ l → All (λ k → k ∈ l) (keys l₂)) (sym kl₁≡kl₂) (All-x∈xs (keys l₂))
... | kl₂⊆kl₁ = trans kl₁≡kl₂ (restrict-subset-keys {l₁} {l₂} kl₂⊆kl₁)
intersect-equal-keys : ∀ {l₁ l₂ : List (A × B)} →
keys l₁ ≡ keys l₂ →
keys l₁ ≡ keys (intersect l₁ l₂)
intersect-equal-keys {l₁} {l₂} kl₁≡kl₂
rewrite restrict-equal-keys (trans kl₁≡kl₂ (updates-keys {l₁} {l₂}))
rewrite updates-keys {l₁} {l₂} = refl
restrict-preserves-∉₁ : ∀ {k : A} {l₁ l₂ : List (A × B)} →
¬ k ∈k l₁ → ¬ k ∈k restrict l₁ l₂
restrict-preserves-∉₁ {k} {l₁} {l₂} k∉kl₁ k∈kl₁l₂ =
@ -465,16 +448,13 @@ private module ImplInsert (f : B → B → B) where
Map : Set (a ⊔ℓ b)
Map = Σ (List (A × B)) (λ l → Unique (ImplKeys.keys l))
keys : Map → List A
keys (kvs , _) = ImplKeys.keys kvs
Map = Σ (List (A × B)) (λ l → Unique (keys l))
_∈_ : (A × B) → Map → Set (a ⊔ℓ b)
_∈_ p (kvs , _) = MemProp._∈_ p kvs
_∈k_ : A → Map → Set a
_∈k_ k m = MemProp._∈_ k (keys m)
_∈k_ k (kvs , _) = MemProp._∈_ k (keys kvs)
Map-functional : ∀ {k : A} {v v' : B} {m : Map} → (k , v) ∈ m → (k , v') ∈ m → v ≡ v'
Map-functional {m = (l , ul)} k,v∈m k,v'∈m = ListAB-functional ul k,v∈m k,v'∈m
@ -512,8 +492,8 @@ data Expr : Set (a ⊔ℓ b) where
_∪_ : Expr → Expr → Expr
_∩_ : Expr → Expr → Expr
open ImplInsert _⊔₂_ using (union-preserves-Unique; union-equal-keys) renaming (insert to insert-impl; union to union-impl)
open ImplInsert _⊓₂_ using (intersect-preserves-Unique; intersect-equal-keys) renaming (intersect to intersect-impl)
open ImplInsert _⊔₂_ using (union-preserves-Unique) renaming (insert to insert-impl; union to union-impl)
open ImplInsert _⊓₂_ using (intersect-preserves-Unique) renaming (intersect to intersect-impl)
_⊔_ : Map → Map → Map
_⊔_ (kvs₁ , _) (kvs₂ , uks₂) = (union-impl kvs₁ kvs₂ , union-preserves-Unique kvs₁ kvs₂ uks₂)
@ -573,46 +553,45 @@ Expr-Provenance k (e₁ ∩ e₂) k∈ke₁e₂
... | no k∉ke₁ | yes k∈ke₂ = ⊥-elim (intersect-preserves-∉₁ {l₂ = proj₁ ⟦ e₂ ⟧} k∉ke₁ k∈ke₁e₂)
... | no k∉ke₁ | no k∉ke₂ = ⊥-elim (intersect-preserves-∉₂ {l₁ = proj₁ ⟦ e₁ ⟧} k∉ke₂ k∈ke₁e₂)
data SubsetInfo (m₁ m₂ : Map) : Set (a ⊔ℓ b) where
extra : (k : A) → k ∈k m₁ → ¬ k ∈k m₂ → SubsetInfo m₁ m₂
mismatch : (k : A) (v₁ v₂ : B) → (k , v₁) ∈ m₁ → (k , v₂) ∈ m₂ → ¬ v₁ ≈₂ v₂ → SubsetInfo m₁ m₂
fine : m₁ ⊆ m₂ → SubsetInfo m₁ m₂
SubsetInfo-to-dec : ∀ {m₁ m₂ : Map} → SubsetInfo m₁ m₂ → Dec (m₁ ⊆ m₂)
SubsetInfo-to-dec (extra k k∈km₁ k∉km₂) =
let (v , k,v∈m₁) = locate k∈km₁
in no (λ m₁⊆m₂ →
let (v' , (_ , k,v'∈m₂)) = m₁⊆m₂ k v k,v∈m₁
in k∉km₂ (∈-cong proj₁ k,v'∈m₂))
SubsetInfo-to-dec {m₁} {m₂} (mismatch k v₁ v₂ k,v₁∈m₁ k,v₂∈m₂ v₁̷≈v₂) =
no (λ m₁⊆m₂ →
let (v' , (v₁≈v' , k,v'∈m₂)) = m₁⊆m₂ k v₁ k,v₁∈m₁
in v₁̷≈v₂ (subst (λ v'' → v₁ ≈₂ v'') (Map-functional {k} {v'} {v₂} {m₂} k,v'∈m₂ k,v₂∈m₂) v₁≈v')) -- for some reason, can't just use subst...
SubsetInfo-to-dec (fine m₁⊆m₂) = yes m₁⊆m₂
module _ (≈₂-dec : ∀ (b₁ b₂ : B) → Dec (b₁ ≈₂ b₂)) where
private module _ where
data SubsetInfo (m₁ m₂ : Map) : Set (a ⊔ℓ b) where
extra : (k : A) → k ∈k m₁ → ¬ k ∈k m₂ → SubsetInfo m₁ m₂
mismatch : (k : A) (v₁ v₂ : B) → (k , v₁) ∈ m₁ → (k , v₂) ∈ m₂ → ¬ v₁ ≈₂ v₂ → SubsetInfo m₁ m₂
fine : m₁ ⊆ m₂ → SubsetInfo m₁ m₂
SubsetInfo-to-dec : ∀ {m₁ m₂ : Map} → SubsetInfo m₁ m₂ → Dec (m₁ ⊆ m₂)
SubsetInfo-to-dec (extra k k∈km₁ k∉km₂) =
let (v , k,v∈m₁) = locate k∈km₁
in no (λ m₁⊆m₂ →
let (v' , (_ , k,v'∈m₂)) = m₁⊆m₂ k v k,v∈m₁
in k∉km₂ (∈-cong proj₁ k,v'∈m₂))
SubsetInfo-to-dec {m₁} {m₂} (mismatch k v₁ v₂ k,v₁∈m₁ k,v₂∈m₂ v₁̷≈v₂) =
no (λ m₁⊆m₂ →
let (v' , (v₁≈v' , k,v'∈m₂)) = m₁⊆m₂ k v₁ k,v₁∈m₁
in v₁̷≈v₂ (subst (λ v'' → v₁ ≈₂ v'') (Map-functional {k} {v'} {v₂} {m₂} k,v'∈m₂ k,v₂∈m₂) v₁≈v')) -- for some reason, can't just use subst...
SubsetInfo-to-dec (fine m₁⊆m₂) = yes m₁⊆m₂
compute-SubsetInfo : ∀ m₁ m₂ → SubsetInfo m₁ m₂
compute-SubsetInfo ([] , _) m₂ = fine (λ k v ())
compute-SubsetInfo m₁@((k , v) ∷ xs₁ , push k≢xs₁ uxs₁) m₂@(l₂ , u₂)
with compute-SubsetInfo (xs₁ , uxs₁) m₂
... | extra k' k'∈kxs₁ k'∉km₂ = extra k' (there k'∈kxs₁) k'∉km₂
... | mismatch k' v₁ v₂ k',v₁∈xs₁ k',v₂∈m₂ v₁̷≈v₂ =
mismatch k' v₁ v₂ (there k',v₁∈xs₁) k',v₂∈m₂ v₁̷≈v₂
... | fine xs₁⊆m₂ with ∈k-dec k l₂
... | no k∉km₂ = extra k (here refl) k∉km₂
... | yes k∈km₂ with locate k∈km₂
... | (v' , k,v'∈m₂) with ≈₂-dec v v'
... | no v̷≈v' = mismatch k v v' (here refl) (k,v'∈m₂) v̷≈v'
... | yes v≈v' = fine m₁⊆m₂
where
m₁⊆m₂ : m₁ ⊆ m₂
m₁⊆m₂ k' v'' (here k,v≡k',v'')
rewrite cong proj₁ k,v≡k',v''
rewrite cong proj₂ k,v≡k',v'' =
(v' , (v≈v' , k,v'∈m₂))
m₁⊆m₂ k' v'' (there k,v≡k',v'') =
xs₁⊆m₂ k' v'' k,v≡k',v''
compute-SubsetInfo : ∀ m₁ m₂ → SubsetInfo m₁ m₂
compute-SubsetInfo ([] , _) m₂ = fine (λ k v ())
compute-SubsetInfo m₁@((k , v) ∷ xs₁ , push k≢xs₁ uxs₁) m₂@(l₂ , u₂)
with compute-SubsetInfo (xs₁ , uxs₁) m₂
... | extra k' k'∈kxs₁ k'∉km₂ = extra k' (there k'∈kxs₁) k'∉km₂
... | mismatch k' v₁ v₂ k',v₁∈xs₁ k',v₂∈m₂ v₁̷≈v₂ =
mismatch k' v₁ v₂ (there k',v₁∈xs₁) k',v₂∈m₂ v₁̷≈v₂
... | fine xs₁⊆m₂ with ∈k-dec k l₂
... | no k∉km₂ = extra k (here refl) k∉km₂
... | yes k∈km₂ with locate k∈km₂
... | (v' , k,v'∈m₂) with ≈₂-dec v v'
... | no v̷≈v' = mismatch k v v' (here refl) (k,v'∈m₂) v̷≈v'
... | yes v≈v' = fine m₁⊆m₂
where
m₁⊆m₂ : m₁ ⊆ m₂
m₁⊆m₂ k' v'' (here k,v≡k',v'')
rewrite cong proj₁ k,v≡k',v''
rewrite cong proj₂ k,v≡k',v'' =
(v' , (v≈v' , k,v'∈m₂))
m₁⊆m₂ k' v'' (there k,v≡k',v'') =
xs₁⊆m₂ k' v'' k,v≡k',v''
⊆-dec : ∀ m₁ m₂ → Dec (m₁ ⊆ m₂)
⊆-dec m₁ m₂ = SubsetInfo-to-dec (compute-SubsetInfo m₁ m₂)
@ -881,9 +860,3 @@ isLattice = record
; absorb-⊔-⊓ = absorb-⊔-⊓
; absorb-⊓-⊔ = absorb-⊓-⊔
}
⊔-equal-keys : ∀ {m₁ m₂ : Map} → keys m₁ ≡ keys m₂ → keys m₁ ≡ keys (m₁ ⊔ m₂)
⊔-equal-keys km₁≡km₂ = union-equal-keys km₁≡km₂
⊓-equal-keys : ∀ {m₁ m₂ : Map} → keys m₁ ≡ keys m₂ → keys m₁ ≡ keys (m₁ ⊓ m₂)
⊓-equal-keys km₁≡km₂ = intersect-equal-keys km₁≡km₂

10
Lattice/Prod.agda
View File

@ -94,16 +94,6 @@ isLattice = record
)
}
module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_) where
≈-dec : IsDecidable _≈_
≈-dec (a₁ , b₁) (a₂ , b₂)
with ≈₁-dec a₁ a₂ | ≈₂-dec b₁ b₂
... | yes a₁≈a₂ | yes b₁≈b₂ = yes (a₁≈a₂ , b₁≈b₂)
... | no a₁̷≈a₂ | _ = no (λ (a₁≈a₂ , _) → a₁̷≈a₂ a₁≈a₂)
... | _ | no b₁̷≈b₂ = no (λ (_ , b₁≈b₂) → b₁̷≈b₂ b₁≈b₂)
module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
(h₁ h₂ : ℕ)
(fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where

41
Utils.agda
View File

@ -1,41 +0,0 @@
module Utils where
open import Data.Nat using (ℕ; suc)
open import Data.List using (List; []; _∷_; _++_)
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Relation.Unary.All using (All; []; _∷_; map)
open import Data.List.Relation.Unary.Any using (Any; here; there) -- TODO: re-export these with nicer names from map
open import Relation.Binary.PropositionalEquality using (_≡_; sym; refl)
open import Relation.Nullary using (¬_)
data Unique {c} {C : Set c} : List C → Set c where
empty : Unique []
push : ∀ {x : C} {xs : List C}
→ All (λ x' → ¬ x ≡ x') xs
→ Unique xs
→ Unique (x ∷ xs)
Unique-append : ∀ {c} {C : Set c} {x : C} {xs : List C} →
¬ x ∈ xs → Unique xs → Unique (xs ++ (x ∷ []))
Unique-append {c} {C} {x} {[]} _ _ = push [] empty
Unique-append {c} {C} {x} {x' ∷ xs'} x∉xs (push x'≢ uxs') =
push (help x'≢) (Unique-append (λ x∈xs' → x∉xs (there x∈xs')) uxs')
where
x'≢x : ¬ x' ≡ x
x'≢x x'≡x = x∉xs (here (sym x'≡x))
help : {l : List C} → All (λ x'' → ¬ x' ≡ x'') l → All (λ x'' → ¬ x' ≡ x'') (l ++ (x ∷ []))
help {[]} _ = x'≢x ∷ []
help {e ∷ es} (x'≢e ∷ x'≢es) = x'≢e ∷ help x'≢es
All¬-¬Any : ∀ {p c} {C : Set c} {P : C → Set p} {l : List C} → All (λ x → ¬ P x) l → ¬ Any P l
All¬-¬Any {l = x ∷ xs} (¬Px ∷ _) (here Px) = ¬Px Px
All¬-¬Any {l = x ∷ xs} (_ ∷ ¬Pxs) (there Pxs) = All¬-¬Any ¬Pxs Pxs
All-x∈xs : ∀ {a} {A : Set a} (xs : List A) → All (λ x → x ∈ xs) xs
All-x∈xs [] = []
All-x∈xs (x ∷ xs') = here refl ∷ map there (All-x∈xs xs')
iterate : ∀ {a} {A : Set a} (n : ℕ) → (f : A → A) → A → A
iterate 0 _ a = a
iterate (suc n) f a = f (iterate n f a)