From 1a7b2a1736bc8a4e34058742f5d7880329b335f1 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Fri, 22 Mar 2024 17:15:40 -0700 Subject: [PATCH] Adjust behavior of eval to not require constant 'k in vars' threading Signed-off-by: Danila Fedorin --- Analysis/Sign.agda | 101 ++++++++++++++++++++--------------------- Lattice/FiniteMap.agda | 7 ++- 2 files changed, 54 insertions(+), 54 deletions(-) diff --git a/Analysis/Sign.agda b/Analysis/Sign.agda index f267c4c..3ebdee6 100644 --- a/Analysis/Sign.agda +++ b/Analysis/Sign.agda @@ -3,6 +3,7 @@ module Analysis.Sign where open import Data.String using (String) renaming (_≟_ to _≟ˢ_) open import Data.Nat using (suc) open import Data.Product using (_×_; proj₁; _,_) +open import Data.Empty using (⊥; ⊥-elim) open import Data.List using (List; _∷_; []; foldr; cartesianProduct; cartesianProductWith) open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_) open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; subst) @@ -61,8 +62,7 @@ open import Lattice.AboveBelow Sign _≡_ (record { ≈-refl = refl; ≈-sym = s -- 'sign' has no underlying lattice structure, so use the 'plain' above-below lattice. open AB.Plain 0ˢ using () renaming - ( finiteHeightLattice to finiteHeightLatticeᵍ - ; isLattice to isLatticeᵍ + ( isLattice to isLatticeᵍ ; fixedHeight to fixedHeightᵍ ; _≼_ to _≼ᵍ_ ; _⊔_ to _⊔ᵍ_ @@ -130,6 +130,8 @@ module WithProg (prog : Program) where ; _updating_via_ to _updatingᵛ_via_ ; locate to locateᵛ ; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵛ≼m₂[k]ᵛ + ; all-equal-keys to all-equal-keysᵛ + ; ∈k-dec to ∈k-decᵛ ) open IsLattice isLatticeᵛ using () @@ -206,57 +208,57 @@ module WithProg (prog : Program) where states-in-Map : ∀ (s : State) (sv : StateVariables) → s ∈kᵐ sv states-in-Map s sv@(m , ksv≡states) rewrite ksv≡states = states-complete s - eval : ∀ (e : Expr) → (∀ k → k ∈ᵉ e → k ∈ˡ vars) → VariableSigns → SignLattice - eval (e₁ + e₂) k∈e⇒k∈vars vs = - plus (eval e₁ (λ k k∈e₁ → k∈e⇒k∈vars k (in⁺₁ k∈e₁)) vs) - (eval e₂ (λ k k∈e₂ → k∈e⇒k∈vars k (in⁺₂ k∈e₂)) vs) - eval (e₁ - e₂) k∈e⇒k∈vars vs = - minus (eval e₁ (λ k k∈e₁ → k∈e⇒k∈vars k (in⁻₁ k∈e₁)) vs) - (eval e₂ (λ k k∈e₂ → k∈e⇒k∈vars k (in⁻₂ k∈e₂)) vs) - eval (` k) k∈e⇒k∈vars vs = proj₁ (locateᵛ {k} {vs} (vars-in-Map k vs (k∈e⇒k∈vars k here))) - eval (# 0) _ _ = [ 0ˢ ]ᵍ - eval (# (suc n')) _ _ = [ + ]ᵍ + eval : ∀ (e : Expr) → VariableSigns → SignLattice + eval (e₁ + e₂) vs = plus (eval e₁ vs) (eval e₂ vs) + eval (e₁ - e₂) vs = minus (eval e₁ vs) (eval e₂ vs) + eval (` k) vs + with ∈k-decᵛ k (proj₁ (proj₁ vs)) + ... | yes k∈vs = proj₁ (locateᵛ {k} {vs} k∈vs) + ... | no _ = ⊤ᵍ + eval (# 0) _ = [ 0ˢ ]ᵍ + eval (# (suc n')) _ = [ + ]ᵍ - eval-Mono : ∀ (e : Expr) (k∈e⇒k∈vars : ∀ k → k ∈ᵉ e → k ∈ˡ vars) → Monotonic _≼ᵛ_ _≼ᵍ_ (eval e k∈e⇒k∈vars) - eval-Mono (e₁ + e₂) k∈e⇒k∈vars {vs₁} {vs₂} vs₁≼vs₂ = + eval-Mono : ∀ (e : Expr) → Monotonic _≼ᵛ_ _≼ᵍ_ (eval e) + eval-Mono (e₁ + e₂) {vs₁} {vs₂} vs₁≼vs₂ = let -- TODO: can this be done with less boilerplate? - k∈e₁⇒k∈vars = λ k k∈e₁ → k∈e⇒k∈vars k (in⁺₁ k∈e₁) - k∈e₂⇒k∈vars = λ k k∈e₂ → k∈e⇒k∈vars k (in⁺₂ k∈e₂) - g₁vs₁ = eval e₁ k∈e₁⇒k∈vars vs₁ - g₂vs₁ = eval e₂ k∈e₂⇒k∈vars vs₁ - g₁vs₂ = eval e₁ k∈e₁⇒k∈vars vs₂ - g₂vs₂ = eval e₂ k∈e₂⇒k∈vars vs₂ + g₁vs₁ = eval e₁ vs₁ + g₂vs₁ = eval e₂ vs₁ + g₁vs₂ = eval e₁ vs₂ + g₂vs₂ = eval e₂ vs₂ in ≼ᵍ-trans {plus g₁vs₁ g₂vs₁} {plus g₁vs₂ g₂vs₁} {plus g₁vs₂ g₂vs₂} - (plus-Monoˡ g₂vs₁ {g₁vs₁} {g₁vs₂} (eval-Mono e₁ k∈e₁⇒k∈vars {vs₁} {vs₂} vs₁≼vs₂)) - (plus-Monoʳ g₁vs₂ {g₂vs₁} {g₂vs₂} (eval-Mono e₂ k∈e₂⇒k∈vars {vs₁} {vs₂} vs₁≼vs₂)) - eval-Mono (e₁ - e₂) k∈e⇒k∈vars {vs₁} {vs₂} vs₁≼vs₂ = + (plus-Monoˡ g₂vs₁ {g₁vs₁} {g₁vs₂} (eval-Mono e₁ {vs₁} {vs₂} vs₁≼vs₂)) + (plus-Monoʳ g₁vs₂ {g₂vs₁} {g₂vs₂} (eval-Mono e₂ {vs₁} {vs₂} vs₁≼vs₂)) + eval-Mono (e₁ - e₂) {vs₁} {vs₂} vs₁≼vs₂ = let -- TODO: here too -- can this be done with less boilerplate? - k∈e₁⇒k∈vars = λ k k∈e₁ → k∈e⇒k∈vars k (in⁻₁ k∈e₁) - k∈e₂⇒k∈vars = λ k k∈e₂ → k∈e⇒k∈vars k (in⁻₂ k∈e₂) - g₁vs₁ = eval e₁ k∈e₁⇒k∈vars vs₁ - g₂vs₁ = eval e₂ k∈e₂⇒k∈vars vs₁ - g₁vs₂ = eval e₁ k∈e₁⇒k∈vars vs₂ - g₂vs₂ = eval e₂ k∈e₂⇒k∈vars vs₂ + g₁vs₁ = eval e₁ vs₁ + g₂vs₁ = eval e₂ vs₁ + g₁vs₂ = eval e₁ vs₂ + g₂vs₂ = eval e₂ vs₂ in ≼ᵍ-trans {minus g₁vs₁ g₂vs₁} {minus g₁vs₂ g₂vs₁} {minus g₁vs₂ g₂vs₂} - (minus-Monoˡ g₂vs₁ {g₁vs₁} {g₁vs₂} (eval-Mono e₁ k∈e₁⇒k∈vars {vs₁} {vs₂} vs₁≼vs₂)) - (minus-Monoʳ g₁vs₂ {g₂vs₁} {g₂vs₂} (eval-Mono e₂ k∈e₂⇒k∈vars {vs₁} {vs₂} vs₁≼vs₂)) - eval-Mono (` k) k∈e⇒k∈vars {vs₁} {vs₂} vs₁≼vs₂ = - let - (v₁ , k,v₁∈vs₁) = locateᵛ {k} {vs₁} (vars-in-Map k vs₁ (k∈e⇒k∈vars k here)) - (v₂ , k,v₂∈vs₂) = locateᵛ {k} {vs₂} (vars-in-Map k vs₂ (k∈e⇒k∈vars k here)) - in - m₁≼m₂⇒m₁[k]ᵛ≼m₂[k]ᵛ vs₁ vs₂ vs₁≼vs₂ k,v₁∈vs₁ k,v₂∈vs₂ - eval-Mono (# 0) _ _ = ≈ᵍ-refl - eval-Mono (# (suc n')) _ _ = ≈ᵍ-refl + (minus-Monoˡ g₂vs₁ {g₁vs₁} {g₁vs₂} (eval-Mono e₁ {vs₁} {vs₂} vs₁≼vs₂)) + (minus-Monoʳ g₁vs₂ {g₂vs₁} {g₂vs₂} (eval-Mono e₂ {vs₁} {vs₂} vs₁≼vs₂)) + eval-Mono (` k) {vs₁@((kvs₁ , _) , _)} {vs₂@((kvs₂ , _), _)} vs₁≼vs₂ + with ∈k-decᵛ k kvs₁ | ∈k-decᵛ k kvs₂ + ... | yes k∈kvs₁ | yes k∈kvs₂ = + let + (v₁ , k,v₁∈vs₁) = locateᵛ {k} {vs₁} k∈kvs₁ + (v₂ , k,v₂∈vs₂) = locateᵛ {k} {vs₂} k∈kvs₂ + in + m₁≼m₂⇒m₁[k]ᵛ≼m₂[k]ᵛ vs₁ vs₂ vs₁≼vs₂ k,v₁∈vs₁ k,v₂∈vs₂ + ... | yes k∈kvs₁ | no k∉kvs₂ = ⊥-elim (k∉kvs₂ (subst (λ l → k ∈ˡ l) (all-equal-keysᵛ vs₁ vs₂) k∈kvs₁)) + ... | no k∉kvs₁ | yes k∈kvs₂ = ⊥-elim (k∉kvs₁ (subst (λ l → k ∈ˡ l) (all-equal-keysᵛ vs₂ vs₁) k∈kvs₂)) + ... | no k∉kvs₁ | no k∉kvs₂ = IsLattice.≈-refl isLatticeᵍ + eval-Mono (# 0) _ = ≈ᵍ-refl + eval-Mono (# (suc n')) _ = ≈ᵍ-refl - private module _ (k : String) (e : Expr) (k∈e⇒k∈vars : ∀ k → k ∈ᵉ e → k ∈ˡ vars) where - open VariableSignsFiniteMap.GeneralizedUpdate vars isLatticeᵛ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) (λ _ → eval e k∈e⇒k∈vars) (λ _ {vs₁} {vs₂} vs₁≼vs₂ → eval-Mono e k∈e⇒k∈vars {vs₁} {vs₂} vs₁≼vs₂) (k ∷ []) + private module _ (k : String) (e : Expr) where + open VariableSignsFiniteMap.GeneralizedUpdate vars isLatticeᵛ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) (λ _ → eval e) (λ _ {vs₁} {vs₂} vs₁≼vs₂ → eval-Mono e {vs₁} {vs₂} vs₁≼vs₂) (k ∷ []) renaming ( f' to updateVariablesFromExpression ; f'-Monotonic to updateVariablesFromExpression-Mono @@ -265,28 +267,23 @@ module WithProg (prog : Program) where updateVariablesForState : State → StateVariables → VariableSigns updateVariablesForState s sv - -- More weirdness here. Apparently, capturing the with-equality proof - -- using 'in p' makes code that reasons about this function (below) - -- throw ill-typed with-abstraction errors. Instead, make use of the - -- fact that later with-clauses are generalized over earlier ones to - -- construct a specialization of vars-complete for (code s). - with code s | (λ k → vars-complete {k} s) - ... | k ← e | k∈codes⇒k∈vars = + with code s + ... | k ← e = let (vs , s,vs∈sv) = locateᵐ {s} {sv} (states-in-Map s sv) in - updateVariablesFromExpression k e (λ k k∈e → k∈codes⇒k∈vars k (in←₂ k∈e)) vs + updateVariablesFromExpression k e vs updateVariablesForState-Monoʳ : ∀ (s : State) → Monotonic _≼ᵐ_ _≼ᵛ_ (updateVariablesForState s) updateVariablesForState-Monoʳ s {sv₁} {sv₂} sv₁≼sv₂ - with code s | (λ k → vars-complete {k} s) - ... | k ← e | k∈codes⇒k∈vars = + with code s + ... | k ← e = let (vs₁ , s,vs₁∈sv₁) = locateᵐ {s} {sv₁} (states-in-Map s sv₁) (vs₂ , s,vs₂∈sv₂) = locateᵐ {s} {sv₂} (states-in-Map s sv₂) vs₁≼vs₂ = m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ sv₁ sv₂ sv₁≼sv₂ s,vs₁∈sv₁ s,vs₂∈sv₂ in - updateVariablesFromExpression-Mono k e (λ k k∈e → k∈codes⇒k∈vars k (in←₂ k∈e)) {vs₁} {vs₂} vs₁≼vs₂ + updateVariablesFromExpression-Mono k e {vs₁} {vs₂} vs₁≼vs₂ open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) updateVariablesForState updateVariablesForState-Monoʳ states renaming diff --git a/Lattice/FiniteMap.agda b/Lattice/FiniteMap.agda index 59d2f36..ca4cb7c 100644 --- a/Lattice/FiniteMap.agda +++ b/Lattice/FiniteMap.agda @@ -12,7 +12,7 @@ module Lattice.FiniteMap {a b : Level} {A : Set a} {B : Set b} open IsLattice lB using () renaming (_≼_ to _≼₂_) open import Lattice.Map ≡-dec-A lB as Map - using (Map; ⊔-equal-keys; ⊓-equal-keys; ∈k-dec) + using (Map; ⊔-equal-keys; ⊓-equal-keys) renaming ( _≈_ to _≈ᵐ_ ; _⊔_ to _⊔ᵐ_ @@ -37,6 +37,7 @@ open import Lattice.Map ≡-dec-A lB as Map ; updating-via-keys-≡ to updatingᵐ-via-keys-≡ ; f'-Monotonic to f'-Monotonicᵐ ; _≼_ to _≼ᵐ_ + ; ∈k-dec to ∈k-decᵐ ) open import Data.List.Membership.Propositional using () renaming (_∈_ to _∈ˡ_) open import Data.Product using (_×_; _,_; Σ; proj₁ ; proj₂) @@ -82,6 +83,8 @@ module WithKeys (ks : List A) where _∈k_ : A → FiniteMap → Set a _∈k_ k (m₁ , _) = k ∈ˡ (keysᵐ m₁) + ∈k-dec = ∈k-decᵐ + locate : ∀ {k : A} {fm : FiniteMap} → k ∈k fm → Σ B (λ v → (k , v) ∈ fm) locate {k} {fm = (m , _)} k∈kfm = locateᵐ {k} {m} k∈kfm @@ -182,7 +185,7 @@ module WithKeys (ks : List A) where fm₁ ≼ fm₂ → Pairwise _≼₂_ (fm₁ [ ks' ]) (fm₂ [ ks' ]) m₁≼m₂⇒m₁[ks]≼m₂[ks] _ _ [] _ = [] m₁≼m₂⇒m₁[ks]≼m₂[ks] fm₁@(m₁ , km₁≡ks) fm₂@(m₂ , km₂≡ks) (k ∷ ks'') m₁≼m₂ - with ∈k-dec k (proj₁ m₁) | ∈k-dec k (proj₁ m₂) + with ∈k-decᵐ k (proj₁ m₁) | ∈k-decᵐ k (proj₁ m₂) ... | yes k∈km₁ | yes k∈km₂ = let (v₁ , k,v₁∈m₁) = locateᵐ {m = m₁} k∈km₁