Compare commits

...

9 Commits

Author SHA1 Message Date
56c72e1388 Delete unused homomorphism proof that was broken by an Agda update.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-03-09 14:07:56 -08:00
0c30f8be48 Start on sign analysis (mostly just imports)
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-03-09 14:00:10 -08:00
75f981cb75 Define simple sequential-only programs
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-03-09 13:59:48 -08:00
ca99e18184 Tweak exports from finite value bundle to avoid (some) redundant arguments
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-03-09 13:59:22 -08:00
702cf2c298 Expose more functionaity from the set lattice
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-03-09 13:58:40 -08:00
0c088ca2ae Prove multi-key access monotonicity in finite maps
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-03-09 13:58:07 -08:00
bc138d87f0 Prove things about key-based access in map
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-03-09 13:57:29 -08:00
311ed75186 Expose more helpers from 'Map'
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-03-09 13:57:02 -08:00
1ccc6f08e5 Add more properties of uniqueness
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-03-09 13:54:01 -08:00
9 changed files with 301 additions and 182 deletions

50
Analysis/Sign.agda Normal file
View File

@ -0,0 +1,50 @@
module Analysis.Sign where
open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Language
open import Lattice
data Sign : Set where
+ : Sign
- : Sign
: Sign
-- g for siGn; s is used for strings and i is not very descriptive.
_≟ᵍ_ : IsDecidable (_≡_ {_} {Sign})
_≟ᵍ_ + + = yes refl
_≟ᵍ_ + - = no (λ ())
_≟ᵍ_ + 0ˢ = no (λ ())
_≟ᵍ_ - + = no (λ ())
_≟ᵍ_ - - = yes refl
_≟ᵍ_ - 0ˢ = no (λ ())
_≟ᵍ_ 0ˢ + = no (λ ())
_≟ᵍ_ 0ˢ - = no (λ ())
_≟ᵍ_ 0ˢ 0ˢ = yes refl
module _ (prog : Program) where
open Program prog
-- embelish 'sign' with a top and bottom element.
open import Lattice.AboveBelow Sign _≡_ (record { ≈-refl = refl; ≈-sym = sym; ≈-trans = trans }) _≟ᵍ_ as AB renaming (AboveBelow to SignLattice; ≈-dec to ≈ᵍ-dec)
-- 'sign' has no underlying lattice structure, so use the 'plain' above-below lattice.
open AB.Plain using () renaming (finiteHeightLattice to finiteHeightLatticeᵍ-if-inhabited)
finiteHeightLatticeᵍ = finiteHeightLatticeᵍ-if-inhabited 0ˢ
-- The variable -> sign map is a finite value-map with keys strings. Use a bundle to avoid explicitly specifying operators.
open import Lattice.Bundles.FiniteValueMap String SignLattice _≟ˢ_ renaming (finiteHeightLattice to finiteHeightLatticeᵛ-if-B-finite; FiniteHeightType to FiniteHeightTypeᵛ; _≈_ to _≈ᵛ_; ≈-dec to ≈ᵛ-dec-if-≈ᵍ-dec)
VariableSigns = FiniteHeightTypeᵛ finiteHeightLatticeᵍ vars-Unique ≈ᵍ-dec
finiteHeightLatticeᵛ = finiteHeightLatticeᵛ-if-B-finite finiteHeightLatticeᵍ vars-Unique ≈ᵍ-dec
≈ᵛ-dec = ≈ᵛ-dec-if-≈ᵍ-dec finiteHeightLatticeᵍ vars-Unique ≈ᵍ-dec
-- Finally, the map we care about is (state -> (variables -> sign)). Bring that in.
open import Lattice.Bundles.FiniteValueMap State VariableSigns _≟_ renaming (finiteHeightLattice to finiteHeightLatticeᵐ-if-B-finite; FiniteHeightType to FiniteHeightTypeᵐ)
StateVariables = FiniteHeightTypeᵐ finiteHeightLatticeᵛ states-Unique ≈ᵛ-dec
finiteHeightLatticeᵐ = finiteHeightLatticeᵐ-if-B-finite finiteHeightLatticeᵛ states-Unique ≈ᵛ-dec

View File

