Fuse 'FiniteMap' and 'FiniteValueMap'
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
c2c04e3ecd
commit
4da9b6d3cd
@ -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
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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∈⊥
|
||||
|
@ -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∈⊥
|
Loading…
Reference in New Issue
Block a user