Adjust behavior of eval to not require constant 'k in vars' threading
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
f0da9a9020
commit
1a7b2a1736
|
@ -3,6 +3,7 @@ module Analysis.Sign where
|
||||||
open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
|
open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
|
||||||
open import Data.Nat using (suc)
|
open import Data.Nat using (suc)
|
||||||
open import Data.Product using (_×_; proj₁; _,_)
|
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 using (List; _∷_; []; foldr; cartesianProduct; cartesianProductWith)
|
||||||
open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_)
|
open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_)
|
||||||
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; subst)
|
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.
|
-- 'sign' has no underlying lattice structure, so use the 'plain' above-below lattice.
|
||||||
open AB.Plain 0ˢ using ()
|
open AB.Plain 0ˢ using ()
|
||||||
renaming
|
renaming
|
||||||
( finiteHeightLattice to finiteHeightLatticeᵍ
|
( isLattice to isLatticeᵍ
|
||||||
; isLattice to isLatticeᵍ
|
|
||||||
; fixedHeight to fixedHeightᵍ
|
; fixedHeight to fixedHeightᵍ
|
||||||
; _≼_ to _≼ᵍ_
|
; _≼_ to _≼ᵍ_
|
||||||
; _⊔_ to _⊔ᵍ_
|
; _⊔_ to _⊔ᵍ_
|
||||||
|
@ -130,6 +130,8 @@ module WithProg (prog : Program) where
|
||||||
; _updating_via_ to _updatingᵛ_via_
|
; _updating_via_ to _updatingᵛ_via_
|
||||||
; locate to locateᵛ
|
; locate to locateᵛ
|
||||||
; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵛ≼m₂[k]ᵛ
|
; 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ᵛ
|
open IsLattice isLatticeᵛ
|
||||||
using ()
|
using ()
|
||||||
|
@ -206,57 +208,57 @@ module WithProg (prog : Program) where
|
||||||
states-in-Map : ∀ (s : State) (sv : StateVariables) → s ∈kᵐ sv
|
states-in-Map : ∀ (s : State) (sv : StateVariables) → s ∈kᵐ sv
|
||||||
states-in-Map s sv@(m , ksv≡states) rewrite ksv≡states = states-complete s
|
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 : Expr) → VariableSigns → SignLattice
|
||||||
eval (e₁ + e₂) k∈e⇒k∈vars vs =
|
eval (e₁ + e₂) vs = plus (eval e₁ vs) (eval e₂ vs)
|
||||||
plus (eval e₁ (λ k k∈e₁ → k∈e⇒k∈vars k (in⁺₁ k∈e₁)) vs)
|
eval (e₁ - e₂) vs = minus (eval e₁ vs) (eval e₂ vs)
|
||||||
(eval e₂ (λ k k∈e₂ → k∈e⇒k∈vars k (in⁺₂ k∈e₂)) vs)
|
eval (` k) vs
|
||||||
eval (e₁ - e₂) k∈e⇒k∈vars vs =
|
with ∈k-decᵛ k (proj₁ (proj₁ vs))
|
||||||
minus (eval e₁ (λ k k∈e₁ → k∈e⇒k∈vars k (in⁻₁ k∈e₁)) vs)
|
... | yes k∈vs = proj₁ (locateᵛ {k} {vs} k∈vs)
|
||||||
(eval e₂ (λ k k∈e₂ → k∈e⇒k∈vars k (in⁻₂ k∈e₂)) vs)
|
... | no _ = ⊤ᵍ
|
||||||
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 (# 0) _ _ = [ 0ˢ ]ᵍ
|
eval (# (suc n')) _ = [ + ]ᵍ
|
||||||
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 : Expr) → Monotonic _≼ᵛ_ _≼ᵍ_ (eval e)
|
||||||
eval-Mono (e₁ + e₂) k∈e⇒k∈vars {vs₁} {vs₂} vs₁≼vs₂ =
|
eval-Mono (e₁ + e₂) {vs₁} {vs₂} vs₁≼vs₂ =
|
||||||
let
|
let
|
||||||
-- TODO: can this be done with less boilerplate?
|
-- TODO: can this be done with less boilerplate?
|
||||||
k∈e₁⇒k∈vars = λ k k∈e₁ → k∈e⇒k∈vars k (in⁺₁ k∈e₁)
|
g₁vs₁ = eval e₁ vs₁
|
||||||
k∈e₂⇒k∈vars = λ k k∈e₂ → k∈e⇒k∈vars k (in⁺₂ k∈e₂)
|
g₂vs₁ = eval e₂ vs₁
|
||||||
g₁vs₁ = eval e₁ k∈e₁⇒k∈vars vs₁
|
g₁vs₂ = eval e₁ vs₂
|
||||||
g₂vs₁ = eval e₂ k∈e₂⇒k∈vars vs₁
|
g₂vs₂ = eval e₂ vs₂
|
||||||
g₁vs₂ = eval e₁ k∈e₁⇒k∈vars vs₂
|
|
||||||
g₂vs₂ = eval e₂ k∈e₂⇒k∈vars vs₂
|
|
||||||
in
|
in
|
||||||
≼ᵍ-trans
|
≼ᵍ-trans
|
||||||
{plus g₁vs₁ g₂vs₁} {plus g₁vs₂ g₂vs₁} {plus g₁vs₂ g₂vs₂}
|
{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₁ {vs₁} {vs₂} vs₁≼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₂ {vs₁} {vs₂} vs₁≼vs₂))
|
||||||
eval-Mono (e₁ - e₂) k∈e⇒k∈vars {vs₁} {vs₂} vs₁≼vs₂ =
|
eval-Mono (e₁ - e₂) {vs₁} {vs₂} vs₁≼vs₂ =
|
||||||
let
|
let
|
||||||
-- TODO: here too -- can this be done with less boilerplate?
|
-- 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₁)
|
g₁vs₁ = eval e₁ vs₁
|
||||||
k∈e₂⇒k∈vars = λ k k∈e₂ → k∈e⇒k∈vars k (in⁻₂ k∈e₂)
|
g₂vs₁ = eval e₂ vs₁
|
||||||
g₁vs₁ = eval e₁ k∈e₁⇒k∈vars vs₁
|
g₁vs₂ = eval e₁ vs₂
|
||||||
g₂vs₁ = eval e₂ k∈e₂⇒k∈vars vs₁
|
g₂vs₂ = eval e₂ vs₂
|
||||||
g₁vs₂ = eval e₁ k∈e₁⇒k∈vars vs₂
|
|
||||||
g₂vs₂ = eval e₂ k∈e₂⇒k∈vars vs₂
|
|
||||||
in
|
in
|
||||||
≼ᵍ-trans
|
≼ᵍ-trans
|
||||||
{minus g₁vs₁ g₂vs₁} {minus g₁vs₂ g₂vs₁} {minus g₁vs₂ g₂vs₂}
|
{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₁ {vs₁} {vs₂} vs₁≼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₂ {vs₁} {vs₂} vs₁≼vs₂))
|
||||||
eval-Mono (` k) k∈e⇒k∈vars {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
|
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₁} k∈kvs₁
|
||||||
(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₂} k∈kvs₂
|
||||||
in
|
in
|
||||||
m₁≼m₂⇒m₁[k]ᵛ≼m₂[k]ᵛ vs₁ vs₂ vs₁≼vs₂ k,v₁∈vs₁ k,v₂∈vs₂
|
m₁≼m₂⇒m₁[k]ᵛ≼m₂[k]ᵛ vs₁ vs₂ vs₁≼vs₂ k,v₁∈vs₁ k,v₂∈vs₂
|
||||||
eval-Mono (# 0) _ _ = ≈ᵍ-refl
|
... | yes k∈kvs₁ | no k∉kvs₂ = ⊥-elim (k∉kvs₂ (subst (λ l → k ∈ˡ l) (all-equal-keysᵛ vs₁ vs₂) k∈kvs₁))
|
||||||
eval-Mono (# (suc n')) _ _ = ≈ᵍ-refl
|
... | 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
|
private module _ (k : String) (e : Expr) 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 ∷ [])
|
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
|
renaming
|
||||||
( f' to updateVariablesFromExpression
|
( f' to updateVariablesFromExpression
|
||||||
; f'-Monotonic to updateVariablesFromExpression-Mono
|
; f'-Monotonic to updateVariablesFromExpression-Mono
|
||||||
|
@ -265,28 +267,23 @@ module WithProg (prog : Program) where
|
||||||
|
|
||||||
updateVariablesForState : State → StateVariables → VariableSigns
|
updateVariablesForState : State → StateVariables → VariableSigns
|
||||||
updateVariablesForState s sv
|
updateVariablesForState s sv
|
||||||
-- More weirdness here. Apparently, capturing the with-equality proof
|
with code s
|
||||||
-- using 'in p' makes code that reasons about this function (below)
|
... | k ← e =
|
||||||
-- 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 =
|
|
||||||
let
|
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)
|
||||||
in
|
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 : State) → Monotonic _≼ᵐ_ _≼ᵛ_ (updateVariablesForState s)
|
||||||
updateVariablesForState-Monoʳ s {sv₁} {sv₂} sv₁≼sv₂
|
updateVariablesForState-Monoʳ s {sv₁} {sv₂} sv₁≼sv₂
|
||||||
with code s | (λ k → vars-complete {k} s)
|
with code s
|
||||||
... | k ← e | k∈codes⇒k∈vars =
|
... | k ← e =
|
||||||
let
|
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₂ , 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₂
|
vs₁≼vs₂ = m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ sv₁ sv₂ sv₁≼sv₂ s,vs₁∈sv₁ s,vs₂∈sv₂
|
||||||
in
|
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
|
open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) updateVariablesForState updateVariablesForState-Monoʳ states
|
||||||
renaming
|
renaming
|
||||||
|
|
|
@ -12,7 +12,7 @@ module Lattice.FiniteMap {a b : Level} {A : Set a} {B : Set b}
|
||||||
|
|
||||||
open IsLattice lB using () renaming (_≼_ to _≼₂_)
|
open IsLattice lB using () renaming (_≼_ to _≼₂_)
|
||||||
open import Lattice.Map ≡-dec-A lB as Map
|
open import Lattice.Map ≡-dec-A lB as Map
|
||||||
using (Map; ⊔-equal-keys; ⊓-equal-keys; ∈k-dec)
|
using (Map; ⊔-equal-keys; ⊓-equal-keys)
|
||||||
renaming
|
renaming
|
||||||
( _≈_ to _≈ᵐ_
|
( _≈_ to _≈ᵐ_
|
||||||
; _⊔_ to _⊔ᵐ_
|
; _⊔_ to _⊔ᵐ_
|
||||||
|
@ -37,6 +37,7 @@ open import Lattice.Map ≡-dec-A lB as Map
|
||||||
; updating-via-keys-≡ to updatingᵐ-via-keys-≡
|
; updating-via-keys-≡ to updatingᵐ-via-keys-≡
|
||||||
; f'-Monotonic to f'-Monotonicᵐ
|
; f'-Monotonic to f'-Monotonicᵐ
|
||||||
; _≼_ to _≼ᵐ_
|
; _≼_ to _≼ᵐ_
|
||||||
|
; ∈k-dec to ∈k-decᵐ
|
||||||
)
|
)
|
||||||
open import Data.List.Membership.Propositional using () renaming (_∈_ to _∈ˡ_)
|
open import Data.List.Membership.Propositional using () renaming (_∈_ to _∈ˡ_)
|
||||||
open import Data.Product using (_×_; _,_; Σ; proj₁ ; proj₂)
|
open import Data.Product using (_×_; _,_; Σ; proj₁ ; proj₂)
|
||||||
|
@ -82,6 +83,8 @@ module WithKeys (ks : List A) where
|
||||||
_∈k_ : A → FiniteMap → Set a
|
_∈k_ : A → FiniteMap → Set a
|
||||||
_∈k_ k (m₁ , _) = k ∈ˡ (keysᵐ m₁)
|
_∈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 : A} {fm : FiniteMap} → k ∈k fm → Σ B (λ v → (k , v) ∈ fm)
|
||||||
locate {k} {fm = (m , _)} k∈kfm = locateᵐ {k} {m} k∈kfm
|
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' ])
|
fm₁ ≼ fm₂ → Pairwise _≼₂_ (fm₁ [ ks' ]) (fm₂ [ ks' ])
|
||||||
m₁≼m₂⇒m₁[ks]≼m₂[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₂
|
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₂ =
|
... | yes k∈km₁ | yes k∈km₂ =
|
||||||
let
|
let
|
||||||
(v₁ , k,v₁∈m₁) = locateᵐ {m = m₁} k∈km₁
|
(v₁ , k,v₁∈m₁) = locateᵐ {m = m₁} k∈km₁
|
||||||
|
|
Loading…
Reference in New Issue
Block a user