@ -1,149 +0,0 @@
open import Equivalence
module Homomorphism {a b} (A : Set a) (B : Set b)
(_≈₁_ : A A Set a) (_≈₂_ : B B Set b)
(≈₂-equiv : IsEquivalence B _≈₂_)
(f : A B) where
open import Agda.Primitive using (lsuc; Level) renaming (_⊔_ to _⊔_)
open import Function.Definitions using (Surjective)
open import Relation.Binary.Core using (_Preserves_⟶_ )
open import Data.Product using (_,_)
open import Lattice
open IsEquivalence ≈₂-equiv using () renaming (≈-trans to ≈₂-trans; ≈-sym to ≈₂-sym; ≈-refl to ≈₂-refl)
open import Relation.Binary.Reasoning.Base.Single _≈₂_ ≈₂-refl ≈₂-trans
infixl 20 _∙₂_
_∙₂_ = ≈₂-trans
record SemilatticeHomomorphism (_⊔₁_ : A A A)
(_⊔₂_ : B B B) : Set (a ⊔ℓ b) where
field
f-preserves-≈ : f Preserves _≈₁_ _≈₂_
f-⊔-distr : (a₁ a₂ : A) f (a₁ ⊔₁ a₂) ≈₂ ((f a₁) ⊔₂ (f a₂))
module _ (_⊔₁_ : A A A) (_⊔₂_ : B B B)
(sh : SemilatticeHomomorphism _⊔₁_ _⊔₂_)
(≈₂-⊔₂-cong : {a₁ a₂ a₃ a₄} a₁ ≈₂ a₂ a₃ ≈₂ a₄ (a₁ ⊔₂ a₃) ≈₂ (a₂ ⊔₂ a₄))
(surF : Surjective _≈₁_ _≈₂_ f) where
open SemilatticeHomomorphism sh
transportSemilattice : IsSemilattice A _≈₁_ _⊔₁_ IsSemilattice B _≈₂_ _⊔₂_
transportSemilattice sA = record
{ ≈-equiv = ≈₂-equiv
; ≈-⊔-cong = ≈₂-⊔₂-cong
; ⊔-assoc = λ b₁ b₂ b₃
let (a₁ , fa₁≈b₁) = surF b₁
(a₂ , fa₂≈b₂) = surF b₂
(a₃ , fa₃≈b₃) = surF b₃
in
begin
(b₁ ⊔₂ b₂) ⊔₂ b₃
∼⟨ ≈₂-⊔₂-cong (≈₂-⊔₂-cong (≈₂-sym fa₁≈b₁) (≈₂-sym fa₂≈b₂)) (≈₂-sym fa₃≈b₃)
(f a₁ ⊔₂ f a₂) ⊔₂ f a₃
∼⟨ ≈₂-⊔₂-cong (≈₂-sym (f-⊔-distr a₁ a₂)) ≈₂-refl
f (a₁ ⊔₁ a₂) ⊔₂ f a₃
∼⟨ ≈₂-sym (f-⊔-distr (a₁ ⊔₁ a₂) a₃)
f ((a₁ ⊔₁ a₂) ⊔₁ a₃)
∼⟨ f-preserves-≈ (IsSemilattice.⊔-assoc sA a₁ a₂ a₃)
f (a₁ ⊔₁ (a₂ ⊔₁ a₃))
∼⟨ f-⊔-distr a₁ (a₂ ⊔₁ a₃)
f a₁ ⊔₂ f (a₂ ⊔₁ a₃)
∼⟨ ≈₂-⊔₂-cong ≈₂-refl (f-⊔-distr a₂ a₃)
f a₁ ⊔₂ (f a₂ ⊔₂ f a₃)
∼⟨ ≈₂-⊔₂-cong fa₁≈b₁ (≈₂-⊔₂-cong fa₂≈b₂ fa₃≈b₃)
b₁ ⊔₂ (b₂ ⊔₂ b₃)
; ⊔-comm = λ b₁ b₂
let (a₁ , fa₁≈b₁) = surF b₁
(a₂ , fa₂≈b₂) = surF b₂
in
begin
b₁ ⊔₂ b₂
∼⟨ ≈₂-⊔₂-cong (≈₂-sym fa₁≈b₁) (≈₂-sym fa₂≈b₂)
f a₁ ⊔₂ f a₂
∼⟨ ≈₂-sym (f-⊔-distr a₁ a₂)
f (a₁ ⊔₁ a₂)
∼⟨ f-preserves-≈ (IsSemilattice.⊔-comm sA a₁ a₂)
f (a₂ ⊔₁ a₁)
∼⟨ f-⊔-distr a₂ a₁
f a₂ ⊔₂ f a₁
∼⟨ ≈₂-⊔₂-cong fa₂≈b₂ fa₁≈b₁
b₂ ⊔₂ b₁
; ⊔-idemp = λ b
let (a , fa≈b) = surF b
in
begin
b ⊔₂ b
∼⟨ ≈₂-⊔₂-cong (≈₂-sym fa≈b) (≈₂-sym fa≈b)
f a ⊔₂ f a
∼⟨ ≈₂-sym (f-⊔-distr a a)
f (a ⊔₁ a)
∼⟨ f-preserves-≈ (IsSemilattice.⊔-idemp sA a)
f a
∼⟨ fa≈b
b
}
record LatticeHomomorphism (_⊔₁_ : A A A) (_⊔₂_ : B B B)
(_⊓₁_ : A A A) (_⊓₂_ : B B B) : Set (a ⊔ℓ b) where
field
⊔-homomorphism : SemilatticeHomomorphism _⊔₁_ _⊔₂_
⊓-homomorphism : SemilatticeHomomorphism _⊓₁_ _⊓₂_
open SemilatticeHomomorphism ⊔-homomorphism using (f-⊔-distr; f-preserves-≈) public
open SemilatticeHomomorphism ⊓-homomorphism using () renaming (f-⊔-distr to f-⊓-distr) public
module _ (_⊔₁_ : A A A) (_⊔₂_ : B B B)
(_⊓₁_ : A A A) (_⊓₂_ : B B B)
(lh : LatticeHomomorphism _⊔₁_ _⊔₂_ _⊓₁_ _⊓₂_)
(≈₂-⊔₂-cong : {a₁ a₂ a₃ a₄} a₁ ≈₂ a₂ a₃ ≈₂ a₄ (a₁ ⊔₂ a₃) ≈₂ (a₂ ⊔₂ a₄))
(≈₂-⊓₂-cong : {a₁ a₂ a₃ a₄} a₁ ≈₂ a₂ a₃ ≈₂ a₄ (a₁ ⊓₂ a₃) ≈₂ (a₂ ⊓₂ a₄))
(surF : Surjective _≈₁_ _≈₂_ f) where
open LatticeHomomorphism lh
transportLattice : IsLattice A _≈₁_ _⊔₁_ _⊓₁_ IsLattice B _≈₂_ _⊔₂_ _⊓₂_
transportLattice lA = record
{ joinSemilattice = transportSemilattice _⊔₁_ _⊔₂_ (LatticeHomomorphism.⊔-homomorphism lh) ≈₂-⊔₂-cong surF (IsLattice.joinSemilattice lA)
; meetSemilattice = transportSemilattice _⊓₁_ _⊓₂_ (LatticeHomomorphism.⊓-homomorphism lh) ≈₂-⊓₂-cong surF (IsLattice.meetSemilattice lA)
; absorb-⊔-⊓ = λ b₁ b₂
let (a₁ , fa₁≈b₁) = surF b₁
(a₂ , fa₂≈b₂) = surF b₂
in
begin
b₁ ⊔₂ (b₁ ⊓₂ b₂)
∼⟨ ≈₂-⊔₂-cong (≈₂-sym fa₁≈b₁) (≈₂-⊓₂-cong (≈₂-sym fa₁≈b₁) (≈₂-sym fa₂≈b₂))
f a₁ ⊔₂ (f a₁ ⊓₂ f a₂)
∼⟨ ≈₂-⊔₂-cong ≈₂-refl (≈₂-sym (f-⊓-distr a₁ a₂))
f a₁ ⊔₂ f (a₁ ⊓₁ a₂)
∼⟨ ≈₂-sym (f-⊔-distr a₁ (a₁ ⊓₁ a₂))
f (a₁ ⊔₁ (a₁ ⊓₁ a₂))
∼⟨ f-preserves-≈ (IsLattice.absorb-⊔-⊓ lA a₁ a₂)
f a₁
∼⟨ fa₁≈b₁
b₁
; absorb-⊓-⊔ = λ b₁ b₂
let (a₁ , fa₁≈b₁) = surF b₁
(a₂ , fa₂≈b₂) = surF b₂
in
begin
b₁ ⊓₂ (b₁ ⊔₂ b₂)
∼⟨ ≈₂-⊓₂-cong (≈₂-sym fa₁≈b₁) (≈₂-⊔₂-cong (≈₂-sym fa₁≈b₁) (≈₂-sym fa₂≈b₂))
f a₁ ⊓₂ (f a₁ ⊔₂ f a₂)
∼⟨ ≈₂-⊓₂-cong ≈₂-refl (≈₂-sym (f-⊔-distr a₁ a₂))
f a₁ ⊓₂ f (a₁ ⊔₁ a₂)
∼⟨ ≈₂-sym (f-⊓-distr a₁ (a₁ ⊔₁ a₂))
f (a₁ ⊓₁ (a₁ ⊔₁ a₂))
∼⟨ f-preserves-≈ (IsLattice.absorb-⊓-⊔ lA a₁ a₂)
f a₁
∼⟨ fa₁≈b₁
b₁
}

