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

Compare commits

base: DanilaFe:3d2a507f2ffabc096c08534d9a9a3826ee12c2a9
Branches Tags
DanilaFe:main
..
compare: DanilaFe:f0b0d51b488be7f4aab036bc8527ef4fd0734585
Branches Tags
DanilaFe:main

No commits in common. "3d2a507f2ffabc096c08534d9a9a3826ee12c2a9" and "f0b0d51b488be7f4aab036bc8527ef4fd0734585" have entirely different histories.
3d2a507f2f ... f0b0d51b48

14 changed files with 136 additions and 333 deletions
Show Stats Expand all files Collapse all files

100
Analysis/Forward.agda
View File

@ -10,18 +10,16 @@ module Analysis.Forward
open import Data.Empty using (⊥-elim)
open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
open import Data.Nat using (suc)
open import Data.Product using (_×_; proj₁; proj₂; _,_)
open import Data.Sum using (inj₁; inj₂)
open import Data.Product using (_×_; proj₁; _,_)
open import Data.List using (List; _∷_; []; foldr; foldl; cartesianProduct; cartesianProductWith)
open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_)
open import Data.List.Relation.Unary.Any as Any using ()
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym; trans; subst)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; subst)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Data.Unit using (⊤)
open import Function using (_∘_; flip)
import Chain
open import Utils using (Pairwise; _⇒_; _∨_)
open import Utils using (Pairwise; _⇒_)
import Lattice.FiniteValueMap
open IsFiniteHeightLattice isFiniteHeightLatticeˡ
@ -64,32 +62,25 @@ module WithProg (prog : Program) where
; ⊔-Monotonicʳ to ⊔ᵛ-Monotonicʳ
; ⊔-idemp to ⊔ᵛ-idemp
)
open Lattice.FiniteValueMap.IterProdIsomorphism _≟ˢ_ isLatticeˡ
using ()
renaming
( Provenance-union to Provenance-unionᵐ
)
open Lattice.FiniteValueMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight _≟ˢ_ isLatticeˡ vars-Unique ≈ˡ-dec _ fixedHeightˡ
using ()
renaming
( isFiniteHeightLattice to isFiniteHeightLatticeᵛ
; ⊥-contains-bottoms to ⊥ᵛ-contains-bottoms
)
≈ᵛ-dec = ≈ˡ-dec⇒≈ᵛ-dec ≈ˡ-dec
joinSemilatticeᵛ = IsFiniteHeightLattice.joinSemilattice isFiniteHeightLatticeᵛ
fixedHeightᵛ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵛ
⊥ᵛ = Chain.Height.⊥ fixedHeightᵛ
⊥ᵛ = proj₁ (proj₁ (proj₁ fixedHeightᵛ))
-- Finally, the map we care about is (state -> (variables -> value)). Bring that in.
module StateVariablesFiniteMap = Lattice.FiniteValueMap.WithKeys _≟_ isLatticeᵛ states
open StateVariablesFiniteMap
using (_[_]; []-∈; m₁≼m₂⇒m₁[ks]≼m₂[ks]; m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂)
using (_[_]; m₁≼m₂⇒m₁[ks]≼m₂[ks])
renaming
( FiniteMap to StateVariables
; isLattice to isLatticeᵐ
; _≈_ to _≈ᵐ_
; _∈_ to _∈ᵐ_
; _∈k_ to _∈kᵐ_
; locate to locateᵐ
; _≼_ to _≼ᵐ_
@ -122,13 +113,8 @@ module WithProg (prog : Program) where
variablesAt : State → StateVariables → VariableValues
variablesAt s sv = proj₁ (locateᵐ {s} {sv} (states-in-Map s sv))
variablesAt-∈ : ∀ (s : State) (sv : StateVariables) → (s , variablesAt s sv) ∈ᵐ sv
variablesAt-∈ s sv = proj₂ (locateᵐ {s} {sv} (states-in-Map s sv))
variablesAt-≈ : ∀ s sv₁ sv₂ → sv₁ ≈ᵐ sv₂ → variablesAt s sv₁ ≈ᵛ variablesAt s sv₂
variablesAt-≈ s sv₁ sv₂ sv₁≈sv₂ =
m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ sv₁ sv₂ sv₁≈sv₂
(states-in-Map s sv₁) (states-in-Map s sv₂)
variablesAt-≈ = {!!}
-- build up the 'join' function, which follows from Exercise 4.26's
--
@ -246,17 +232,11 @@ module WithProg (prog : Program) where
module WithInterpretation (latticeInterpretationˡ : LatticeInterpretation isLatticeˡ) where
open LatticeInterpretation latticeInterpretationˡ
using ()
renaming
( ⟦_⟧ to ⟦_⟧ˡ
; ⟦⟧-respects-≈ to ⟦⟧ˡ-respects-≈ˡ
; ⟦⟧-⊔-∨ to ⟦⟧ˡ-⊔ˡ-∨
)
renaming (⟦_⟧ to ⟦_⟧ˡ; ⟦⟧-respects-≈ to ⟦⟧ˡ-respects-≈ˡ)
⟦_⟧ᵛ : VariableValues → Env → Set
⟦_⟧ᵛ vs ρ = ∀ {k l} → (k , l) ∈ᵛ vs → ∀ {v} → (k , v) Language.∈ ρ → ⟦ l ⟧ˡ v
⟦⊥ᵛ⟧ᵛ∅ : ⟦ ⊥ᵛ ⟧ᵛ []
⟦⊥ᵛ⟧ᵛ∅ _ ()
⟦⟧ᵛ-respects-≈ᵛ : ∀ {vs₁ vs₂ : VariableValues} → vs₁ ≈ᵛ vs₂ → ⟦ vs₁ ⟧ᵛ ⇒ ⟦ vs₂ ⟧ᵛ
⟦⟧ᵛ-respects-≈ᵛ {m₁ , _} {m₂ , _}
@ -267,21 +247,9 @@ module WithProg (prog : Program) where
in
⟦⟧ˡ-respects-≈ˡ (≈ˡ-sym l≈l') v ⟦l'⟧v
⟦⟧ᵛ-⊔ᵛ-∨ : ∀ {vs₁ vs₂ : VariableValues} → (⟦ vs₁ ⟧ᵛ ∨ ⟦ vs₂ ⟧ᵛ) ⇒ ⟦ vs₁ ⊔ᵛ vs₂ ⟧ᵛ
⟦⟧ᵛ-⊔ᵛ-∨ {vs₁} {vs₂} ρ ⟦vs₁⟧ρ∨⟦vs₂⟧ρ {k} {l} k,l∈vs₁₂ {v} k,v∈ρ
with ((l₁ , l₂) , (refl , (k,l₁∈vs₁ , k,l₂∈vs₂)))
← Provenance-unionᵐ vs₁ vs₂ k,l∈vs₁₂
with ⟦vs₁⟧ρ∨⟦vs₂⟧ρ
... | inj₁ ⟦vs₁⟧ρ = ⟦⟧ˡ-⊔ˡ-∨ {l₁} {l₂} v (inj₁ (⟦vs₁⟧ρ k,l₁∈vs₁ k,v∈ρ))
... | inj₂ ⟦vs₂⟧ρ = ⟦⟧ˡ-⊔ˡ-∨ {l₁} {l₂} v (inj₂ (⟦vs₂⟧ρ k,l₂∈vs₂ k,v∈ρ))
⟦⟧ᵛ-foldr : ∀ {vs : VariableValues} {vss : List VariableValues} {ρ : Env} →
⟦ vs ⟧ᵛ ρ → vs ∈ˡ vss → ⟦ foldr _⊔ᵛ_ ⊥ᵛ vss ⟧ᵛ ρ
⟦⟧ᵛ-foldr {vs} {vs ∷ vss'} {ρ = ρ} ⟦vs⟧ρ (Any.here refl) =
⟦⟧ᵛ-⊔ᵛ-∨ {vs₁ = vs} {vs₂ = foldr _⊔ᵛ_ ⊥ᵛ vss'} ρ (inj₁ ⟦vs⟧ρ)
⟦⟧ᵛ-foldr {vs} {vs' ∷ vss'} {ρ = ρ} ⟦vs⟧ρ (Any.there vs∈vss') =
⟦⟧ᵛ-⊔ᵛ-∨ {vs₁ = vs'} {vs₂ = foldr _⊔ᵛ_ ⊥ᵛ vss'} ρ
(inj₂ (⟦⟧ᵛ-foldr ⟦vs⟧ρ vs∈vss'))
⟦⟧ᵛ-foldr = {!!}
InterpretationValid : Set
InterpretationValid = ∀ {vs ρ e v} → ρ , e ⇒ᵉ v → ⟦ vs ⟧ᵛ ρ → ⟦ eval e vs ⟧ˡ v
@ -307,17 +275,13 @@ module WithProg (prog : Program) where
updateVariablesFromStmt-fold-matches : ∀ {bss vs ρ₁ ρ₂} → ρ₁ , bss ⇒ᵇˢ ρ₂ → ⟦ vs ⟧ᵛ ρ₁ → ⟦ foldl (flip updateVariablesFromStmt) vs bss ⟧ᵛ ρ₂
updateVariablesFromStmt-fold-matches [] ⟦vs⟧ρ = ⟦vs⟧ρ
updateVariablesFromStmt-fold-matches {bs ∷ bss'} {vs} {ρ₁} {ρ₂} (ρ₁,bs⇒ρ ∷ ρ,bss'⇒ρ₂) ⟦vs⟧ρ₁ =
updateVariablesFromStmt-fold-matches
{bss'} {updateVariablesFromStmt bs vs} ρ,bss'⇒ρ₂
(updateVariablesFromStmt-matches ρ₁,bs⇒ρ ⟦vs⟧ρ₁)
updateVariablesFromStmt-fold-matches {bss'} {updateVariablesFromStmt bs vs} ρ,bss'⇒ρ₂ (updateVariablesFromStmt-matches ρ₁,bs⇒ρ ⟦vs⟧ρ₁)
updateVariablesForState-matches : ∀ {s sv ρ₁ ρ₂} → ρ₁ , (code s) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s sv ⟧ᵛ ρ₁ → ⟦ updateVariablesForState s sv ⟧ᵛ ρ₂
updateVariablesForState-matches =
updateVariablesFromStmt-fold-matches
updateVariablesForState-matches = updateVariablesFromStmt-fold-matches
updateAll-matches : ∀ {s sv ρ₁ ρ₂} → ρ₁ , (code s) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s sv ⟧ᵛ ρ₁ → ⟦ variablesAt s (updateAll sv) ⟧ᵛ ρ₂
updateAll-matches {s} {sv} ρ₁,bss⇒ρ₂ ⟦vs⟧ρ₁
rewrite variablesAt-updateAll s sv =
updateAll-matches {s} {sv} ρ₁,bss⇒ρ₂ ⟦vs⟧ρ₁ rewrite variablesAt-updateAll s sv =
updateVariablesForState-matches {s} {sv} ρ₁,bss⇒ρ₂ ⟦vs⟧ρ₁
@ -325,44 +289,12 @@ module WithProg (prog : Program) where
stepTrace {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ ρ₁,bss⇒ρ₂ =
let
-- I'd use rewrite, but Agda gets a memory overflow (?!).
⟦joinAll-result⟧ρ₁ =
subst (λ vs → ⟦ vs ⟧ᵛ ρ₁)
(sym (variablesAt-joinAll s₁ result))
⟦joinForKey-s₁⟧ρ₁
⟦analyze-result⟧ρ₂ =
updateAll-matches {sv = joinAll result}
ρ₁,bss⇒ρ₂ ⟦joinAll-result⟧ρ₁
analyze-result≈result =
≈ᵐ-sym {result} {updateAll (joinAll result)}
result≈analyze-result
analyze-s₁≈s₁ =
variablesAt-≈ s₁ (updateAll (joinAll result))
result (analyze-result≈result)
⟦joinAll-result⟧ρ₁ = subst (λ vs → ⟦ vs ⟧ᵛ ρ₁) (sym (variablesAt-joinAll s₁ result)) ⟦joinForKey-s₁⟧ρ₁
⟦analyze-result⟧ρ₂ = updateAll-matches {sv = joinAll result} ρ₁,bss⇒ρ₂ ⟦joinAll-result⟧ρ₁
analyze-result≈result = ≈ᵐ-sym {result} {updateAll (joinAll result)} result≈analyze-result
analyze-s₁≈s₁ = variablesAt-≈ s₁ (updateAll (joinAll result)) result (analyze-result≈result)
in
⟦⟧ᵛ-respects-≈ᵛ {variablesAt s₁ (updateAll (joinAll result))} {variablesAt s₁ result} (analyze-s₁≈s₁) ρ₂ ⟦analyze-result⟧ρ₂
walkTrace : ∀ {s₁ s₂ ρ₁ ρ₂} → ⟦ joinForKey s₁ result ⟧ᵛ ρ₁ → Trace {graph} s₁ s₂ ρ₁ ρ₂ → ⟦ variablesAt s₂ result ⟧ᵛ ρ₂
walkTrace {s₁} {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ (Trace-single ρ₁,bss⇒ρ₂) =
stepTrace {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ ρ₁,bss⇒ρ₂
walkTrace {s₁} {s₂} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ (Trace-edge {ρ₂ = ρ} {idx₂ = s} ρ₁,bss⇒ρ s₁→s₂ tr) =
let
⟦result-s₁⟧ρ =
stepTrace {s₁} {ρ₁} {ρ} ⟦joinForKey-s₁⟧ρ₁ ρ₁,bss⇒ρ
s₁∈incomingStates =
[]-∈ result (edge⇒incoming s₁→s₂)
(variablesAt-∈ s₁ result)
⟦joinForKey-s⟧ρ =
⟦⟧ᵛ-foldr ⟦result-s₁⟧ρ s₁∈incomingStates
in
walkTrace ⟦joinForKey-s⟧ρ tr
postulate initialState-pred-∅ : incoming initialState ≡ []
joinForKey-initialState-⊥ᵛ : joinForKey initialState result ≡ ⊥ᵛ
joinForKey-initialState-⊥ᵛ = cong (λ ins → foldr _⊔ᵛ_ ⊥ᵛ (result [ ins ])) initialState-pred-∅
⟦joinAll-initialState⟧ᵛ∅ : ⟦ joinForKey initialState result ⟧ᵛ []
⟦joinAll-initialState⟧ᵛ∅ = subst (λ vs → ⟦ vs ⟧ᵛ []) (sym joinForKey-initialState-⊥ᵛ) ⟦⊥ᵛ⟧ᵛ∅
analyze-correct : ∀ {ρ : Env} → [] , rootStmt ⇒ˢ ρ → ⟦ variablesAt finalState result ⟧ᵛ ρ
analyze-correct {ρ} ∅,s⇒ρ = walkTrace {initialState} {finalState} {[]} {ρ} ⟦joinAll-initialState⟧ᵛ∅ (trace ∅,s⇒ρ)
walkTrace {s₁} {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ (Trace-single ρ₁,bss⇒ρ₂) = stepTrace {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ ρ₁,bss⇒ρ₂

13
Chain.agda
View File

@ -10,7 +10,7 @@ open import Data.Nat using (ℕ; suc; _+_; _≤_)
open import Data.Nat.Properties using (+-comm; m+1+n≰m)
open import Data.Product using (_×_; Σ; _,_)
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
open import Data.Empty as Empty using ()
open import Data.Empty using (⊥)
open IsEquivalence ≈-equiv
@ -38,16 +38,11 @@ module _ where
Bounded : ℕ → Set a
Bounded bound = ∀ {a₁ a₂ : A} {n : ℕ} → Chain a₁ a₂ n → n ≤ bound
Bounded-suc-n : ∀ {a₁ a₂ : A} {n : ℕ} → Bounded n → Chain a₁ a₂ (suc n) → Empty.⊥
Bounded-suc-n : ∀ {a₁ a₂ : A} {n : ℕ} → Bounded n → Chain a₁ a₂ (suc n) → ⊥
Bounded-suc-n {a₁} {a₂} {n} bounded c = (m+1+n≰m n n+1≤n)
where
n+1≤n : n + 1 ≤ n
n+1≤n rewrite (+-comm n 1) = bounded c
record Height (height : ℕ) : Set a where
field
⊥ : A
⊤ : A
longestChain : Chain ⊥ ⊤ height
bounded : Bounded height
Height : ℕ → Set a
Height height = (Σ (A × A) (λ (a₁ , a₂) → Chain a₁ a₂ height) × Bounded height)

16
Fixedpoint.agda
View File

@ -23,21 +23,15 @@ import Chain
module ChainA = Chain _≈_ ≈-equiv _≺_ ≺-cong
private
open ChainA.Height fixedHeight
using ()
renaming
( ⊥ to ⊥ᴬ
; longestChain to longestChainᴬ
; bounded to boundedᴬ
)
⊥ᴬ : A
⊥ᴬ = proj₁ (proj₁ (proj₁ fixedHeight))
⊥ᴬ≼ : ∀ (a : A) → ⊥ᴬ ≼ a
⊥ᴬ≼ a with ≈-dec a ⊥ᴬ
... | yes a≈⊥ᴬ = ≼-cong a≈⊥ᴬ ≈-refl (≼-refl a)
... | no a̷≈⊥ᴬ with ≈-dec ⊥ᴬ (a ⊓ ⊥ᴬ)
... | yes ⊥ᴬ≈a⊓⊥ᴬ = ≈-trans (⊔-comm ⊥ᴬ a) (≈-trans (≈-⊔-cong (≈-refl {a}) ⊥ᴬ≈a⊓⊥ᴬ) (absorb-⊔-⊓ a ⊥ᴬ))
... | no ⊥ᴬ̷≈a⊓⊥ᴬ = ⊥-elim (ChainA.Bounded-suc-n boundedᴬ (ChainA.step x≺⊥ᴬ ≈-refl longestChainᴬ))
... | no ⊥ᴬ̷≈a⊓⊥ᴬ = ⊥-elim (ChainA.Bounded-suc-n (proj₂ fixedHeight) (ChainA.step x≺⊥ᴬ ≈-refl (proj₂ (proj₁ fixedHeight))))
where
⊥ᴬ⊓a̷≈⊥ᴬ : ¬ (⊥ᴬ ⊓ a) ≈ ⊥ᴬ
⊥ᴬ⊓a̷≈⊥ᴬ = λ ⊥ᴬ⊓a≈⊥ᴬ → ⊥ᴬ̷≈a⊓⊥ᴬ (≈-trans (≈-sym ⊥ᴬ⊓a≈⊥ᴬ) (⊓-comm _ _))
@ -51,7 +45,7 @@ private
-- out, we have exceeded h steps, which shouldn't be possible.
doStep : ∀ (g hᶜ : ℕ) (a₁ a₂ : A) (c : ChainA.Chain a₁ a₂ hᶜ) (g+hᶜ≡h : g + hᶜ ≡ suc h) (a₂≼fa₂ : a₂ ≼ f a₂) → Σ A (λ a → a ≈ f a)
doStep 0 hᶜ a₁ a₂ c g+hᶜ≡sh a₂≼fa₂ rewrite g+hᶜ≡sh = ⊥-elim (ChainA.Bounded-suc-n boundedᴬ c)
doStep 0 hᶜ a₁ a₂ c g+hᶜ≡sh a₂≼fa₂ rewrite g+hᶜ≡sh = ⊥-elim (ChainA.Bounded-suc-n (proj₂ fixedHeight) c)
doStep (suc g') hᶜ a₁ a₂ c g+hᶜ≡sh a₂≼fa₂ rewrite sym (+-suc g' hᶜ)
with ≈-dec a₂ (f a₂)
... | yes a₂≈fa₂ = (a₂ , a₂≈fa₂)
@ -77,7 +71,7 @@ private
(c : ChainA.Chain a₁ a₂ hᶜ) (g+hᶜ≡h : g + hᶜ ≡ suc h)
(a₂≼fa₂ : a₂ ≼ f a₂) →
proj₁ (doStep g hᶜ a₁ a₂ c g+hᶜ≡h a₂≼fa₂) ≼ a
stepPreservesLess 0 _ _ _ _ _ _ c g+hᶜ≡sh _ rewrite g+hᶜ≡sh = ⊥-elim (ChainA.Bounded-suc-n boundedᴬ c)
stepPreservesLess 0 _ _ _ _ _ _ c g+hᶜ≡sh _ rewrite g+hᶜ≡sh = ⊥-elim (ChainA.Bounded-suc-n (proj₂ fixedHeight) c)
stepPreservesLess (suc g') hᶜ a₁ a₂ a a≈fa a₂≼a c g+hᶜ≡sh a₂≼fa₂ rewrite sym (+-suc g' hᶜ)
with ≈-dec a₂ (f a₂)
... | yes _ = a₂≼a

16
Isomorphism.agda
View File

@ -38,9 +38,8 @@ module TransportFiniteHeight
open IsEquivalence ≈₁-equiv using () renaming (≈-sym to ≈₁-sym; ≈-trans to ≈₁-trans)
open IsEquivalence ≈₂-equiv using () renaming (≈-sym to ≈₂-sym; ≈-trans to ≈₂-trans)
import Chain
open Chain _≈₁_ ≈₁-equiv _≺₁_ ≺₁-cong using () renaming (Chain to Chain₁; done to done₁; step to step₁)
open Chain _≈₂_ ≈₂-equiv _≺₂_ ≺₂-cong using () renaming (Chain to Chain₂; done to done₂; step to step₂)
open import Chain _≈₁_ ≈₁-equiv _≺₁_ ≺₁-cong using () renaming (Chain to Chain₁; done to done₁; step to step₁)
open import Chain _≈₂_ ≈₂-equiv _≺₂_ ≺₂-cong using () renaming (Chain to Chain₂; done to done₂; step to step₂)
private
f-Injective : Injective _≈₁_ _≈₂_ f
@ -66,17 +65,10 @@ module TransportFiniteHeight
isFiniteHeightLattice : IsFiniteHeightLattice B height _≈₂_ _⊔₂_ _⊓₂_
isFiniteHeightLattice =
let
open Chain.Height (IsFiniteHeightLattice.fixedHeight fhlA)
using ()
renaming (⊥ to ⊥₁; ⊤ to ⊤₁; bounded to bounded₁; longestChain to c)
(((a₁ , a₂) , c) , bounded₁) = IsFiniteHeightLattice.fixedHeight fhlA
in record
{ isLattice = lB
; fixedHeight = record
{ ⊥ = f ⊥₁
; ⊤ = f ⊤₁
; longestChain = portChain₁ c
; bounded = λ c' → bounded₁ (portChain₂ c')
}
; fixedHeight = (((f a₁ , f a₂), portChain₁ c) , λ c' → bounded₁ (portChain₂ c'))
}
finiteHeightLattice : FiniteHeightLattice B

49
Language.agda
View File

@ -10,7 +10,7 @@ open import Data.Fin using (Fin; suc; zero)
open import Data.Fin.Properties as FinProp using (suc-injective)
open import Data.List as List using (List; []; _∷_)
open import Data.List.Membership.Propositional as ListMem using ()
open import Data.List.Membership.Propositional.Properties as ListMemProp using (∈-filter⁺)
open import Data.List.Relation.Unary.All using (All; []; _∷_)
open import Data.List.Relation.Unary.Any as RelAny using ()
open import Data.Nat using (ℕ; suc)
open import Data.Product using (_,_; Σ; proj₁; proj₂)
@ -27,26 +27,43 @@ open import Lattice.MapSet _≟ˢ_ using ()
; to-List to to-Listˢ
)
private
z≢sf : ∀ {n : ℕ} (f : Fin n) → ¬ (zero ≡ suc f)
z≢sf f ()
z≢mapsfs : ∀ {n : ℕ} (fs : List (Fin n)) → All (λ sf → ¬ zero ≡ sf) (List.map suc fs)
z≢mapsfs [] = []
z≢mapsfs (f ∷ fs') = z≢sf f ∷ z≢mapsfs fs'
indices : ∀ (n : ℕ) → Σ (List (Fin n)) Unique
indices 0 = ([] , Utils.empty)
indices (suc n') =
let
(inds' , unids') = indices n'
in
( zero ∷ List.map suc inds'
, push (z≢mapsfs inds') (Unique-map suc suc-injective unids')
)
indices-complete : ∀ (n : ℕ) (f : Fin n) → f ListMem.∈ (proj₁ (indices n))
indices-complete (suc n') zero = RelAny.here refl
indices-complete (suc n') (suc f') = RelAny.there (x∈xs⇒fx∈fxs suc (indices-complete n' f'))
record Program : Set where
field
rootStmt : Stmt
graph : Graph
graph = wrap (buildCfg rootStmt)
graph = buildCfg rootStmt
State : Set
State = Graph.Index graph
initialState : State
initialState = proj₁ (wrap-input (buildCfg rootStmt))
initialState = proj₁ (buildCfg-input rootStmt)
finalState : State
finalState = proj₁ (wrap-output (buildCfg rootStmt))
trace : ∀ {ρ : Env} → [] , rootStmt ⇒ˢ ρ → Trace {graph} initialState finalState [] ρ
trace {ρ} ∅,s⇒ρ
with MkEndToEndTrace idx₁ (RelAny.here refl) idx₂ (RelAny.here refl) tr
← EndToEndTrace-wrap (buildCfg-sufficient ∅,s⇒ρ) = tr
finalState = proj₁ (buildCfg-output rootStmt)
private
vars-Set : StringSet
@ -59,13 +76,13 @@ record Program : Set where
vars-Unique = proj₂ vars-Set
states : List State
states = indices graph
states = proj₁ (indices (Graph.size graph))
states-complete : ∀ (s : State) → s ListMem.∈ states
states-complete = indices-complete graph
states-complete = indices-complete (Graph.size graph)
states-Unique : Unique states
states-Unique = indices-Unique graph
states-Unique = proj₂ (indices (Graph.size graph))
code : State → List BasicStmt
code st = graph [ st ]
@ -82,10 +99,4 @@ record Program : Set where
open import Data.List.Membership.DecPropositional _≟ᵉ_ using (_∈?_)
incoming : State → List State
incoming = predecessors graph
edge⇒incoming : ∀ {s₁ s₂ : State} → (s₁ , s₂) ListMem.∈ (Graph.edges graph) →
s₁ ListMem.∈ (incoming s₂)
edge⇒incoming {s₁} {s₂} s₁,s₂∈es =
∈-filter⁺ (λ s' → (s' , s₂) ∈? (Graph.edges graph))
(states-complete s₁) s₁,s₂∈es
incoming idx = List.filter (λ idx' → (idx' , idx) ∈? (Graph.edges graph)) states

48
Language/Graphs.agda
View File

@ -7,19 +7,15 @@ open import Data.Fin.Properties as FinProp using (suc-injective)
open import Data.List as List using (List; []; _∷_)
open import Data.List.Membership.Propositional as ListMem using ()
open import Data.List.Membership.Propositional.Properties as ListMemProp using ()
open import Data.List.Relation.Unary.All using (All; []; _∷_)
open import Data.List.Relation.Unary.Any as RelAny using ()
open import Data.Nat as Nat using (ℕ; suc)
open import Data.Nat.Properties using (+-assoc; +-comm)
open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
open import Data.Product.Properties as ProdProp using ()
open import Data.Product using (_×_; Σ; _,_)
open import Data.Vec using (Vec; []; _∷_; lookup; cast; _++_)
open import Data.Vec.Properties using (cast-is-id; ++-assoc; lookup-++ˡ; cast-sym; ++-identityʳ; lookup-++ʳ)
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; refl; subst; trans)
open import Relation.Nullary using (¬_)
open import Lattice
open import Utils using (Unique; push; Unique-map; x∈xs⇒fx∈fxs; ∈-cartesianProduct)
open import Utils using (x∈xs⇒fx∈fxs; ∈-cartesianProduct)
record Graph : Set where
constructor MkGraph
@ -116,48 +112,8 @@ singleton bss = record
; outputs = zero ∷ []
}
wrap : Graph → Graph
wrap g = singleton [] ↦ g ↦ singleton []
buildCfg : Stmt → Graph
buildCfg ⟨ bs₁ ⟩ = singleton (bs₁ ∷ [])
buildCfg (s₁ then s₂) = buildCfg s₁ ↦ buildCfg s₂
buildCfg (if _ then s₁ else s₂) = singleton [] ↦ (buildCfg s₁ ∙ buildCfg s₂) ↦ singleton []
buildCfg (while _ repeat s) = loop (buildCfg s)
private
z≢sf : ∀ {n : ℕ} (f : Fin n) → ¬ (zero ≡ suc f)
z≢sf f ()
z≢mapsfs : ∀ {n : ℕ} (fs : List (Fin n)) → All (λ sf → ¬ zero ≡ sf) (List.map suc fs)
z≢mapsfs [] = []
z≢mapsfs (f ∷ fs') = z≢sf f ∷ z≢mapsfs fs'
finValues : ∀ (n : ℕ) → Σ (List (Fin n)) Unique
finValues 0 = ([] , Utils.empty)
finValues (suc n') =
let
(inds' , unids') = finValues n'
in
( zero ∷ List.map suc inds'
, push (z≢mapsfs inds') (Unique-map suc suc-injective unids')
)
finValues-complete : ∀ (n : ℕ) (f : Fin n) → f ListMem.∈ (proj₁ (finValues n))
finValues-complete (suc n') zero = RelAny.here refl
finValues-complete (suc n') (suc f') = RelAny.there (x∈xs⇒fx∈fxs suc (finValues-complete n' f'))
module _ (g : Graph) where
open import Data.List.Membership.DecPropositional (ProdProp.≡-dec (FinProp._≟_ {Graph.size g}) (FinProp._≟_ {Graph.size g})) using (_∈?_)
indices : List (Graph.Index g)
indices = proj₁ (finValues (Graph.size g))
indices-complete : ∀ (idx : (Graph.Index g)) → idx ListMem.∈ indices
indices-complete = finValues-complete (Graph.size g)
indices-Unique : Unique indices
indices-Unique = proj₂ (finValues (Graph.size g))
predecessors : (Graph.Index g) → List (Graph.Index g)
predecessors idx = List.filter (λ idx' → (idx' , idx) ∈? (Graph.edges g)) indices

23
Language/Properties.agda
View File

@ -18,11 +18,22 @@ open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym)
open import Utils using (x∈xs⇒fx∈fxs; ∈-cartesianProduct; concat-∈)
wrap-input : ∀ (g : Graph) → Σ (Graph.Index (wrap g)) (λ idx → Graph.inputs (wrap g) ≡ idx ∷ [])
wrap-input g = (_ , refl)
wrap-output : ∀ (g : Graph) → Σ (Graph.Index (wrap g)) (λ idx → Graph.outputs (wrap g) ≡ idx ∷ [])
wrap-output g = (_ , refl)
buildCfg-input : ∀ (s : Stmt) → let g = buildCfg s in Σ (Graph.Index g) (λ idx → Graph.inputs g ≡ idx ∷ [])
buildCfg-input ⟨ bs₁ ⟩ = (zero , refl)
buildCfg-input (s₁ then s₂)
with (idx , p) ← buildCfg-input s₁ rewrite p = (_ , refl)
buildCfg-input (if _ then s₁ else s₂) = (zero , refl)
buildCfg-input (while _ repeat s)
with (idx , p) ← buildCfg-input s rewrite p = (_ , refl)
buildCfg-output : ∀ (s : Stmt) → let g = buildCfg s in Σ (Graph.Index g) (λ idx → Graph.outputs g ≡ idx ∷ [])
buildCfg-output ⟨ bs₁ ⟩ = (zero , refl)
buildCfg-output (s₁ then s₂)
with (idx , p) ← buildCfg-output s₂ rewrite p = (_ , refl)
buildCfg-output (if _ then s₁ else s₂) = (_ , refl)
buildCfg-output (while _ repeat s)
with (idx , p) ← buildCfg-output s rewrite p = (_ , refl)
Trace-∙ˡ : ∀ {g₁ g₂ : Graph} {idx₁ idx₂ : Graph.Index g₁} {ρ₁ ρ₂ : Env} →
Trace {g₁} idx₁ idx₂ ρ₁ ρ₂ →
@ -213,10 +224,6 @@ EndToEndTrace-singleton ρ₁⇒ρ₂ = record
EndToEndTrace-singleton[] : ∀ (ρ : Env) → EndToEndTrace {singleton []} ρ ρ
EndToEndTrace-singleton[] env = EndToEndTrace-singleton []
EndToEndTrace-wrap : ∀ {g : Graph} {ρ₁ ρ₂ : Env} →
EndToEndTrace {g} ρ₁ ρ₂ → EndToEndTrace {wrap g} ρ₁ ρ₂
EndToEndTrace-wrap {g} {ρ₁} {ρ₂} etr = EndToEndTrace-singleton[] ρ₁ ++ etr ++ EndToEndTrace-singleton[] ρ₂
buildCfg-sufficient : ∀ {s : Stmt} {ρ₁ ρ₂ : Env} → ρ₁ , s ⇒ˢ ρ₂ →
EndToEndTrace {buildCfg s} ρ₁ ρ₂
buildCfg-sufficient (⇒ˢ-⟨⟩ ρ₁ ρ₂ bs ρ₁,bs⇒ρ₂) =

7
Lattice/AboveBelow.agda
View File

@ -355,12 +355,7 @@ module Plain (x : A) where
rewrite [x]≺y⇒y≡⊤ _ _ [x]≺y with ≈-⊤-⊤ ← y≈z = ⊥-elim (¬-Chain-⊤ c)
fixedHeight : IsLattice.FixedHeight isLattice 2
fixedHeight = record
{ ⊥ = ⊥
; ⊤ = ⊤
; longestChain = longestChain
; bounded = isLongest
}
fixedHeight = (((⊥ , ⊤) , longestChain) , isLongest)
isFiniteHeightLattice : IsFiniteHeightLattice AboveBelow 2 _≈_ _⊔_ _⊓_
isFiniteHeightLattice = record

11
Lattice/FiniteMap.agda
View File

@ -30,9 +30,7 @@ open import Lattice.Map ≡-dec-A lB as Map
; absorb-⊓-⊔ to absorb-⊓ᵐ-⊔ᵐ
; ≈-dec to ≈ᵐ-dec
; _[_] to _[_]ᵐ
; []-∈ to []ᵐ-∈
; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ
; m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ to m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ᵐ
; locate to locateᵐ
; keys to keysᵐ
; _updating_via_ to _updatingᵐ_via_
@ -106,10 +104,6 @@ module WithKeys (ks : List A) where
_[_] : FiniteMap → List A → List B
_[_] (m₁ , _) ks = m₁ [ ks ]ᵐ
[]-∈ : ∀ {k : A} {v : B} {ks' : List A} (fm : FiniteMap) →
k ∈ˡ ks' → (k , v) ∈ fm → v ∈ˡ (fm [ ks' ])
[]-∈ {k} {v} {ks'} (m , _) k∈ks' k,v∈fm = []ᵐ-∈ m k,v∈fm k∈ks'
≈-equiv : IsEquivalence FiniteMap _≈_
≈-equiv = record
{ ≈-refl =
@ -165,11 +159,6 @@ module WithKeys (ks : List A) where
fm₁ ≼ fm₂ → (k , v₁) ∈ fm₁ → (k , v₂) ∈ fm₂ → v₁ ≼₂ v₂
m₁≼m₂⇒m₁[k]≼m₂[k] (m₁ , _) (m₂ , _) m₁≼m₂ k,v₁∈m₁ k,v₂∈m₂ = m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ m₁ m₂ m₁≼m₂ k,v₁∈m₁ k,v₂∈m₂
m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ : ∀ (fm₁ fm₂ : FiniteMap) {k : A} →
fm₁ ≈ fm₂ → ∀ (k∈kfm₁ : k ∈k fm₁) (k∈kfm₂ : k ∈k fm₂) →
proj₁ (locate {fm = fm₁} k∈kfm₁) ≈₂ proj₁ (locate {fm = fm₂} k∈kfm₂)
m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ (m₁ , _) (m₂ , _) = m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ᵐ m₁ m₂
module GeneralizedUpdate
{l} {L : Set l}
{_≈ˡ_ : L → L → Set l} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L}

58
Lattice/FiniteValueMap.agda
View File

@ -28,7 +28,6 @@ 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
@ -105,14 +104,6 @@ module IterProdIsomorphism where
_∈ᵐ_ : ∀ {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})
@ -162,26 +153,6 @@ module IterProdIsomorphism where
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)
@ -233,6 +204,26 @@ module IterProdIsomorphism where
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'
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₂)))
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₂ , _) =
@ -416,12 +407,3 @@ module IterProdIsomorphism where
(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∈⊥

65
Lattice/IterProd.agda
View File

@ -11,11 +11,9 @@ module Lattice.IterProd {a} {A B : Set a}
(lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
open import Agda.Primitive using (lsuc)
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; cong)
open import Data.Nat using (ℕ; suc; _+_)
open import Data.Product using (_×_)
open import Utils using (iterate)
open import Chain using (Height)
open IsLattice lA renaming (FixedHeight to FixedHeight₁)
open IsLattice lB renaming (FixedHeight to FixedHeight₂)
@ -32,10 +30,6 @@ IterProd k = iterate k (λ t → A × t) B
-- that are built up by the two iterations. So, do everything in one iteration.
-- This requires some odd code.
build : A → B → (k : ℕ) → IterProd k
build _ b zero = b
build a b (suc s) = (a , build a b s)
private
record RequiredForFixedHeight : Set (lsuc a) where
field
@ -45,37 +39,22 @@ private
fhA : FixedHeight₁ h₁
fhB : FixedHeight₂ h₂
⊥₁ : A
⊥₁ = Height.⊥ fhA
⊥₂ : B
⊥₂ = Height.⊥ fhB
⊥k : ∀ (k : ℕ) → IterProd k
⊥k = build ⊥₁ ⊥₂
record IsFiniteHeightWithBotAndDecEq {A : Set a} {_≈_ : A → A → Set a} {_⊔_ : A → A → A} {_⊓_ : A → A → A} (isLattice : IsLattice A _≈_ _⊔_ _⊓_) (⊥ : A) : Set (lsuc a) where
record IsFiniteHeightAndDecEq {A : Set a} {_≈_ : A → A → Set a} {_⊔_ : A → A → A} {_⊓_ : A → A → A} (isLattice : IsLattice A _≈_ _⊔_ _⊓_) : Set (lsuc a) where
field
height : ℕ
fixedHeight : IsLattice.FixedHeight isLattice height
≈-dec : IsDecidable _≈_
⊥-correct : Height.⊥ fixedHeight ≡ ⊥
record Everything (k : ℕ) : Set (lsuc a) where
T = IterProd k
record Everything (A : Set a) : Set (lsuc a) where
field
_≈_ : T → T → Set a
_⊔_ : T → T → T
_⊓_ : T → T → T
_≈_ : A → A → Set a
_⊔_ : A → A → A
_⊓_ : A → A → A
isLattice : IsLattice T _≈_ _⊔_ _⊓_
isFiniteHeightIfSupported :
∀ (req : RequiredForFixedHeight) →
IsFiniteHeightWithBotAndDecEq isLattice (RequiredForFixedHeight.⊥k req k)
isLattice : IsLattice A _≈_ _⊔_ _⊓_
isFiniteHeightIfSupported : RequiredForFixedHeight → IsFiniteHeightAndDecEq isLattice
everything : ∀ (k : ℕ) → Everything k
everything : ∀ (k : ℕ) → Everything (IterProd k)
everything 0 = record
{ _≈_ = _≈₂_
; _⊔_ = _⊔₂_
@ -85,7 +64,6 @@ private
{ height = RequiredForFixedHeight.h₂ req
; fixedHeight = RequiredForFixedHeight.fhB req
; ≈-dec = RequiredForFixedHeight.≈₂-dec req
; ⊥-correct = refl
}
}
everything (suc k') = record
@ -98,16 +76,13 @@ private
fhlRest = Everything.isFiniteHeightIfSupported everythingRest req
in
record
{ height = (RequiredForFixedHeight.h₁ req) + IsFiniteHeightWithBotAndDecEq.height fhlRest
{ height = (RequiredForFixedHeight.h₁ req) + IsFiniteHeightAndDecEq.height fhlRest
; fixedHeight =
P.fixedHeight
(RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightWithBotAndDecEq.≈-dec fhlRest)
(RequiredForFixedHeight.h₁ req) (IsFiniteHeightWithBotAndDecEq.height fhlRest)
(RequiredForFixedHeight.fhA req) (IsFiniteHeightWithBotAndDecEq.fixedHeight fhlRest)
; ≈-dec = P.≈-dec (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightWithBotAndDecEq.≈-dec fhlRest)
; ⊥-correct =
cong ((Height.⊥ (RequiredForFixedHeight.fhA req)) ,_)
(IsFiniteHeightWithBotAndDecEq.⊥-correct fhlRest)
(RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightAndDecEq.≈-dec fhlRest)
(RequiredForFixedHeight.h₁ req) (IsFiniteHeightAndDecEq.height fhlRest)
(RequiredForFixedHeight.fhA req) (IsFiniteHeightAndDecEq.fixedHeight fhlRest)
; ≈-dec = P.≈-dec (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightAndDecEq.≈-dec fhlRest)
}
}
where
@ -146,22 +121,16 @@ module _ (k : ℕ) where
; fhB = fhB
}
fixedHeight = IsFiniteHeightWithBotAndDecEq.fixedHeight (Everything.isFiniteHeightIfSupported (everything k) required)
isFiniteHeightLattice = record
{ isLattice = isLattice
; fixedHeight = fixedHeight
; fixedHeight = IsFiniteHeightAndDecEq.fixedHeight (Everything.isFiniteHeightIfSupported (everything k) required)
}
finiteHeightLattice : FiniteHeightLattice (IterProd k)
finiteHeightLattice = record
{ height = IsFiniteHeightWithBotAndDecEq.height (Everything.isFiniteHeightIfSupported (everything k) required)
{ height = IsFiniteHeightAndDecEq.height (Everything.isFiniteHeightIfSupported (everything k) required)
; _≈_ = _≈_
; _⊔_ = _⊔_
; _⊓_ = _⊓_
; isFiniteHeightLattice = isFiniteHeightLattice
}
⊥-built : Height.⊥ fixedHeight ≡ (build (Height.⊥ fhA) (Height.⊥ fhB) k)
⊥-built = IsFiniteHeightWithBotAndDecEq.⊥-correct (Everything.isFiniteHeightIfSupported (everything k) required)

22
Lattice/Map.agda
View File

@ -1112,19 +1112,6 @@ _[_] m (k ∷ ks)
... | yes k∈km = proj₁ (locate {m = m} k∈km) ∷ (m [ ks ])
... | no _ = m [ ks ]
[]-∈ : ∀ {k : A} {v : B} {ks : List A} (m : Map) →
(k , v) ∈ m → k ∈ˡ ks → v ∈ˡ (m [ ks ])
[]-∈ {k} {v} {ks} m k,v∈m (here refl)
with ∈k-dec k (proj₁ m)
... | no k∉km = ⊥-elim (k∉km (forget k,v∈m))
... | yes k∈km
with (v' , k,v'∈m) ← locate {m = m} k∈km
rewrite Map-functional {m = m} k,v'∈m k,v∈m = here refl
[]-∈ {k} {v} {k' ∷ ks'} m k,v∈m (there k∈ks')
with ∈k-dec k' (proj₁ m)
... | no _ = []-∈ m k,v∈m k∈ks'
... | yes _ = there ([]-∈ m k,v∈m k∈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₂
@ -1142,12 +1129,3 @@ m₁≼m₂⇒k∈km₁⇒k∈km₂ m₁ m₂ m₁≼m₂ k∈km₁ =
(v' , (v≈v' , k,v'∈m₂)) = (proj₁ m₁≼m₂) _ _ k,v∈m₁m₂
in
forget k,v'∈m₂
m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ : ∀ (m₁ m₂ : Map) {k : A} →
m₁ ≈ m₂ → ∀ (k∈km₁ : k ∈k m₁) (k∈km₂ : k ∈k m₂) →
proj₁ (locate {m = m₁} k∈km₁) ≈₂ proj₁ (locate {m = m₂} k∈km₂)
m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ m₁ m₂ {k} (m₁⊆m₂ , m₂⊆m₁) k∈km₁ k∈km₂
with (v₁ , k,v₁∈m₁) ← locate {m = m₁} k∈km₁
with (v₂ , k,v₂∈m₂) ← locate {m = m₂} k∈km₂
with (v₂' , (v₁≈v₂' , k,v₂'∈m₂)) ← m₁⊆m₂ k v₁ k,v₁∈m₁
rewrite Map-functional {m = m₂} k,v₂∈m₂ k,v₂'∈m₂ = v₁≈v₂'

32
Lattice/Prod.agda
View File

@ -143,8 +143,17 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
∙,b-Preserves-≈₁ : ∀ (b : B) → (λ a → (a , b)) Preserves _≈₁_ ⟶ _≈_
∙,b-Preserves-≈₁ b {a₁} {a₂} a₁≈a₂ = (a₁≈a₂ , ≈₂-refl)
open ChainA.Height fhA using () renaming (⊥ to ⊥₁; ⊤ to ⊤₁; longestChain to longestChain₁; bounded to bounded₁)
open ChainB.Height fhB using () renaming (⊥ to ⊥₂; ⊤ to ⊤₂; longestChain to longestChain₂; bounded to bounded₂)
amin : A
amin = proj₁ (proj₁ (proj₁ fhA))
amax : A
amax = proj₂ (proj₁ (proj₁ fhA))
bmin : B
bmin = proj₁ (proj₁ (proj₁ fhB))
bmax : B
bmax = proj₂ (proj₁ (proj₁ fhB))
unzip : ∀ {a₁ a₂ : A} {b₁ b₂ : B} {n : ℕ} → Chain (a₁ , b₁) (a₂ , b₂) n → Σ (ℕ × ℕ) (λ (n₁ , n₂) → ((Chain₁ a₁ a₂ n₁ × Chain₂ b₁ b₂ n₂) × (n ≤ n₁ + n₂)))
unzip (done (a₁≈a₂ , b₁≈b₂)) = ((0 , 0) , ((done₁ a₁≈a₂ , done₂ b₁≈b₂) , ≤-refl))
@ -163,16 +172,15 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
))
fixedHeight : IsLattice.FixedHeight isLattice (h₁ + h₂)
fixedHeight = record
{ ⊥ = (⊥₁ , ⊥₂)
; ⊤ = (⊤₁ , ⊤₂)
; longestChain = concat
(ChainMapping₁.Chain-map (λ a → (a , ⊥₂)) (∙,b-Monotonic _) proj₁ (∙,b-Preserves-≈₁ _) longestChain₁)
(ChainMapping₂.Chain-map (λ b → (⊤₁ , b)) (a,∙-Monotonic _) proj₂ (a,∙-Preserves-≈₂ _) longestChain₂)
; bounded = λ a₁b₁a₂b₂ →
let ((n₁ , n₂) , ((a₁a₂ , b₁b₂) , n≤n₁+n₂)) = unzip a₁b₁a₂b₂
in ≤-trans n≤n₁+n₂ (+-mono-≤ (bounded₁ a₁a₂) (bounded₂ b₁b₂))
}
fixedHeight =
( ( ((amin , bmin) , (amax , bmax))
, concat
(ChainMapping₁.Chain-map (λ a → (a , bmin)) (∙,b-Monotonic _) proj₁ (∙,b-Preserves-≈₁ _) (proj₂ (proj₁ fhA)))
(ChainMapping₂.Chain-map (λ b → (amax , b)) (a,∙-Monotonic _) proj₂ (a,∙-Preserves-≈₂ _) (proj₂ (proj₁ fhB)))
)
, λ a₁b₁a₂b₂ → let ((n₁ , n₂) , ((a₁a₂ , b₁b₂) , n≤n₁+n₂)) = unzip a₁b₁a₂b₂
in ≤-trans n≤n₁+n₂ (+-mono-≤ (proj₂ fhA a₁a₂) (proj₂ fhB b₁b₂))
)
isFiniteHeightLattice : IsFiniteHeightLattice (A × B) (h₁ + h₂) _≈_ _⊔_ _⊓_
isFiniteHeightLattice = record

7
Lattice/Unit.agda
View File

@ -108,12 +108,7 @@ private
isLongest (done _) = z≤n
fixedHeight : IsLattice.FixedHeight isLattice 0
fixedHeight = record
{ ⊥ = tt
; ⊤ = tt
; longestChain = longestChain
; bounded = isLongest
}
fixedHeight = (((tt , tt) , longestChain) , isLongest)
isFiniteHeightLattice : IsFiniteHeightLattice ⊤ 0 _≈_ _⊔_ _⊓_
isFiniteHeightLattice = record