diff --git a/Analysis/Forward.agda b/Analysis/Forward.agda index fd04f0f..a7dfd7c 100644 --- a/Analysis/Forward.agda +++ b/Analysis/Forward.agda @@ -43,7 +43,7 @@ module WithProg (prog : Program) where (flip (eval s)) (eval-Monoʳ s) vs₁≼vs₂ - open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) updateVariablesForState updateVariablesForState-Monoʳ states + open StateVariablesFiniteMap.GeneralizedUpdate isLatticeᵐ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) updateVariablesForState updateVariablesForState-Monoʳ states using () renaming ( f' to updateAll diff --git a/Analysis/Forward/Adapters.agda b/Analysis/Forward/Adapters.agda index 01b6ba7..c1a9e60 100644 --- a/Analysis/Forward/Adapters.agda +++ b/Analysis/Forward/Adapters.agda @@ -41,7 +41,7 @@ module ExprToStmtAdapter {{ exprEvaluator : ExprEvaluator }} where -- for an assignment, and update the corresponding key. Use Exercise 4.26's -- generalized update to set the single key's value. private module _ (k : String) (e : Expr) where - open VariableValuesFiniteMap.GeneralizedUpdate vars isLatticeᵛ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) (λ _ → evalᵉ e) (λ _ {vs₁} {vs₂} vs₁≼vs₂ → evalᵉ-Monoʳ e {vs₁} {vs₂} vs₁≼vs₂) (k ∷ []) + open VariableValuesFiniteMap.GeneralizedUpdate isLatticeᵛ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) (λ _ → evalᵉ e) (λ _ {vs₁} {vs₂} vs₁≼vs₂ → evalᵉ-Monoʳ e {vs₁} {vs₂} vs₁≼vs₂) (k ∷ []) using () renaming ( f' to updateVariablesFromExpression diff --git a/Analysis/Forward/Lattices.agda b/Analysis/Forward/Lattices.agda index 7becec0..ae3766d 100644 --- a/Analysis/Forward/Lattices.agda +++ b/Analysis/Forward/Lattices.agda @@ -26,14 +26,14 @@ open IsFiniteHeightLattice isFiniteHeightLatticeˡ ) open Program prog -import Lattice.FiniteValueMap +import Lattice.FiniteMap import Chain -- The variable -> abstract value (e.g. sign) map is a finite value-map -- with keys strings. Use a bundle to avoid explicitly specifying operators. -- It's helpful to export these via 'public' since consumers tend to -- use various variable lattice operations. -module VariableValuesFiniteMap = Lattice.FiniteValueMap.WithKeys _≟ˢ_ isLatticeˡ vars +module VariableValuesFiniteMap = Lattice.FiniteMap.WithKeys _≟ˢ_ isLatticeˡ vars open VariableValuesFiniteMap using () renaming @@ -60,13 +60,13 @@ open IsLattice isLatticeᵛ ; ⊔-idemp to ⊔ᵛ-idemp ) public -open Lattice.FiniteValueMap.IterProdIsomorphism _≟ˢ_ isLatticeˡ +open Lattice.FiniteMap.IterProdIsomorphism _≟ˢ_ isLatticeˡ using () renaming ( Provenance-union to Provenance-unionᵐ ) public -open Lattice.FiniteValueMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight _≟ˢ_ isLatticeˡ vars-Unique ≈ˡ-dec _ fixedHeightˡ +open Lattice.FiniteMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight _≟ˢ_ isLatticeˡ vars-Unique ≈ˡ-dec _ fixedHeightˡ using () renaming ( isFiniteHeightLattice to isFiniteHeightLatticeᵛ @@ -80,7 +80,7 @@ fixedHeightᵛ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵛ ⊥ᵛ = Chain.Height.⊥ fixedHeightᵛ -- Finally, the map we care about is (state -> (variables -> value)). Bring that in. -module StateVariablesFiniteMap = Lattice.FiniteValueMap.WithKeys _≟_ isLatticeᵛ states +module StateVariablesFiniteMap = Lattice.FiniteMap.WithKeys _≟_ isLatticeᵛ states open StateVariablesFiniteMap using (_[_]; []-∈; m₁≼m₂⇒m₁[ks]≼m₂[ks]; m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂) renaming @@ -95,7 +95,7 @@ open StateVariablesFiniteMap ; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ ) public -open Lattice.FiniteValueMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight _≟_ isLatticeᵛ states-Unique ≈ᵛ-dec _ fixedHeightᵛ +open Lattice.FiniteMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight _≟_ isLatticeᵛ states-Unique ≈ᵛ-dec _ fixedHeightᵛ using () renaming ( isFiniteHeightLattice to isFiniteHeightLatticeᵐ @@ -149,7 +149,7 @@ joinForKey-Mono k {fm₁} {fm₂} fm₁≼fm₂ = (⊔ᵛ-idemp ⊥ᵛ) ⊔ᵛ-Monotonicʳ ⊔ᵛ-Monotonicˡ -- The name f' comes from the formulation of Exercise 4.26. -open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) joinForKey joinForKey-Mono states +open StateVariablesFiniteMap.GeneralizedUpdate isLatticeᵐ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) joinForKey joinForKey-Mono states using () renaming ( f' to joinAll diff --git a/Lattice/FiniteMap.agda b/Lattice/FiniteMap.agda index ee26419..17c2bda 100644 --- a/Lattice/FiniteMap.agda +++ b/Lattice/FiniteMap.agda @@ -4,15 +4,26 @@ open import Relation.Binary.PropositionalEquality as Eq 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} +module Lattice.FiniteMap {A : Set} {B : Set} + {_≈₂_ : B → B → Set} {_⊔₂_ : B → B → B} {_⊓₂_ : B → B → B} - (≡-dec-A : IsDecidable (_≡_ {a} {A})) + (≡-dec-A : IsDecidable (_≡_ {_} {A})) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where open IsLattice lB using () renaming (_≼_ to _≼₂_) open import Lattice.Map ≡-dec-A lB as Map - using (Map; ⊔-equal-keys; ⊓-equal-keys) + using + ( Map + ; ⊔-equal-keys + ; ⊓-equal-keys + ; subset-impl + ; Map-functional + ; Expr-Provenance + ; Expr-Provenance-≡ + ; `_; _∪_; _∩_ + ; in₁; in₂; bothᵘ; single + ; ⊔-combines + ) renaming ( _≈_ to _≈ᵐ_ ; _⊔_ to _⊔ᵐ_ @@ -46,17 +57,25 @@ open import Lattice.Map ≡-dec-A lB as Map ; _≼_ to _≼ᵐ_ ; ∈k-dec to ∈k-decᵐ ) +open import Data.Empty using (⊥-elim) +open import Data.List using (List; length; []; _∷_; map) open import Data.List.Membership.Propositional using () renaming (_∈_ to _∈ˡ_) -open import Data.Product using (_×_; _,_; Σ; proj₁ ; proj₂) +open import Data.List.Properties using (∷-injectiveʳ) +open import Data.List.Relation.Unary.All using (All) +open import Data.List.Relation.Unary.Any using (Any; here; there) +open import Data.Nat using (ℕ) +open import Data.Product using (_×_; _,_; Σ; proj₁; proj₂) open import Equivalence open import Function using (_∘_) +open import Relation.Binary.Definitions using (Decidable) open import Relation.Nullary using (¬_; Dec; yes; no) -open import Utils using (Pairwise; _∷_; []) -open import Data.Empty using (⊥-elim) +open import Utils using (Pairwise; _∷_; []; Unique; push; empty; All¬-¬Any) open import Showable using (Showable; show) +open import Isomorphism using (IsInverseˡ; IsInverseʳ) +open import Chain using (Height) module WithKeys (ks : List A) where - FiniteMap : Set (a ⊔ℓ b) + FiniteMap : Set FiniteMap = Σ Map (λ m → Map.keys m ≡ ks) instance @@ -64,7 +83,7 @@ module WithKeys (ks : List A) where Showable FiniteMap showable = record { show = λ (m₁ , _) → show m₁ } - _≈_ : FiniteMap → FiniteMap → Set (a ⊔ℓ b) + _≈_ : FiniteMap → FiniteMap → Set _≈_ (m₁ , _) (m₂ , _) = m₁ ≈ᵐ m₂ ≈₂-dec⇒≈-dec : IsDecidable _≈₂_ → IsDecidable _≈_ @@ -84,10 +103,10 @@ module WithKeys (ks : List A) where km₁≡ks ) - _∈_ : A × B → FiniteMap → Set (a ⊔ℓ b) + _∈_ : A × B → FiniteMap → Set _∈_ k,v (m₁ , _) = k,v ∈ˡ (proj₁ m₁) - _∈k_ : A → FiniteMap → Set a + _∈k_ : A → FiniteMap → Set _∈k_ k (m₁ , _) = k ∈ˡ (keysᵐ m₁) open Map using (forget) public @@ -230,3 +249,380 @@ module WithKeys (ks : List A) where ... | no k∉km₁ | yes k∈km₂ = ⊥-elim (∈k-exclusive fm₂ fm₁ (k∈km₂ , k∉km₁)) open WithKeys public + +module IterProdIsomorphism where + 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.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 {[]} (([] , _) , _) = tt + 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 {[]} _ ⊤ = (([] , empty) , refl) + to {k ∷ ks'} (push k≢ks' uks') (v , rest) = + let + ((fm' , ufm') , fm'≡ks') = to uks' rest + + -- This would be easier if we pattern matched on the equiality proof + -- to get refl, but that makes it harder to reason about 'to' when + -- the arguments are not known to be refl. + k≢fm' = subst (λ ks → All (λ k' → ¬ k ≡ k') ks) (sym fm'≡ks') k≢ks' + kvs≡ks = cong (k ∷_) fm'≡ks' + in + (((k , v) ∷ fm' , push k≢fm' ufm') , kvs≡ks) + + + private + _⊆ᵐ_ : ∀ {ks₁ ks₂ : List A} → FiniteMap ks₁ → FiniteMap ks₂ → Set + _⊆ᵐ_ fm₁ fm₂ = subset-impl (proj₁ (proj₁ fm₁)) (proj₁ (proj₁ fm₂)) + + _≈ⁱᵖ_ : ∀ {n : ℕ} → IterProd n → IterProd n → Set + _≈ⁱᵖ_ {n} = IP._≈_ n + + _⊔ⁱᵖ_ : ∀ {ks : List A} → + IterProd (length ks) → IterProd (length ks) → IterProd (length ks) + _⊔ⁱᵖ_ {ks} = IP._⊔_ (length ks) + + _∈ᵐ_ : ∀ {ks : List A} → A × B → FiniteMap ks → Set + _∈ᵐ_ {ks} = _∈_ ks + + to-build : ∀ {b : B} {ks : List A} (uks : Unique ks) → + let fm = to uks (IP.build b tt (length ks)) + in ∀ (k : A) (v : B) → (k , v) ∈ᵐ fm → v ≡ b + to-build {b} {k ∷ ks'} (push _ uks') k v (here refl) = refl + to-build {b} {k ∷ ks'} (push _ uks') k' v (there k',v∈m') = + to-build {ks = ks'} uks' k' v k',v∈m' + + + -- The left inverse is: from (to x) = x + from-to-inverseˡ : ∀ {ks : List A} (uks : Unique ks) → + IsInverseˡ (_≈_ ks) (_≈ⁱᵖ_ {length ks}) + (from {ks}) (to {ks} uks) + from-to-inverseˡ {[]} _ _ = IsEquivalence.≈-refl (IP.≈-equiv 0) + from-to-inverseˡ {k ∷ ks'} (push k≢ks' uks') (v , rest) + with ((fm' , ufm') , refl) ← to uks' rest in p rewrite sym p = + (IsLattice.≈-refl lB , from-to-inverseˡ {ks'} uks' rest) + -- the rewrite here is needed because the IH is in terms of `to uks' rest`, + -- but we end up with the 'unpacked' form (fm', ...). So, put it back + -- in the 'packed' form after we've performed enough inspection + -- to know we take the cons branch of `to`. + + -- The map has its own uniqueness proof, but the call to 'to' needs a standalone + -- uniqueness proof too. Work with both proofs as needed to thread things through. + -- + -- The right inverse is: to (from x) = x + from-to-inverseʳ : ∀ {ks : List A} (uks : Unique ks) → + IsInverseʳ (_≈_ ks) (_≈ⁱᵖ_ {length ks}) + (from {ks}) (to {ks} uks) + from-to-inverseʳ {[]} _ (([] , empty) , kvs≡ks) rewrite kvs≡ks = + ( (λ k v ()) + , (λ k v ()) + ) + from-to-inverseʳ {k ∷ ks'} uks@(push _ uks'₁) fm₁@(((k , v) ∷ fm'₁ , push _ uks'₂) , refl) + with to uks'₁ (from ((fm'₁ , uks'₂) , refl)) + | from-to-inverseʳ {ks'} uks'₁ ((fm'₁ , uks'₂) , refl) + ... | ((fm'₂ , ufm'₂) , _) + | (fm'₂⊆fm'₁ , fm'₁⊆fm'₂) = (m₂⊆m₁ , m₁⊆m₂) + where + kvs₁ = (k , v) ∷ fm'₁ + kvs₂ = (k , v) ∷ fm'₂ + + m₁⊆m₂ : subset-impl kvs₁ kvs₂ + m₁⊆m₂ k' v' (here refl) = + (v' , (IsLattice.≈-refl lB , here refl)) + m₁⊆m₂ k' v' (there k',v'∈fm'₁) = + let (v'' , (v'≈v'' , k',v''∈fm'₂)) = + fm'₁⊆fm'₂ k' v' k',v'∈fm'₁ + in (v'' , (v'≈v'' , there k',v''∈fm'₂)) + + m₂⊆m₁ : subset-impl kvs₂ kvs₁ + m₂⊆m₁ k' v' (here refl) = + (v' , (IsLattice.≈-refl lB , here refl)) + m₂⊆m₁ k' v' (there k',v'∈fm'₂) = + let (v'' , (v'≈v'' , k',v''∈fm'₁)) = + fm'₂⊆fm'₁ k' v' k',v'∈fm'₂ + in (v'' , (v'≈v'' , there k',v''∈fm'₁)) + + FromBothMaps : ∀ (k : A) (v : B) {ks : List A} (fm₁ fm₂ : FiniteMap ks) → Set + FromBothMaps k v fm₁ fm₂ = + Σ (B × B) + (λ (v₁ , v₂) → ( (v ≡ v₁ ⊔₂ v₂) × ((k , v₁) ∈ᵐ fm₁ × (k , v₂) ∈ᵐ fm₂))) + + Provenance-union : ∀ {ks : List A} (fm₁ fm₂ : FiniteMap ks) {k : A} {v : B} → + (k , v) ∈ᵐ (_⊔_ ks fm₁ fm₂) → FromBothMaps k v fm₁ fm₂ + Provenance-union fm₁@(m₁ , ks₁≡ks) fm₂@(m₂ , ks₂≡ks) {k} {v} k,v∈fm₁fm₂ + with Expr-Provenance-≡ ((` m₁) ∪ (` m₂)) k,v∈fm₁fm₂ + ... | in₁ (single k,v∈m₁) k∉km₂ + with k∈km₁ ← (forget k,v∈m₁) + rewrite trans ks₁≡ks (sym ks₂≡ks) = + ⊥-elim (k∉km₂ k∈km₁) + ... | in₂ k∉km₁ (single k,v∈m₂) + with k∈km₂ ← (forget k,v∈m₂) + rewrite trans ks₁≡ks (sym ks₂≡ks) = + ⊥-elim (k∉km₁ k∈km₂) + ... | bothᵘ {v₁} {v₂} (single k,v₁∈m₁) (single k,v₂∈m₂) = + ((v₁ , v₂) , (refl , (k,v₁∈m₁ , k,v₂∈m₂))) + + private + first-key-in-map : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) → + Σ B (λ v → (k , v) ∈ᵐ fm) + first-key-in-map (((k , v) ∷ _ , _) , refl) = (v , here refl) + + from-first-value : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) → + proj₁ (from fm) ≡ proj₁ (first-key-in-map fm) + from-first-value {k} {ks} (((k , v) ∷ _ , push _ _) , refl) = refl + + -- We need pop because reasoning about two distinct 'refl' pattern + -- matches is giving us unification errors. So, stash the 'refl' pattern + -- matching into a helper functions, and write solutions in terms + -- of that. + pop : ∀ {k : A} {ks : List A} → FiniteMap (k ∷ ks) → FiniteMap ks + pop (((_ ∷ fm') , push _ ufm') , refl) = ((fm' , ufm') , refl) + + pop-≈ : ∀ {k : A} {ks : List A} (fm₁ fm₂ : FiniteMap (k ∷ ks)) → + _≈_ _ fm₁ fm₂ → _≈_ _ (pop fm₁) (pop fm₂) + pop-≈ {k} {ks} fm₁ fm₂ (fm₁⊆fm₂ , fm₂⊆fm₁) = + (narrow fm₁⊆fm₂ , narrow fm₂⊆fm₁) + where + narrow₁ : ∀ {fm₁ fm₂ : FiniteMap (k ∷ ks)} → + fm₁ ⊆ᵐ fm₂ → pop fm₁ ⊆ᵐ fm₂ + narrow₁ {(_ ∷ _ , push _ _) , refl} kvs₁⊆kvs₂ k' v' k',v'∈fm'₁ = + kvs₁⊆kvs₂ k' v' (there k',v'∈fm'₁) + + narrow₂ : ∀ {fm₁ : FiniteMap ks} {fm₂ : FiniteMap (k ∷ ks)} → + fm₁ ⊆ᵐ fm₂ → fm₁ ⊆ᵐ pop fm₂ + narrow₂ {fm₁} {fm₂ = (_ ∷ fm'₂ , push k≢ks _) , kvs≡ks@refl} kvs₁⊆kvs₂ k' v' k',v'∈fm'₁ + with kvs₁⊆kvs₂ k' v' k',v'∈fm'₁ + ... | (v'' , (v'≈v'' , here refl)) rewrite sym (proj₂ fm₁) = + ⊥-elim (All¬-¬Any k≢ks (forget k',v'∈fm'₁)) + ... | (v'' , (v'≈v'' , there k',v'∈fm'₂)) = + (v'' , (v'≈v'' , k',v'∈fm'₂)) + + narrow : ∀ {fm₁ fm₂ : FiniteMap (k ∷ ks)} → + fm₁ ⊆ᵐ fm₂ → pop fm₁ ⊆ᵐ pop fm₂ + narrow {fm₁} {fm₂} x = narrow₂ {pop fm₁} (narrow₁ {fm₂ = fm₂} x) + + k,v∈pop⇒k,v∈ : ∀ {k : A} {ks : List A} {k' : A} {v : B} (fm : FiniteMap (k ∷ ks)) → + (k' , v) ∈ᵐ pop fm → (¬ k ≡ k' × ((k' , v) ∈ᵐ fm)) + k,v∈pop⇒k,v∈ {k} {ks} {k'} {v} (m@((k , _) ∷ fm' , push k≢ks uks') , refl) k',v∈fm = + ( (λ { refl → All¬-¬Any k≢ks (forget k',v∈fm) }) + , there k',v∈fm + ) + + k,v∈⇒k,v∈pop : ∀ {k : A} {ks : List A} {k' : A} {v : B} (fm : FiniteMap (k ∷ ks)) → + ¬ k ≡ k' → (k' , v) ∈ᵐ fm → (k' , v) ∈ᵐ pop fm + k,v∈⇒k,v∈pop (m@(_ ∷ _ , push k≢ks _) , refl) k≢k' (here refl) = ⊥-elim (k≢k' refl) + k,v∈⇒k,v∈pop (m@(_ ∷ _ , push k≢ks _) , refl) k≢k' (there k,v'∈fm') = k,v'∈fm' + + pop-⊔-distr : ∀ {k : A} {ks : List A} (fm₁ fm₂ : FiniteMap (k ∷ ks)) → + _≈_ _ (pop (_⊔_ _ fm₁ fm₂)) ((_⊔_ _ (pop fm₁) (pop fm₂))) + pop-⊔-distr {k} {ks} fm₁@(m₁ , _) fm₂@(m₂ , _) = + (pfm₁fm₂⊆pfm₁pfm₂ , pfm₁pfm₂⊆pfm₁fm₂) + where + -- pfm₁fm₂⊆pfm₁pfm₂ = {!!} + pfm₁fm₂⊆pfm₁pfm₂ : pop (_⊔_ _ fm₁ fm₂) ⊆ᵐ (_⊔_ _ (pop fm₁) (pop fm₂)) + pfm₁fm₂⊆pfm₁pfm₂ k' v' k',v'∈pfm₁fm₂ + with (k≢k' , k',v'∈fm₁fm₂) ← k,v∈pop⇒k,v∈ (_⊔_ _ fm₁ fm₂) k',v'∈pfm₁fm₂ + with ((v₁ , v₂) , (refl , (k,v₁∈fm₁ , k,v₂∈fm₂))) + ← Provenance-union fm₁ fm₂ k',v'∈fm₁fm₂ + with k',v₁∈pfm₁ ← k,v∈⇒k,v∈pop fm₁ k≢k' k,v₁∈fm₁ + with k',v₂∈pfm₂ ← k,v∈⇒k,v∈pop fm₂ k≢k' k,v₂∈fm₂ + = + ( v₁ ⊔₂ v₂ + , (IsLattice.≈-refl lB + , ⊔-combines {m₁ = proj₁ (pop fm₁)} + {m₂ = proj₁ (pop fm₂)} + k',v₁∈pfm₁ k',v₂∈pfm₂ + ) + ) + + pfm₁pfm₂⊆pfm₁fm₂ : (_⊔_ _ (pop fm₁) (pop fm₂)) ⊆ᵐ pop (_⊔_ _ fm₁ fm₂) + pfm₁pfm₂⊆pfm₁fm₂ k' v' k',v'∈pfm₁pfm₂ + with ((v₁ , v₂) , (refl , (k,v₁∈pfm₁ , k,v₂∈pfm₂))) + ← Provenance-union (pop fm₁) (pop fm₂) k',v'∈pfm₁pfm₂ + with (k≢k' , k',v₁∈fm₁) ← k,v∈pop⇒k,v∈ fm₁ k,v₁∈pfm₁ + with (_ , k',v₂∈fm₂) ← k,v∈pop⇒k,v∈ fm₂ k,v₂∈pfm₂ + = + ( v₁ ⊔₂ v₂ + , ( IsLattice.≈-refl lB + , k,v∈⇒k,v∈pop (_⊔_ _ fm₁ fm₂) k≢k' + (⊔-combines {m₁ = m₁} {m₂ = m₂} + k',v₁∈fm₁ k',v₂∈fm₂) + ) + ) + + from-rest : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) → + proj₂ (from fm) ≡ from (pop fm) + from-rest (((_ ∷ fm') , push _ ufm') , refl) = refl + + from-preserves-≈ : ∀ {ks : List A} → {fm₁ fm₂ : FiniteMap ks} → + _≈_ _ fm₁ fm₂ → (_≈ⁱᵖ_ {length ks}) (from fm₁) (from fm₂) + from-preserves-≈ {[]} {_} {_} _ = IsEquivalence.≈-refl ≈ᵘ-equiv + from-preserves-≈ {k ∷ ks'} {fm₁@(m₁ , _)} {fm₂@(m₂ , _)} fm₁≈fm₂@(kvs₁⊆kvs₂ , kvs₂⊆kvs₁) + with first-key-in-map fm₁ + | first-key-in-map fm₂ + | from-first-value fm₁ + | from-first-value fm₂ + ... | (v₁ , k,v₁∈fm₁) | (v₂ , k,v₂∈fm₂) | refl | refl + with kvs₁⊆kvs₂ _ _ k,v₁∈fm₁ + ... | (v₁' , (v₁≈v₁' , k,v₁'∈fm₂)) + rewrite Map-functional {m = m₂} k,v₂∈fm₂ k,v₁'∈fm₂ + rewrite from-rest fm₁ rewrite from-rest fm₂ + = + ( v₁≈v₁' + , from-preserves-≈ {ks'} {pop fm₁} {pop fm₂} + (pop-≈ fm₁ fm₂ fm₁≈fm₂) + ) + + to-preserves-≈ : ∀ {ks : List A} (uks : Unique ks) {ip₁ ip₂ : IterProd (length ks)} → + _≈ⁱᵖ_ {length ks} ip₁ ip₂ → _≈_ _ (to uks ip₁) (to uks ip₂) + to-preserves-≈ {[]} empty {tt} {tt} _ = ((λ k v ()), (λ k v ())) + to-preserves-≈ {k ∷ ks'} uks@(push k≢ks' uks') {ip₁@(v₁ , rest₁)} {ip₂@(v₂ , rest₂)} (v₁≈v₂ , rest₁≈rest₂) = (fm₁⊆fm₂ , fm₂⊆fm₁) + where + inductive-step : ∀ {v₁ v₂ : B} {rest₁ rest₂ : IterProd (length ks')} → + v₁ ≈₂ v₂ → _≈ⁱᵖ_ {length ks'} rest₁ rest₂ → + to uks (v₁ , rest₁) ⊆ᵐ to uks (v₂ , rest₂) + inductive-step {v₁} {v₂} {rest₁} {rest₂} v₁≈v₂ rest₁≈rest₂ k v k,v∈kvs₁ + with ((fm'₁ , ufm'₁) , fm'₁≡ks') ← to uks' rest₁ in p₁ + with ((fm'₂ , ufm'₂) , fm'₂≡ks') ← to uks' rest₂ in p₂ + with k,v∈kvs₁ + ... | here refl = (v₂ , (v₁≈v₂ , here refl)) + ... | there k,v∈fm'₁ with refl ← p₁ with refl ← p₂ = + let + (fm'₁⊆fm'₂ , _) = to-preserves-≈ uks' {rest₁} {rest₂} + rest₁≈rest₂ + (v' , (v≈v' , k,v'∈kvs₁)) = fm'₁⊆fm'₂ k v k,v∈fm'₁ + in + (v' , (v≈v' , there k,v'∈kvs₁)) + + fm₁⊆fm₂ : to uks ip₁ ⊆ᵐ to uks ip₂ + fm₁⊆fm₂ = inductive-step v₁≈v₂ rest₁≈rest₂ + + fm₂⊆fm₁ : to uks ip₂ ⊆ᵐ to uks ip₁ + fm₂⊆fm₁ = inductive-step (≈₂-sym v₁≈v₂) + (IP.≈-sym (length ks') rest₁≈rest₂) + + from-⊔-distr : ∀ {ks : List A} → (fm₁ fm₂ : FiniteMap ks) → + _≈ⁱᵖ_ {length ks} (from (_⊔_ _ fm₁ fm₂)) + (_⊔ⁱᵖ_ {ks} (from fm₁) (from fm₂)) + from-⊔-distr {[]} fm₁ fm₂ = IsEquivalence.≈-refl ≈ᵘ-equiv + from-⊔-distr {k ∷ ks} fm₁@(m₁ , _) fm₂@(m₂ , _) + with first-key-in-map (_⊔_ _ fm₁ fm₂) + | first-key-in-map fm₁ + | first-key-in-map fm₂ + | from-first-value (_⊔_ _ fm₁ fm₂) + | from-first-value fm₁ | from-first-value fm₂ + ... | (v , k,v∈fm₁fm₂) | (v₁ , k,v₁∈fm₁) | (v₂ , k,v₂∈fm₂) | refl | refl | refl + with Expr-Provenance k ((` m₁) ∪ (` m₂)) (forget k,v∈fm₁fm₂) + ... | (_ , (in₁ _ k∉km₂ , _)) = ⊥-elim (k∉km₂ (forget k,v₂∈fm₂)) + ... | (_ , (in₂ k∉km₁ _ , _)) = ⊥-elim (k∉km₁ (forget k,v₁∈fm₁)) + ... | (v₁⊔v₂ , (bothᵘ {v₁'} {v₂'} (single k,v₁'∈m₁) (single k,v₂'∈m₂) , k,v₁⊔v₂∈m₁m₂)) + rewrite Map-functional {m = m₁} k,v₁∈fm₁ k,v₁'∈m₁ + rewrite Map-functional {m = m₂} k,v₂∈fm₂ k,v₂'∈m₂ + rewrite Map-functional {m = proj₁ (_⊔_ _ fm₁ fm₂)} k,v∈fm₁fm₂ k,v₁⊔v₂∈m₁m₂ + rewrite from-rest (_⊔_ _ fm₁ fm₂) rewrite from-rest fm₁ rewrite from-rest fm₂ + = ( IsLattice.≈-refl lB + , IsEquivalence.≈-trans + (IP.≈-equiv (length ks)) + (from-preserves-≈ {_} {pop (_⊔_ _ fm₁ fm₂)} + {_⊔_ _ (pop fm₁) (pop fm₂)} + (pop-⊔-distr fm₁ fm₂)) + ((from-⊔-distr (pop fm₁) (pop fm₂))) + ) + + + to-⊔-distr : ∀ {ks : List A} (uks : Unique ks) → (ip₁ ip₂ : IterProd (length ks)) → + _≈_ _ (to uks (_⊔ⁱᵖ_ {ks} ip₁ ip₂)) ((_⊔_ _ (to uks ip₁) (to uks ip₂))) + to-⊔-distr {[]} empty tt tt = ((λ k v ()), (λ k v ())) + to-⊔-distr {ks@(k ∷ ks')} uks@(push k≢ks' uks') ip₁@(v₁ , rest₁) ip₂@(v₂ , rest₂) = (fm⊆fm₁fm₂ , fm₁fm₂⊆fm) + where + fm₁ = to uks ip₁ + fm₁' = to uks' rest₁ + fm₂ = to uks ip₂ + fm₂' = to uks' rest₂ + fm = to uks (_⊔ⁱᵖ_ {k ∷ ks'} ip₁ ip₂) + + fm⊆fm₁fm₂ : fm ⊆ᵐ (_⊔_ _ fm₁ fm₂) + fm⊆fm₁fm₂ k v (here refl) = + (v₁ ⊔₂ v₂ + , (IsLattice.≈-refl lB + , ⊔-combines {k} {v₁} {v₂} {proj₁ fm₁} {proj₁ fm₂} + (here refl) (here refl) + ) + ) + fm⊆fm₁fm₂ k' v (there k',v∈fm') + with (fm'⊆fm'₁fm'₂ , _) ← to-⊔-distr uks' rest₁ rest₂ + with (v' , (v₁⊔v₂≈v' , k',v'∈fm'₁fm'₂)) + ← fm'⊆fm'₁fm'₂ k' v k',v∈fm' + with (_ , (refl , (v₁∈fm'₁ , v₂∈fm'₂))) + ← Provenance-union fm₁' fm₂' k',v'∈fm'₁fm'₂ = + ( v' + , ( v₁⊔v₂≈v' + , ⊔-combines {m₁ = proj₁ fm₁} {m₂ = proj₁ fm₂} + (there v₁∈fm'₁) (there v₂∈fm'₂) + ) + ) + + fm₁fm₂⊆fm : (_⊔_ _ fm₁ fm₂) ⊆ᵐ fm + fm₁fm₂⊆fm k' v k',v∈fm₁fm₂ + with (_ , fm'₁fm'₂⊆fm') + ← to-⊔-distr uks' rest₁ rest₂ + with (_ , (refl , (v₁∈fm₁ , v₂∈fm₂))) + ← Provenance-union fm₁ fm₂ k',v∈fm₁fm₂ + with v₁∈fm₁ | v₂∈fm₂ + ... | here refl | here refl = + (v , (IsLattice.≈-refl lB , here refl)) + ... | here refl | there k',v₂∈fm₂' = + ⊥-elim (All¬-¬Any k≢ks' (subst (k' ∈ˡ_) (proj₂ fm₂') + (forget k',v₂∈fm₂'))) + ... | there k',v₁∈fm₁' | here refl = + ⊥-elim (All¬-¬Any k≢ks' (subst (k' ∈ˡ_) (proj₂ fm₁') + (forget k',v₁∈fm₁'))) + ... | there k',v₁∈fm₁' | there k',v₂∈fm₂' = + let + k',v₁v₂∈fm₁'fm₂' = + ⊔-combines {m₁ = proj₁ fm₁'} {m₂ = proj₁ fm₂'} + k',v₁∈fm₁' k',v₂∈fm₂' + (v' , (v₁⊔v₂≈v' , v'∈fm')) = + fm'₁fm'₂⊆fm' _ _ k',v₁v₂∈fm₁'fm₂' + in + (v' , (v₁⊔v₂≈v' , there v'∈fm')) + + module WithUniqueKeysAndFixedHeight {ks : List A} (uks : Unique ks) (≈₂-dec : Decidable _≈₂_) (h₂ : ℕ) (fhB : FixedHeight₂ h₂) where + import Isomorphism + open Isomorphism.TransportFiniteHeight + (IP.isFiniteHeightLattice (length ks) ≈₂-dec ≈ᵘ-dec h₂ 0 fhB fixedHeightᵘ) (isLattice ks) + {f = to uks} {g = from {ks}} + (to-preserves-≈ uks) (from-preserves-≈ {ks}) + (to-⊔-distr uks) (from-⊔-distr {ks}) + (from-to-inverseʳ uks) (from-to-inverseˡ uks) + using (isFiniteHeightLattice; finiteHeightLattice) public + + -- Helpful lemma: all entries of the 'bottom' map are assigned to bottom. + + open Height (IsFiniteHeightLattice.fixedHeight isFiniteHeightLattice) using (⊥) + + ⊥-contains-bottoms : ∀ {k : A} {v : B} → (k , v) ∈ᵐ ⊥ → v ≡ (Height.⊥ fhB) + ⊥-contains-bottoms {k} {v} k,v∈⊥ + rewrite IP.⊥-built (length ks) ≈₂-dec ≈ᵘ-dec h₂ 0 fhB fixedHeightᵘ = + to-build uks k v k,v∈⊥ diff --git a/Lattice/FiniteValueMap.agda b/Lattice/FiniteValueMap.agda deleted file mode 100644 index 998807c..0000000 --- a/Lattice/FiniteValueMap.agda +++ /dev/null @@ -1,427 +0,0 @@ --- Because iterated products currently require both A and B to be of the same --- universe, and the FiniteMap is written in a universe-polymorphic way, --- specialize the FiniteMap module with Set-typed types only. - -open import Lattice -open import Equivalence -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 Function.Definitions using (Inverseˡ; Inverseʳ) - -module Lattice.FiniteValueMap {A : Set} {B : Set} - {_≈₂_ : B → B → Set} - {_⊔₂_ : B → B → B} {_⊓₂_ : B → B → B} - (≡-dec-A : Decidable (_≡_ {_} {A})) - (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where - -open import Data.List using (List; length; []; _∷_; map) -open import Data.List.Membership.Propositional using () renaming (_∈_ to _∈ˡ_) -open import Data.Nat using (ℕ) -open import Data.Product using (Σ; proj₁; proj₂; _×_) -open import Data.Empty using (⊥-elim) -open import Utils using (Unique; push; empty; All¬-¬Any) -open import Data.Product using (_,_) -open import Data.List.Properties using (∷-injectiveʳ) -open import Data.List.Relation.Unary.All using (All) -open import Data.List.Relation.Unary.Any using (Any; here; there) -open import Relation.Nullary using (¬_) -open import Isomorphism using (IsInverseˡ; IsInverseʳ) -open import Chain using (Height) - -open import Lattice.Map ≡-dec-A lB - using - ( subset-impl - ; locate - ; Map-functional - ; Expr-Provenance - ; Expr-Provenance-≡ - ; _∩_; _∪_; `_ - ; in₁; in₂; bothᵘ; single - ; ⊔-combines - ) -open import Lattice.FiniteMap ≡-dec-A lB public - -module IterProdIsomorphism where - 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.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 {[]} (([] , _) , _) = tt - 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 {[]} _ ⊤ = (([] , empty) , refl) - to {k ∷ ks'} (push k≢ks' uks') (v , rest) = - let - ((fm' , ufm') , fm'≡ks') = to uks' rest - - -- This would be easier if we pattern matched on the equiality proof - -- to get refl, but that makes it harder to reason about 'to' when - -- the arguments are not known to be refl. - k≢fm' = subst (λ ks → All (λ k' → ¬ k ≡ k') ks) (sym fm'≡ks') k≢ks' - kvs≡ks = cong (k ∷_) fm'≡ks' - in - (((k , v) ∷ fm' , push k≢fm' ufm') , kvs≡ks) - - - private - _≈ᵐ_ : ∀ {ks : List A} → FiniteMap ks → FiniteMap ks → Set - _≈ᵐ_ {ks} = _≈_ ks - - _⊔ᵐ_ : ∀ {ks : List A} → FiniteMap ks → FiniteMap ks → FiniteMap ks - _⊔ᵐ_ {ks} = _⊔_ ks - - _⊆ᵐ_ : ∀ {ks₁ ks₂ : List A} → FiniteMap ks₁ → FiniteMap ks₂ → Set - _⊆ᵐ_ fm₁ fm₂ = subset-impl (proj₁ (proj₁ fm₁)) (proj₁ (proj₁ fm₂)) - - _≈ⁱᵖ_ : ∀ {n : ℕ} → IterProd n → IterProd n → Set - _≈ⁱᵖ_ {n} = IP._≈_ n - - _⊔ⁱᵖ_ : ∀ {ks : List A} → - IterProd (length ks) → IterProd (length ks) → IterProd (length ks) - _⊔ⁱᵖ_ {ks} = IP._⊔_ (length ks) - - _∈ᵐ_ : ∀ {ks : List A} → A × B → FiniteMap ks → Set - _∈ᵐ_ {ks} = _∈_ ks - - to-build : ∀ {b : B} {ks : List A} (uks : Unique ks) → - let fm = to uks (IP.build b tt (length ks)) - in ∀ (k : A) (v : B) → (k , v) ∈ᵐ fm → v ≡ b - to-build {b} {k ∷ ks'} (push _ uks') k v (here refl) = refl - to-build {b} {k ∷ ks'} (push _ uks') k' v (there k',v∈m') = - to-build {ks = ks'} uks' k' v k',v∈m' - - - -- The left inverse is: from (to x) = x - from-to-inverseˡ : ∀ {ks : List A} (uks : Unique ks) → - IsInverseˡ (_≈ᵐ_ {ks}) (_≈ⁱᵖ_ {length ks}) - (from {ks}) (to {ks} uks) - from-to-inverseˡ {[]} _ _ = IsEquivalence.≈-refl (IP.≈-equiv 0) - from-to-inverseˡ {k ∷ ks'} (push k≢ks' uks') (v , rest) - with ((fm' , ufm') , refl) ← to uks' rest in p rewrite sym p = - (IsLattice.≈-refl lB , from-to-inverseˡ {ks'} uks' rest) - -- the rewrite here is needed because the IH is in terms of `to uks' rest`, - -- but we end up with the 'unpacked' form (fm', ...). So, put it back - -- in the 'packed' form after we've performed enough inspection - -- to know we take the cons branch of `to`. - - -- The map has its own uniqueness proof, but the call to 'to' needs a standalone - -- uniqueness proof too. Work with both proofs as needed to thread things through. - -- - -- The right inverse is: to (from x) = x - from-to-inverseʳ : ∀ {ks : List A} (uks : Unique ks) → - IsInverseʳ (_≈ᵐ_ {ks}) (_≈ⁱᵖ_ {length ks}) - (from {ks}) (to {ks} uks) - from-to-inverseʳ {[]} _ (([] , empty) , kvs≡ks) rewrite kvs≡ks = - ( (λ k v ()) - , (λ k v ()) - ) - from-to-inverseʳ {k ∷ ks'} uks@(push _ uks'₁) fm₁@(((k , v) ∷ fm'₁ , push _ uks'₂) , refl) - with to uks'₁ (from ((fm'₁ , uks'₂) , refl)) - | from-to-inverseʳ {ks'} uks'₁ ((fm'₁ , uks'₂) , refl) - ... | ((fm'₂ , ufm'₂) , _) - | (fm'₂⊆fm'₁ , fm'₁⊆fm'₂) = (m₂⊆m₁ , m₁⊆m₂) - where - kvs₁ = (k , v) ∷ fm'₁ - kvs₂ = (k , v) ∷ fm'₂ - - m₁⊆m₂ : subset-impl kvs₁ kvs₂ - m₁⊆m₂ k' v' (here refl) = - (v' , (IsLattice.≈-refl lB , here refl)) - m₁⊆m₂ k' v' (there k',v'∈fm'₁) = - let (v'' , (v'≈v'' , k',v''∈fm'₂)) = - fm'₁⊆fm'₂ k' v' k',v'∈fm'₁ - in (v'' , (v'≈v'' , there k',v''∈fm'₂)) - - m₂⊆m₁ : subset-impl kvs₂ kvs₁ - m₂⊆m₁ k' v' (here refl) = - (v' , (IsLattice.≈-refl lB , here refl)) - m₂⊆m₁ k' v' (there k',v'∈fm'₂) = - let (v'' , (v'≈v'' , k',v''∈fm'₁)) = - fm'₂⊆fm'₁ k' v' k',v'∈fm'₂ - in (v'' , (v'≈v'' , there k',v''∈fm'₁)) - - FromBothMaps : ∀ (k : A) (v : B) {ks : List A} (fm₁ fm₂ : FiniteMap ks) → Set - FromBothMaps k v fm₁ fm₂ = - Σ (B × B) - (λ (v₁ , v₂) → ( (v ≡ v₁ ⊔₂ v₂) × ((k , v₁) ∈ᵐ fm₁ × (k , v₂) ∈ᵐ fm₂))) - - Provenance-union : ∀ {ks : List A} (fm₁ fm₂ : FiniteMap ks) {k : A} {v : B} → - (k , v) ∈ᵐ (fm₁ ⊔ᵐ fm₂) → FromBothMaps k v fm₁ fm₂ - Provenance-union fm₁@(m₁ , ks₁≡ks) fm₂@(m₂ , ks₂≡ks) {k} {v} k,v∈fm₁fm₂ - with Expr-Provenance-≡ ((` m₁) ∪ (` m₂)) k,v∈fm₁fm₂ - ... | in₁ (single k,v∈m₁) k∉km₂ - with k∈km₁ ← (forget k,v∈m₁) - rewrite trans ks₁≡ks (sym ks₂≡ks) = - ⊥-elim (k∉km₂ k∈km₁) - ... | in₂ k∉km₁ (single k,v∈m₂) - with k∈km₂ ← (forget k,v∈m₂) - rewrite trans ks₁≡ks (sym ks₂≡ks) = - ⊥-elim (k∉km₁ k∈km₂) - ... | bothᵘ {v₁} {v₂} (single k,v₁∈m₁) (single k,v₂∈m₂) = - ((v₁ , v₂) , (refl , (k,v₁∈m₁ , k,v₂∈m₂))) - - private - first-key-in-map : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) → - Σ B (λ v → (k , v) ∈ᵐ fm) - first-key-in-map (((k , v) ∷ _ , _) , refl) = (v , here refl) - - from-first-value : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) → - proj₁ (from fm) ≡ proj₁ (first-key-in-map fm) - from-first-value {k} {ks} (((k , v) ∷ _ , push _ _) , refl) = refl - - -- We need pop because reasoning about two distinct 'refl' pattern - -- matches is giving us unification errors. So, stash the 'refl' pattern - -- matching into a helper functions, and write solutions in terms - -- of that. - pop : ∀ {k : A} {ks : List A} → FiniteMap (k ∷ ks) → FiniteMap ks - pop (((_ ∷ fm') , push _ ufm') , refl) = ((fm' , ufm') , refl) - - pop-≈ : ∀ {k : A} {ks : List A} (fm₁ fm₂ : FiniteMap (k ∷ ks)) → - fm₁ ≈ᵐ fm₂ → pop fm₁ ≈ᵐ pop fm₂ - pop-≈ {k} {ks} fm₁ fm₂ (fm₁⊆fm₂ , fm₂⊆fm₁) = - (narrow fm₁⊆fm₂ , narrow fm₂⊆fm₁) - where - narrow₁ : ∀ {fm₁ fm₂ : FiniteMap (k ∷ ks)} → - fm₁ ⊆ᵐ fm₂ → pop fm₁ ⊆ᵐ fm₂ - narrow₁ {(_ ∷ _ , push _ _) , refl} kvs₁⊆kvs₂ k' v' k',v'∈fm'₁ = - kvs₁⊆kvs₂ k' v' (there k',v'∈fm'₁) - - narrow₂ : ∀ {fm₁ : FiniteMap ks} {fm₂ : FiniteMap (k ∷ ks)} → - fm₁ ⊆ᵐ fm₂ → fm₁ ⊆ᵐ pop fm₂ - narrow₂ {fm₁} {fm₂ = (_ ∷ fm'₂ , push k≢ks _) , kvs≡ks@refl} kvs₁⊆kvs₂ k' v' k',v'∈fm'₁ - with kvs₁⊆kvs₂ k' v' k',v'∈fm'₁ - ... | (v'' , (v'≈v'' , here refl)) rewrite sym (proj₂ fm₁) = - ⊥-elim (All¬-¬Any k≢ks (forget k',v'∈fm'₁)) - ... | (v'' , (v'≈v'' , there k',v'∈fm'₂)) = - (v'' , (v'≈v'' , k',v'∈fm'₂)) - - narrow : ∀ {fm₁ fm₂ : FiniteMap (k ∷ ks)} → - fm₁ ⊆ᵐ fm₂ → pop fm₁ ⊆ᵐ pop fm₂ - narrow {fm₁} {fm₂} x = narrow₂ {pop fm₁} (narrow₁ {fm₂ = fm₂} x) - - k,v∈pop⇒k,v∈ : ∀ {k : A} {ks : List A} {k' : A} {v : B} (fm : FiniteMap (k ∷ ks)) → - (k' , v) ∈ᵐ pop fm → (¬ k ≡ k' × ((k' , v) ∈ᵐ fm)) - k,v∈pop⇒k,v∈ {k} {ks} {k'} {v} (m@((k , _) ∷ fm' , push k≢ks uks') , refl) k',v∈fm = - ( (λ { refl → All¬-¬Any k≢ks (forget k',v∈fm) }) - , there k',v∈fm - ) - - k,v∈⇒k,v∈pop : ∀ {k : A} {ks : List A} {k' : A} {v : B} (fm : FiniteMap (k ∷ ks)) → - ¬ k ≡ k' → (k' , v) ∈ᵐ fm → (k' , v) ∈ᵐ pop fm - k,v∈⇒k,v∈pop (m@(_ ∷ _ , push k≢ks _) , refl) k≢k' (here refl) = ⊥-elim (k≢k' refl) - k,v∈⇒k,v∈pop (m@(_ ∷ _ , push k≢ks _) , refl) k≢k' (there k,v'∈fm') = k,v'∈fm' - - pop-⊔-distr : ∀ {k : A} {ks : List A} (fm₁ fm₂ : FiniteMap (k ∷ ks)) → - pop (fm₁ ⊔ᵐ fm₂) ≈ᵐ (pop fm₁ ⊔ᵐ pop fm₂) - pop-⊔-distr {k} {ks} fm₁@(m₁ , _) fm₂@(m₂ , _) = - (pfm₁fm₂⊆pfm₁pfm₂ , pfm₁pfm₂⊆pfm₁fm₂) - where - -- pfm₁fm₂⊆pfm₁pfm₂ = {!!} - pfm₁fm₂⊆pfm₁pfm₂ : pop (fm₁ ⊔ᵐ fm₂) ⊆ᵐ (pop fm₁ ⊔ᵐ pop fm₂) - pfm₁fm₂⊆pfm₁pfm₂ k' v' k',v'∈pfm₁fm₂ - with (k≢k' , k',v'∈fm₁fm₂) ← k,v∈pop⇒k,v∈ (fm₁ ⊔ᵐ fm₂) k',v'∈pfm₁fm₂ - with ((v₁ , v₂) , (refl , (k,v₁∈fm₁ , k,v₂∈fm₂))) - ← Provenance-union fm₁ fm₂ k',v'∈fm₁fm₂ - with k',v₁∈pfm₁ ← k,v∈⇒k,v∈pop fm₁ k≢k' k,v₁∈fm₁ - with k',v₂∈pfm₂ ← k,v∈⇒k,v∈pop fm₂ k≢k' k,v₂∈fm₂ - = - ( v₁ ⊔₂ v₂ - , (IsLattice.≈-refl lB - , ⊔-combines {m₁ = proj₁ (pop fm₁)} - {m₂ = proj₁ (pop fm₂)} - k',v₁∈pfm₁ k',v₂∈pfm₂ - ) - ) - - pfm₁pfm₂⊆pfm₁fm₂ : (pop fm₁ ⊔ᵐ pop fm₂) ⊆ᵐ pop (fm₁ ⊔ᵐ fm₂) - pfm₁pfm₂⊆pfm₁fm₂ k' v' k',v'∈pfm₁pfm₂ - with ((v₁ , v₂) , (refl , (k,v₁∈pfm₁ , k,v₂∈pfm₂))) - ← Provenance-union (pop fm₁) (pop fm₂) k',v'∈pfm₁pfm₂ - with (k≢k' , k',v₁∈fm₁) ← k,v∈pop⇒k,v∈ fm₁ k,v₁∈pfm₁ - with (_ , k',v₂∈fm₂) ← k,v∈pop⇒k,v∈ fm₂ k,v₂∈pfm₂ - = - ( v₁ ⊔₂ v₂ - , ( IsLattice.≈-refl lB - , k,v∈⇒k,v∈pop (fm₁ ⊔ᵐ fm₂) k≢k' - (⊔-combines {m₁ = m₁} {m₂ = m₂} - k',v₁∈fm₁ k',v₂∈fm₂) - ) - ) - - from-rest : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) → - proj₂ (from fm) ≡ from (pop fm) - from-rest (((_ ∷ fm') , push _ ufm') , refl) = refl - - from-preserves-≈ : ∀ {ks : List A} → {fm₁ fm₂ : FiniteMap ks} → - fm₁ ≈ᵐ fm₂ → (_≈ⁱᵖ_ {length ks}) (from fm₁) (from fm₂) - from-preserves-≈ {[]} {_} {_} _ = IsEquivalence.≈-refl ≈ᵘ-equiv - from-preserves-≈ {k ∷ ks'} {fm₁@(m₁ , _)} {fm₂@(m₂ , _)} fm₁≈fm₂@(kvs₁⊆kvs₂ , kvs₂⊆kvs₁) - with first-key-in-map fm₁ - | first-key-in-map fm₂ - | from-first-value fm₁ - | from-first-value fm₂ - ... | (v₁ , k,v₁∈fm₁) | (v₂ , k,v₂∈fm₂) | refl | refl - with kvs₁⊆kvs₂ _ _ k,v₁∈fm₁ - ... | (v₁' , (v₁≈v₁' , k,v₁'∈fm₂)) - rewrite Map-functional {m = m₂} k,v₂∈fm₂ k,v₁'∈fm₂ - rewrite from-rest fm₁ rewrite from-rest fm₂ - = - ( v₁≈v₁' - , from-preserves-≈ {ks'} {pop fm₁} {pop fm₂} - (pop-≈ fm₁ fm₂ fm₁≈fm₂) - ) - - to-preserves-≈ : ∀ {ks : List A} (uks : Unique ks) {ip₁ ip₂ : IterProd (length ks)} → - _≈ⁱᵖ_ {length ks} ip₁ ip₂ → to uks ip₁ ≈ᵐ to uks ip₂ - to-preserves-≈ {[]} empty {tt} {tt} _ = ((λ k v ()), (λ k v ())) - to-preserves-≈ {k ∷ ks'} uks@(push k≢ks' uks') {ip₁@(v₁ , rest₁)} {ip₂@(v₂ , rest₂)} (v₁≈v₂ , rest₁≈rest₂) = (fm₁⊆fm₂ , fm₂⊆fm₁) - where - inductive-step : ∀ {v₁ v₂ : B} {rest₁ rest₂ : IterProd (length ks')} → - v₁ ≈₂ v₂ → _≈ⁱᵖ_ {length ks'} rest₁ rest₂ → - to uks (v₁ , rest₁) ⊆ᵐ to uks (v₂ , rest₂) - inductive-step {v₁} {v₂} {rest₁} {rest₂} v₁≈v₂ rest₁≈rest₂ k v k,v∈kvs₁ - with ((fm'₁ , ufm'₁) , fm'₁≡ks') ← to uks' rest₁ in p₁ - with ((fm'₂ , ufm'₂) , fm'₂≡ks') ← to uks' rest₂ in p₂ - with k,v∈kvs₁ - ... | here refl = (v₂ , (v₁≈v₂ , here refl)) - ... | there k,v∈fm'₁ with refl ← p₁ with refl ← p₂ = - let - (fm'₁⊆fm'₂ , _) = to-preserves-≈ uks' {rest₁} {rest₂} - rest₁≈rest₂ - (v' , (v≈v' , k,v'∈kvs₁)) = fm'₁⊆fm'₂ k v k,v∈fm'₁ - in - (v' , (v≈v' , there k,v'∈kvs₁)) - - fm₁⊆fm₂ : to uks ip₁ ⊆ᵐ to uks ip₂ - fm₁⊆fm₂ = inductive-step v₁≈v₂ rest₁≈rest₂ - - fm₂⊆fm₁ : to uks ip₂ ⊆ᵐ to uks ip₁ - fm₂⊆fm₁ = inductive-step (≈₂-sym v₁≈v₂) - (IP.≈-sym (length ks') rest₁≈rest₂) - - from-⊔-distr : ∀ {ks : List A} → (fm₁ fm₂ : FiniteMap ks) → - _≈ⁱᵖ_ {length ks} (from (fm₁ ⊔ᵐ fm₂)) - (_⊔ⁱᵖ_ {ks} (from fm₁) (from fm₂)) - from-⊔-distr {[]} fm₁ fm₂ = IsEquivalence.≈-refl ≈ᵘ-equiv - from-⊔-distr {k ∷ ks} fm₁@(m₁ , _) fm₂@(m₂ , _) - with first-key-in-map (fm₁ ⊔ᵐ fm₂) - | first-key-in-map fm₁ - | first-key-in-map fm₂ - | from-first-value (fm₁ ⊔ᵐ fm₂) - | from-first-value fm₁ | from-first-value fm₂ - ... | (v , k,v∈fm₁fm₂) | (v₁ , k,v₁∈fm₁) | (v₂ , k,v₂∈fm₂) | refl | refl | refl - with Expr-Provenance k ((` m₁) ∪ (` m₂)) (forget k,v∈fm₁fm₂) - ... | (_ , (in₁ _ k∉km₂ , _)) = ⊥-elim (k∉km₂ (forget k,v₂∈fm₂)) - ... | (_ , (in₂ k∉km₁ _ , _)) = ⊥-elim (k∉km₁ (forget k,v₁∈fm₁)) - ... | (v₁⊔v₂ , (bothᵘ {v₁'} {v₂'} (single k,v₁'∈m₁) (single k,v₂'∈m₂) , k,v₁⊔v₂∈m₁m₂)) - rewrite Map-functional {m = m₁} k,v₁∈fm₁ k,v₁'∈m₁ - rewrite Map-functional {m = m₂} k,v₂∈fm₂ k,v₂'∈m₂ - rewrite Map-functional {m = proj₁ (fm₁ ⊔ᵐ fm₂)} k,v∈fm₁fm₂ k,v₁⊔v₂∈m₁m₂ - rewrite from-rest (fm₁ ⊔ᵐ fm₂) rewrite from-rest fm₁ rewrite from-rest fm₂ - = ( IsLattice.≈-refl lB - , IsEquivalence.≈-trans - (IP.≈-equiv (length ks)) - (from-preserves-≈ {_} {pop (fm₁ ⊔ᵐ fm₂)} - {pop fm₁ ⊔ᵐ pop fm₂} - (pop-⊔-distr fm₁ fm₂)) - ((from-⊔-distr (pop fm₁) (pop fm₂))) - ) - - - to-⊔-distr : ∀ {ks : List A} (uks : Unique ks) → (ip₁ ip₂ : IterProd (length ks)) → - to uks (_⊔ⁱᵖ_ {ks} ip₁ ip₂) ≈ᵐ (to uks ip₁ ⊔ᵐ to uks ip₂) - to-⊔-distr {[]} empty tt tt = ((λ k v ()), (λ k v ())) - to-⊔-distr {ks@(k ∷ ks')} uks@(push k≢ks' uks') ip₁@(v₁ , rest₁) ip₂@(v₂ , rest₂) = (fm⊆fm₁fm₂ , fm₁fm₂⊆fm) - where - fm₁ = to uks ip₁ - fm₁' = to uks' rest₁ - fm₂ = to uks ip₂ - fm₂' = to uks' rest₂ - fm = to uks (_⊔ⁱᵖ_ {k ∷ ks'} ip₁ ip₂) - - fm⊆fm₁fm₂ : fm ⊆ᵐ (fm₁ ⊔ᵐ fm₂) - fm⊆fm₁fm₂ k v (here refl) = - (v₁ ⊔₂ v₂ - , (IsLattice.≈-refl lB - , ⊔-combines {k} {v₁} {v₂} {proj₁ fm₁} {proj₁ fm₂} - (here refl) (here refl) - ) - ) - fm⊆fm₁fm₂ k' v (there k',v∈fm') - with (fm'⊆fm'₁fm'₂ , _) ← to-⊔-distr uks' rest₁ rest₂ - with (v' , (v₁⊔v₂≈v' , k',v'∈fm'₁fm'₂)) - ← fm'⊆fm'₁fm'₂ k' v k',v∈fm' - with (_ , (refl , (v₁∈fm'₁ , v₂∈fm'₂))) - ← Provenance-union fm₁' fm₂' k',v'∈fm'₁fm'₂ = - ( v' - , ( v₁⊔v₂≈v' - , ⊔-combines {m₁ = proj₁ fm₁} {m₂ = proj₁ fm₂} - (there v₁∈fm'₁) (there v₂∈fm'₂) - ) - ) - - fm₁fm₂⊆fm : (fm₁ ⊔ᵐ fm₂) ⊆ᵐ fm - fm₁fm₂⊆fm k' v k',v∈fm₁fm₂ - with (_ , fm'₁fm'₂⊆fm') - ← to-⊔-distr uks' rest₁ rest₂ - with (_ , (refl , (v₁∈fm₁ , v₂∈fm₂))) - ← Provenance-union fm₁ fm₂ k',v∈fm₁fm₂ - with v₁∈fm₁ | v₂∈fm₂ - ... | here refl | here refl = - (v , (IsLattice.≈-refl lB , here refl)) - ... | here refl | there k',v₂∈fm₂' = - ⊥-elim (All¬-¬Any k≢ks' (subst (k' ∈ˡ_) (proj₂ fm₂') - (forget k',v₂∈fm₂'))) - ... | there k',v₁∈fm₁' | here refl = - ⊥-elim (All¬-¬Any k≢ks' (subst (k' ∈ˡ_) (proj₂ fm₁') - (forget k',v₁∈fm₁'))) - ... | there k',v₁∈fm₁' | there k',v₂∈fm₂' = - let - k',v₁v₂∈fm₁'fm₂' = - ⊔-combines {m₁ = proj₁ fm₁'} {m₂ = proj₁ fm₂'} - k',v₁∈fm₁' k',v₂∈fm₂' - (v' , (v₁⊔v₂≈v' , v'∈fm')) = - fm'₁fm'₂⊆fm' _ _ k',v₁v₂∈fm₁'fm₂' - in - (v' , (v₁⊔v₂≈v' , there v'∈fm')) - - module WithUniqueKeysAndFixedHeight {ks : List A} (uks : Unique ks) (≈₂-dec : Decidable _≈₂_) (h₂ : ℕ) (fhB : FixedHeight₂ h₂) where - import Isomorphism - open Isomorphism.TransportFiniteHeight - (IP.isFiniteHeightLattice (length ks) ≈₂-dec ≈ᵘ-dec h₂ 0 fhB fixedHeightᵘ) (isLattice ks) - {f = to uks} {g = from {ks}} - (to-preserves-≈ uks) (from-preserves-≈ {ks}) - (to-⊔-distr uks) (from-⊔-distr {ks}) - (from-to-inverseʳ uks) (from-to-inverseˡ uks) - using (isFiniteHeightLattice; finiteHeightLattice) public - - -- Helpful lemma: all entries of the 'bottom' map are assigned to bottom. - - open Height (IsFiniteHeightLattice.fixedHeight isFiniteHeightLattice) using (⊥) - - ⊥-contains-bottoms : ∀ {k : A} {v : B} → (k , v) ∈ᵐ ⊥ → v ≡ (Height.⊥ fhB) - ⊥-contains-bottoms {k} {v} k,v∈⊥ - rewrite IP.⊥-built (length ks) ≈₂-dec ≈ᵘ-dec h₂ 0 fhB fixedHeightᵘ = - to-build uks k v k,v∈⊥