View File

@ -1,10 +1,93 @@
module Language where
open import Data.String using (String)
open import Data.Nat using ()
open import Data.Nat using (; suc; pred)
open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
open import Data.Product using (Σ; _,_; proj₁; proj₂)
open import Data.Vec using (Vec; foldr)
open import Data.List using ([]; _∷_; List) renaming (foldr to foldrˡ; map to mapˡ)
open import Data.List.Relation.Unary.All using (All; []; _∷_)
open import Data.Fin using (Fin; suc; zero; from; inject₁) renaming (_≟_ to _≟ᶠ_)
open import Data.Fin.Properties using (suc-injective)
open import Relation.Binary.PropositionalEquality using (cong; _≡_)
open import Relation.Nullary using (¬_)
open import Function using (_∘_)
open import Lattice
open import Utils using (Unique; Unique-map; empty; push)
data Expr : Set where
_+_ : Expr Expr Expr
_-_ : Expr Expr Expr
`_ : String Expr
#_ : Expr
data Stmt : Set where
_←_ : String Expr Stmt
open import Lattice.MapSet String _≟ˢ_
renaming
( MapSet to StringSet
; insert to insertˢ
; to-List to to-Listˢ
; empty to emptyˢ
; _⊔_ to _⊔ˢ_
)
private
Expr-vars : Expr StringSet
Expr-vars (l + r) = Expr-vars l ⊔ˢ Expr-vars r
Expr-vars (l - r) = Expr-vars l ⊔ˢ Expr-vars r
Expr-vars (` s) = insertˢ s emptyˢ
Expr-vars (# _) = emptyˢ
Stmt-vars : Stmt StringSet
Stmt-vars (x e) = insertˢ x (Expr-vars e)
-- Creating a new number from a natural number can never create one
-- equal to one you get from weakening the bounds on another number.
z≢sf : {n : } (f : Fin n) ¬ (zero suc f)
z≢sf f ()
z≢mapsfs : {n : } (fs : List (Fin n)) All (λ sf ¬ zero sf) (mapˡ suc fs)
z≢mapsfs [] = []
z≢mapsfs (f fs') = z≢sf f z≢mapsfs fs'
indices : (n : ) Σ (List (Fin n)) Unique
indices 0 = ([] , empty)
indices (suc n') =
let
(inds' , unids') = indices n'
in
( zero mapˡ suc inds'
, push (z≢mapsfs inds') (Unique-map suc suc-injective unids')
)
-- For now, just represent the program and CFG as one type, without branching.
record Program : Set where
field
length :
stmts : Vec Stmt length
private
vars-Set : StringSet
vars-Set = foldr (λ n StringSet)
(λ {k} stmt acc (Stmt-vars stmt) ⊔ˢ acc) emptyˢ stmts
vars : List String
vars = to-Listˢ vars-Set
vars-Unique : Unique vars
vars-Unique = proj₂ vars-Set
State : Set
State = Fin length
states : List State
states = proj₁ (indices length)
states-Unique : Unique states
states-Unique = proj₂ (indices length)
_≟_ : IsDecidable (_≡_ {_} {State})
_≟_ = _≟ᶠ_

View File

@ -19,8 +19,10 @@ module _ (fhB : FiniteHeightLattice B) where
module _ {ks : List A} (uks : Unique ks) (≈₂-dec : Decidable _≈₂_) where
import Lattice.FiniteValueMap A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A isLattice₂ as FVM
FiniteHeightType = FVM.FiniteMap
FiniteHeightType = FVM.FiniteMap ks
finiteHeightLattice = FVM.IterProdIsomorphism.finiteHeightLattice uks ≈₂-dec height₂ fixedHeight₂
open FiniteHeightLattice finiteHeightLattice public
≈-dec = FVM.≈-dec ks ≈₂-dec
finiteHeightLattice = FVM.IterProdIsomorphism.finiteHeightLattice uks ≈₂-dec height₂ fixedHeight₂

View File

@ -2,7 +2,7 @@ open import Lattice
open import Relation.Binary.PropositionalEquality as Eq
using (_≡_;refl; sym; trans; cong; subst)
open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔_)
open import Data.List using (List)
open import Data.List using (List; _∷_; [])
module Lattice.FiniteMap {a b : Level} (A : Set a) (B : Set b)
(_≈₂_ : B B Set b)
@ -10,8 +10,9 @@ module Lattice.FiniteMap {a b : Level} (A : Set a) (B : Set b)
(≡-dec-A : IsDecidable (_≡_ {a} {A}))
(lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
open IsLattice lB using () renaming (_≼_ to _≼₂_)
open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB as Map
using (Map; ⊔-equal-keys; ⊓-equal-keys)
using (Map; ⊔-equal-keys; ⊓-equal-keys; ∈k-dec; m₁≼m₂⇒m₁[k]≼m₂[k])
renaming
( _≈_ to _≈ᵐ_
; _⊔_ to _⊔ᵐ_
@ -28,9 +29,21 @@ open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB as Map
; absorb-⊔-⊓ to absorb-⊔ᵐ-⊓ᵐ
; absorb-⊓-⊔ to absorb-⊓ᵐ-⊔ᵐ
; ≈-dec to ≈ᵐ-dec
; _[_] to _[_]ᵐ
; locate to locateᵐ
; keys to keysᵐ
; _updating_via_ to _updatingᵐ_via_
; updating-via-keys-≡ to updatingᵐ-via-keys-≡
; f'-Monotonic to f'-Monotonicᵐ
; _≼_ to _≼ᵐ_
)
open import Data.List.Membership.Propositional using () renaming (_∈_ to _∈ˡ_)
open import Data.Product using (_×_; _,_; Σ; proj₁ ; proj₂)
open import Equivalence
open import Function using (_∘_)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Utils using (Pairwise; _∷_; [])
open import Data.Empty using (⊥-elim)
module _ (ks : List A) where
FiniteMap : Set (a ⊔ℓ b)
@ -56,6 +69,18 @@ module _ (ks : List A) where
km₁≡ks
)
_∈k_ : A FiniteMap Set a
_∈k_ k (m₁ , _) = k ∈ˡ (keysᵐ m₁)
_updating_via_ : FiniteMap List A (A B) FiniteMap
_updating_via_ (m₁ , ksm₁≡ks) ks f =
( m₁ updatingᵐ ks via f
, trans (sym (updatingᵐ-via-keys-≡ m₁ ks f)) ksm₁≡ks
)
_[_] : FiniteMap List A List B
_[_] (m₁ , _) ks = m₁ [ ks ]ᵐ
≈-equiv : IsEquivalence FiniteMap _≈_
≈-equiv = record
{ ≈-refl =
@ -97,6 +122,8 @@ module _ (ks : List A) where
; absorb-⊓-⊔ = λ (m₁ , _) (m₂ , _) absorb-⊓ᵐ-⊔ᵐ m₁ m₂
}
open IsLattice isLattice using (_≼_) public
lattice : Lattice FiniteMap
lattice = record
{ _≈_ = _≈_
@ -104,3 +131,46 @@ module _ (ks : List A) where
; _⊓_ = _⊓_
; isLattice = isLattice
}
module _ {l} {L : Set l}
{_≈ˡ_ : L L Set l} {_⊔ˡ_ : L L L} {_⊓ˡ_ : L L L}
(lL : IsLattice L _≈ˡ_ _⊔ˡ_ _⊓ˡ_) where
open IsLattice lL using () renaming (_≼_ to _≼ˡ_)
module _ (f : L FiniteMap) (f-Monotonic : Monotonic _≼ˡ_ _≼_ f)
(g : A L B) (g-Monotonicʳ : k Monotonic _≼ˡ_ _≼₂_ (g k))
(ks : List A) where
updater : L A B
updater l k = g k l
f' : L FiniteMap
f' l = (f l) updating ks via (updater l)
f'-Monotonic : Monotonic _≼ˡ_ _≼_ f'
f'-Monotonic {l₁} {l₂} l₁≼l₂ = f'-Monotonicᵐ lL (proj₁ f) f-Monotonic g g-Monotonicʳ ks l₁≼l₂
all-equal-keys : (fm₁ fm₂ : FiniteMap) (Map.keys (proj₁ fm₁) Map.keys (proj₁ fm₂))
all-equal-keys (fm₁ , km₁≡ks) (fm₂ , km₂≡ks) = trans km₁≡ks (sym km₂≡ks)
∈k-exclusive : (fm₁ fm₂ : FiniteMap) {k : A} ¬ ((k ∈k fm₁) × (¬ k ∈k fm₂))
∈k-exclusive fm₁ fm₂ {k} (k∈kfm₁ , k∉kfm₂) =
let
k∈kfm₂ = subst (λ l k ∈ˡ l) (all-equal-keys fm₁ fm₂) k∈kfm₁
in
k∉kfm₂ k∈kfm₂
m₁≼m₂⇒m₁[ks]≼m₂[ks] : (fm₁ fm₂ : FiniteMap) (ks' : List A)
fm₁ fm₂ Pairwise _≼₂_ (fm₁ [ ks' ]) (fm₂ [ ks' ])
m₁≼m₂⇒m₁[ks]≼m₂[ks] _ _ [] _ = []
m₁≼m₂⇒m₁[ks]≼m₂[ks] fm₁@(m₁ , km₁≡ks) fm₂@(m₂ , km₂≡ks) (k ks'') m₁≼m₂
with ∈k-dec k (proj₁ m₁) | ∈k-dec k (proj₁ m₂)
... | yes k∈km₁ | yes k∈km₂ =
let
(v₁ , k,v₁∈m₁) = locateᵐ {m = m₁} k∈km₁
(v₂ , k,v₂∈m₂) = locateᵐ {m = m₂} k∈km₂
in
(m₁≼m₂⇒m₁[k]≼m₂[k] m₁ m₂ m₁≼m₂ k,v₁∈m₁ k,v₂∈m₂) m₁≼m₂⇒m₁[ks]≼m₂[ks] fm₁ fm₂ ks'' m₁≼m₂
... | no k∉km₁ | no k∉km₂ = m₁≼m₂⇒m₁[ks]≼m₂[ks] fm₁ fm₂ ks'' m₁≼m₂
... | yes k∈km₁ | no k∉km₂ = ⊥-elim (∈k-exclusive fm₁ fm₂ (k∈km₁ , k∉km₂))
... | no k∉km₁ | yes k∈km₂ = ⊥-elim (∈k-exclusive fm₂ fm₁ (k∈km₂ , k∉km₁))

View File

@ -19,7 +19,7 @@ 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 import Utils using (Unique; push; Unique-append; All¬-¬Any; All-x∈xs)
open IsLattice lB using () renaming
( ≈-refl to ≈₂-refl; ≈-sym to ≈₂-sym; ≈-trans to ≈₂-trans
@ -34,6 +34,21 @@ private module ImplKeys where
keys : List (A × B) List A
keys = map proj₁
-- See note on `forget` for why this is defined in global scope even though
-- it operates on lists.
∈k-dec : (k : A) (l : List (A × B)) Dec (k ∈ˡ (ImplKeys.keys l))
∈k-dec k [] = no (λ ())
∈k-dec k ((k' , v) xs)
with (≡-dec-A k k')
... | yes k≡k' = yes (here k≡k')
... | no k≢k' with (∈k-dec k xs)
... | yes k∈kxs = yes (there k∈kxs)
... | no k∉kxs = no witness
where
witness : ¬ k ∈ˡ (ImplKeys.keys ((k' , v) xs))
witness (here k≡k') = k≢k' k≡k'
witness (there k∈kxs) = k∉kxs k∈kxs
private module _ where
open MemProp using (_∈_)
open ImplKeys
@ -65,19 +80,6 @@ private module _ where
... | yes k∈xs = yes (there k∈xs)
... | no k∉xs = no (λ { (here k≡x) k≢x k≡x; (there k∈xs) k∉xs k∈xs })
∈k-dec : (k : A) (l : List (A × B)) Dec (k keys l)
∈k-dec k [] = no (λ ())
∈k-dec k ((k' , v) xs)
with (≡-dec-A k k')
... | yes k≡k' = yes (here k≡k')
... | no k≢k' with (∈k-dec k xs)
... | yes k∈kxs = yes (there k∈kxs)
... | no k∉kxs = no witness
where
witness : ¬ k keys ((k' , v) xs)
witness (here k≡k') = k≢k' k≡k'
witness (there k∈kxs) = k∉kxs k∈kxs
∈-cong : {c d} {C : Set c} {D : Set d} {c : C} {l : List C}
(f : C D) c l f c map f l
∈-cong f (here c≡c') = here (cong f c≡c')
@ -340,7 +342,7 @@ private module ImplInsert (f : B → B → B) where
restrict-preserves-Unique : {l₁ l₂ : List (A × B)}
Unique (keys l₂) Unique (keys (restrict l₁ l₂))
restrict-preserves-Unique {l₁} {[]} _ = empty
restrict-preserves-Unique {l₁} {[]} _ = Utils.empty
restrict-preserves-Unique {l₁} {(k , v) xs} (push k≢xs uxs)
with ∈k-dec k l₁
... | yes _ = push (restrict-preserves-k≢ k≢xs) (restrict-preserves-Unique uxs)
@ -476,6 +478,9 @@ private module ImplInsert (f : B → B → B) where
Map : Set (a ⊔ℓ b)
Map = Σ (List (A × B)) (λ l Unique (ImplKeys.keys l))
empty : Map
empty = ([] , Utils.empty)
keys : Map List A
keys (kvs , _) = ImplKeys.keys kvs
@ -488,8 +493,9 @@ _∈k_ k m = MemProp._∈_ k (keys m)
locate : {k : A} {m : Map} k ∈k m Σ B (λ v (k , v) m)
locate k∈km = locate-impl k∈km
-- defined this way because ∈ for maps uses projection, so the full map can't be guessed.
-- On the other hand, list can be guessed.
-- `forget` and `∈k-dec` are defined this way because ∈ for maps uses
-- projection, so the full map can't be guessed. On the other hand, list can
-- be guessed.
forget : {k : A} {v : B} {l : List (A × B)} (k , v) ∈ˡ l k ∈ˡ (ImplKeys.keys l)
forget = ∈-cong proj₁
@ -529,9 +535,12 @@ 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 (union-preserves-Unique; union-equal-keys; insert-preserves-Unique) renaming (insert to insert-impl; union to union-impl)
open ImplInsert _⊓₂_ using (intersect-preserves-Unique; intersect-equal-keys) renaming (intersect to intersect-impl)
insert : A B Map Map
insert k v (l , uks) = (insert-impl k v l , insert-preserves-Unique uks)
_⊔_ : Map Map Map
_⊔_ (kvs₁ , _) (kvs₂ , uks₂) = (union-impl kvs₁ kvs₂ , union-preserves-Unique kvs₁ kvs₂ uks₂)
@ -878,6 +887,8 @@ isLattice = record
; absorb-⊓-⊔ = absorb-⊓-⊔
}
open IsLattice isLattice using (_≼_) public
lattice : Lattice Map
lattice = record
{ _≈_ = _≈_
@ -958,6 +969,10 @@ _updating_via_ (kvs , uks) ks f =
, subst Unique (transform-keys-≡ kvs ks f) uks
)
updating-via-keys-≡ : (m : Map) (ks : List A) (f : A B)
keys m keys (m updating ks via f)
updating-via-keys-≡ (l , _) = transform-keys-≡ l
updating-via-∉k-forward : (m : Map) (ks : List A) (f : A B) {k : A}
¬ k ∈k m ¬ k ∈k (m updating ks via f)
updating-via-∉k-forward m = transform-∉k-forward
@ -995,7 +1010,6 @@ updating-via-k∉ks-backward m = transform-k∉ks-backward
module _ {l} {L : Set l}
{_≈ˡ_ : L L Set l} {_⊔ˡ_ : L L L} {_⊓ˡ_ : L L L}
(lL : IsLattice L _≈ˡ_ _⊔ˡ_ _⊓ˡ_) where
open IsLattice isLattice using (_≼_)
open IsLattice lL using () renaming (_≼_ to _≼ˡ_)
module _ (f : L Map) (f-Monotonic : Monotonic _≼ˡ_ _≼_ f)
@ -1072,3 +1086,29 @@ module _ {l} {L : Set l}
with refl Map-functional {m = f' l₂} k,v∈f'l₂ k,v₂∈f'l₂
with refl Map-functional {m = f l₂} k,v'∈fl₂ k,v₂∈fl₂ =
(v₁ ⊔₂ v , (v'≈v'' , k,v₁v₂∈f'l₁f'l₂))
_[_] : Map List A List B
_[_] m [] = []
_[_] m (k ks)
with ∈k-dec k (proj₁ m)
... | yes k∈km = proj₁ (locate {m = m} k∈km) (m [ ks ])
... | no _ = m [ ks ]
m₁≼m₂⇒m₁[k]≼m₂[k] : (m₁ m₂ : Map) {k : A} {v₁ v₂ : B}
m₁ m₂ (k , v₁) m₁ (k , v₂) m₂ v₁ ≼₂ v₂
m₁≼m₂⇒m₁[k]≼m₂[k] m₁ m₂ m₁≼m₂ k,v₁∈m₁ k,v₂∈m₂
with k,v₁v₂∈m₁m₂ ⊔-combines {m₁ = m₁} {m₂ = m₂} k,v₁∈m₁ k,v₂∈m₂
with (v' , (v₁v₂≈v' , k,v'∈m₂)) (proj₁ m₁≼m₂) _ _ k,v₁v₂∈m₁m₂
with refl Map-functional {m = m₂} k,v₂∈m₂ k,v'∈m₂
= v₁v₂≈v'
m₁≼m₂⇒k∈km₁⇒k∈km₂ : (m₁ m₂ : Map) {k : A}
m₁ m₂ k ∈k m₁ k ∈k m₂
m₁≼m₂⇒k∈km₁⇒k∈km₂ m₁ m₂ m₁≼m₂ k∈km₁ =
let
k∈km₁m₂ = union-preserves-∈k₁ {l₁ = proj₁ m₁} {l₂ = proj₁ m₂} k∈km₁
(v , k,v∈m₁m₂) = locate {m = m₁ m₂} k∈km₁m₂
(v' , (v≈v' , k,v'∈m₂)) = (proj₁ m₁≼m₂) _ _ k,v∈m₁m₂
in
forget k,v'∈m₂

View File

@ -5,15 +5,25 @@ open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔_)
module Lattice.MapSet {a : Level} (A : Set a) (≡-dec-A : Decidable (_≡_ {a} {A})) where
open import Lattice.Unit using () renaming (_≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_; isLattice to -isLattice)
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 A _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A -isLattice
open UnitMap using (Map)
open UnitMap using
( _⊆_; _≈_; ≈-equiv; _⊔_; _⊓_
( _⊆_; _≈_; ≈-equiv; _⊔_; _⊓_; empty
; isUnionSemilattice; isIntersectSemilattice; isLattice; lattice
) 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

View File

@ -22,7 +22,7 @@ xyzw-Unique = push ((λ ()) ∷ (λ ()) ∷ (λ ()) ∷ []) (push ((λ ()) ∷ (
open import Lattice using (IsFiniteHeightLattice; FiniteHeightLattice; Monotonic)
open import Lattice.AboveBelow _≡_ (record { ≈-refl = refl; ≈-sym = sym; ≈-trans = trans }) _≟ᵘ_ as AB using () renaming (≈-dec to ≈ᵘ-dec)
open AB.Plain using () renaming (finiteHeightLattice to finiteHeightLatticeᵘ)
open import Lattice.Bundles.FiniteValueMap String AB.AboveBelow _≟ˢ_ renaming (finiteHeightLattice to finiteHeightLatticeᵐ; FiniteHeightType to FiniteHeightTypeᵐ; ≈-dec to ≈-dec)
open import Lattice.Bundles.FiniteValueMap String AB.AboveBelow _≟ˢ_ using () renaming (finiteHeightLattice to finiteHeightLatticeᵐ; FiniteHeightType to FiniteHeightTypeᵐ; ≈-dec to ≈-dec)
fhlᵘ = finiteHeightLatticeᵘ (Data.Unit.tt)
@ -33,7 +33,7 @@ showAboveBelow AB. = ""
showAboveBelow AB.⊥ = ""
showAboveBelow (AB.[_] tt) = "()"
showMap : {ks : List String} FiniteHeightMap ks String
showMap : FiniteHeightMap String
showMap ((kvs , _) , _) = "{" ++ foldr (λ (x , y) rest x ++ "" ++ showAboveBelow y ++ ", " ++ rest) "" kvs ++ "}"
fhlⁱᵖ = finiteHeightLatticeᵐ fhlᵘ xyzw-Unique ≈ᵘ-dec
@ -44,16 +44,16 @@ open import Relation.Binary.Reasoning.Base.Single _≈_ (λ {m} → ≈-refl {m}
smallestMap = proj₁ (proj₁ (proj₁ (FiniteHeightLattice.fixedHeight fhlⁱᵖ)))
largestMap = proj₂ (proj₁ (proj₁ (FiniteHeightLattice.fixedHeight fhlⁱᵖ)))
dumb : FiniteHeightMap xyzw
dumb : FiniteHeightMap
dumb = ((("x" , AB.[_] tt) ("y" , AB.⊥) ("z" , AB.⊥) ("w" , AB.⊥) [] , xyzw-Unique) , refl)
dumbFunction : FiniteHeightMap xyzw FiniteHeightMap xyzw
dumbFunction : FiniteHeightMap FiniteHeightMap
dumbFunction = _⊔_ dumb
dumbFunction-Monotonic : Monotonic _≼_ _≼_ dumbFunction
dumbFunction-Monotonic {m₁} {m₂} m₁≼m₂ = ⊔-Monotonicˡ dumb {m₁} {m₂} m₁≼m₂
open import Fixedpoint {0} {FiniteHeightMap xyzw} {8} {_≈_} {_⊔_} {_⊓_} (≈-dec fhlᵘ xyzw-Unique ≈ᵘ-dec) (FiniteHeightLattice.isFiniteHeightLattice fhlⁱᵖ) dumbFunction (λ {m₁} {m₂} m₁≼m₂ dumbFunction-Monotonic {m₁} {m₂} m₁≼m₂)
open import Fixedpoint {0} {FiniteHeightMap} {8} {_≈_} {_⊔_} {_⊓_} (≈-dec fhlᵘ xyzw-Unique ≈ᵘ-dec) (FiniteHeightLattice.isFiniteHeightLattice fhlⁱᵖ) dumbFunction (λ {m₁} {m₂} m₁≼m₂ dumbFunction-Monotonic {m₁} {m₂} m₁≼m₂)
main = run {0} (putStrLn (showMap aᶠ))

View File

@ -2,10 +2,11 @@ module Utils where
open import Agda.Primitive using () renaming (_⊔_ to _⊔_)
open import Data.Nat using (; suc)
open import Data.List using (List; []; _∷_; _++_)
open import Data.List using (List; []; _∷_; _++_) renaming (map to mapˡ)
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 Function.Definitions using (Injective)
open import Relation.Binary.PropositionalEquality using (_≡_; sym; refl)
open import Relation.Nullary using (¬_)
@ -29,6 +30,18 @@ Unique-append {c} {C} {x} {x' ∷ xs'} x∉xs (push x'≢ uxs') =
help {[]} _ = x'≢x []
help {e es} (x'≢e x'≢es) = x'≢e help x'≢es
All-≢-map : {c d} {C : Set c} {D : Set d} (x : C) {xs : List C} (f : C D)
Injective (_≡_ {_} {C}) (_≡_ {_} {D}) f
All (λ x' ¬ x x') xs All (λ y' ¬ (f x) y') (mapˡ f xs)
All-≢-map x f f-Injecitve [] = []
All-≢-map x {x' xs'} f f-Injecitve (x≢x' x≢xs') = (λ fx≡fx' x≢x' (f-Injecitve fx≡fx')) All-≢-map x f f-Injecitve x≢xs'
Unique-map : {c d} {C : Set c} {D : Set d} {l : List C} (f : C D)
Injective (_≡_ {_} {C}) (_≡_ {_} {D}) f
Unique l Unique (mapˡ f l)
Unique-map {l = []} _ _ _ = empty
Unique-map {l = x xs} f f-Injecitve (push x≢xs uxs) = push (All-≢-map x f f-Injecitve x≢xs) (Unique-map f f-Injecitve uxs)
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