Extract common parts of forward analyses into Forward.agda
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
1a7b2a1736
commit
2e096bd64e
187
Analysis/Forward.agda
Normal file
187
Analysis/Forward.agda
Normal file
|
|
@ -0,0 +1,187 @@
|
||||||
|
open import Language
|
||||||
|
open import Lattice
|
||||||
|
|
||||||
|
module Analysis.Forward
|
||||||
|
{L : Set} {h}
|
||||||
|
{_≈ˡ_ : L → L → Set} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L}
|
||||||
|
(isFiniteHeightLatticeˡ : IsFiniteHeightLattice L h _≈ˡ_ _⊔ˡ_ _⊓ˡ_)
|
||||||
|
(≈ˡ-dec : IsDecidable _≈ˡ_) where
|
||||||
|
|
||||||
|
open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
|
||||||
|
open import Data.Nat using (suc)
|
||||||
|
open import Data.Product using (_×_; proj₁; _,_)
|
||||||
|
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)
|
||||||
|
open import Relation.Nullary using (¬_; Dec; yes; no)
|
||||||
|
open import Data.Unit using (⊤)
|
||||||
|
open import Function using (_∘_)
|
||||||
|
|
||||||
|
open import Utils using (Pairwise)
|
||||||
|
import Lattice.FiniteValueMap
|
||||||
|
|
||||||
|
open IsFiniteHeightLattice isFiniteHeightLatticeˡ
|
||||||
|
using ()
|
||||||
|
renaming
|
||||||
|
( isLattice to isLatticeˡ
|
||||||
|
; fixedHeight to fixedHeightˡ
|
||||||
|
; _≼_ to _≼ˡ_
|
||||||
|
)
|
||||||
|
|
||||||
|
module WithProg (prog : Program) where
|
||||||
|
open Program prog
|
||||||
|
|
||||||
|
-- The variable -> sign map is a finite value-map with keys strings. Use a bundle to avoid explicitly specifying operators.
|
||||||
|
module VariableValuesFiniteMap = Lattice.FiniteValueMap.WithKeys _≟ˢ_ isLatticeˡ vars
|
||||||
|
open VariableValuesFiniteMap
|
||||||
|
using ()
|
||||||
|
renaming
|
||||||
|
( FiniteMap to VariableValues
|
||||||
|
; isLattice to isLatticeᵛ
|
||||||
|
; _≈_ to _≈ᵛ_
|
||||||
|
; _⊔_ to _⊔ᵛ_
|
||||||
|
; _≼_ to _≼ᵛ_
|
||||||
|
; ≈₂-dec⇒≈-dec to ≈ˡ-dec⇒≈ᵛ-dec
|
||||||
|
; _∈_ to _∈ᵛ_
|
||||||
|
; _∈k_ to _∈kᵛ_
|
||||||
|
; _updating_via_ to _updatingᵛ_via_
|
||||||
|
; locate to locateᵛ
|
||||||
|
; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵛ≼m₂[k]ᵛ
|
||||||
|
; ∈k-dec to ∈k-decᵛ
|
||||||
|
; all-equal-keys to all-equal-keysᵛ
|
||||||
|
)
|
||||||
|
public
|
||||||
|
open IsLattice isLatticeᵛ
|
||||||
|
using ()
|
||||||
|
renaming
|
||||||
|
( ⊔-Monotonicˡ to ⊔ᵛ-Monotonicˡ
|
||||||
|
; ⊔-Monotonicʳ to ⊔ᵛ-Monotonicʳ
|
||||||
|
; ⊔-idemp to ⊔ᵛ-idemp
|
||||||
|
)
|
||||||
|
open Lattice.FiniteValueMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight _≟ˢ_ isLatticeˡ vars-Unique ≈ˡ-dec _ fixedHeightˡ
|
||||||
|
using ()
|
||||||
|
renaming
|
||||||
|
( isFiniteHeightLattice to isFiniteHeightLatticeᵛ
|
||||||
|
)
|
||||||
|
|
||||||
|
≈ᵛ-dec = ≈ˡ-dec⇒≈ᵛ-dec ≈ˡ-dec
|
||||||
|
joinSemilatticeᵛ = IsFiniteHeightLattice.joinSemilattice isFiniteHeightLatticeᵛ
|
||||||
|
fixedHeightᵛ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵛ
|
||||||
|
⊥ᵛ = proj₁ (proj₁ (proj₁ fixedHeightᵛ))
|
||||||
|
|
||||||
|
-- Finally, the map we care about is (state -> (variables -> sign)). Bring that in.
|
||||||
|
module StateVariablesFiniteMap = Lattice.FiniteValueMap.WithKeys _≟_ isLatticeᵛ states
|
||||||
|
open StateVariablesFiniteMap
|
||||||
|
using (_[_]; m₁≼m₂⇒m₁[ks]≼m₂[ks])
|
||||||
|
renaming
|
||||||
|
( FiniteMap to StateVariables
|
||||||
|
; isLattice to isLatticeᵐ
|
||||||
|
; _∈k_ to _∈kᵐ_
|
||||||
|
; locate to locateᵐ
|
||||||
|
; _≼_ to _≼ᵐ_
|
||||||
|
; ≈₂-dec⇒≈-dec to ≈ᵛ-dec⇒≈ᵐ-dec
|
||||||
|
; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ
|
||||||
|
)
|
||||||
|
public
|
||||||
|
open Lattice.FiniteValueMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight _≟_ isLatticeᵛ states-Unique ≈ᵛ-dec _ fixedHeightᵛ
|
||||||
|
using ()
|
||||||
|
renaming
|
||||||
|
( isFiniteHeightLattice to isFiniteHeightLatticeᵐ
|
||||||
|
)
|
||||||
|
|
||||||
|
≈ᵐ-dec = ≈ᵛ-dec⇒≈ᵐ-dec ≈ᵛ-dec
|
||||||
|
fixedHeightᵐ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵐ
|
||||||
|
|
||||||
|
-- build up the 'join' function, which follows from Exercise 4.26's
|
||||||
|
--
|
||||||
|
-- L₁ → (A → L₂)
|
||||||
|
--
|
||||||
|
-- Construction, with L₁ = (A → L₂), and f = id
|
||||||
|
|
||||||
|
joinForKey : State → StateVariables → VariableValues
|
||||||
|
joinForKey k states = foldr _⊔ᵛ_ ⊥ᵛ (states [ incoming k ])
|
||||||
|
|
||||||
|
-- The per-key join is made up of map key accesses (which are monotonic)
|
||||||
|
-- and folds using the join operation (also monotonic)
|
||||||
|
|
||||||
|
joinForKey-Mono : ∀ (k : State) → Monotonic _≼ᵐ_ _≼ᵛ_ (joinForKey k)
|
||||||
|
joinForKey-Mono k {fm₁} {fm₂} fm₁≼fm₂ =
|
||||||
|
foldr-Mono joinSemilatticeᵛ joinSemilatticeᵛ (fm₁ [ incoming k ]) (fm₂ [ incoming k ]) _⊔ᵛ_ ⊥ᵛ ⊥ᵛ
|
||||||
|
(m₁≼m₂⇒m₁[ks]≼m₂[ks] fm₁ fm₂ (incoming k) 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
|
||||||
|
renaming
|
||||||
|
( f' to joinAll
|
||||||
|
; f'-Monotonic to joinAll-Mono
|
||||||
|
)
|
||||||
|
|
||||||
|
-- With 'join' in hand, we need to perform abstract evaluation.
|
||||||
|
module WithEvaluator (eval : Expr → VariableValues → L)
|
||||||
|
(eval-Mono : ∀ (e : Expr) → Monotonic _≼ᵛ_ _≼ˡ_ (eval e)) where
|
||||||
|
|
||||||
|
-- For a particular evaluation function, we need to perform an evaluation
|
||||||
|
-- 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 ∷ [])
|
||||||
|
renaming
|
||||||
|
( f' to updateVariablesFromExpression
|
||||||
|
; f'-Monotonic to updateVariablesFromExpression-Mono
|
||||||
|
)
|
||||||
|
public
|
||||||
|
|
||||||
|
states-in-Map : ∀ (s : State) (sv : StateVariables) → s ∈kᵐ sv
|
||||||
|
states-in-Map s sv@(m , ksv≡states) rewrite ksv≡states = states-complete s
|
||||||
|
|
||||||
|
-- The per-state update function makes use of the single-key setter,
|
||||||
|
-- updateVariablesFromExpression, for the case where the statement
|
||||||
|
-- is an assignment.
|
||||||
|
--
|
||||||
|
-- This per-state function adjusts the variables in that state,
|
||||||
|
-- also monotonically; we derive the for-each-state update from
|
||||||
|
-- the Exercise 4.26 again.
|
||||||
|
|
||||||
|
updateVariablesForState : State → StateVariables → VariableValues
|
||||||
|
updateVariablesForState s sv
|
||||||
|
with code s
|
||||||
|
... | k ← e =
|
||||||
|
let
|
||||||
|
(vs , s,vs∈sv) = locateᵐ {s} {sv} (states-in-Map s sv)
|
||||||
|
in
|
||||||
|
updateVariablesFromExpression k e vs
|
||||||
|
|
||||||
|
updateVariablesForState-Monoʳ : ∀ (s : State) → Monotonic _≼ᵐ_ _≼ᵛ_ (updateVariablesForState s)
|
||||||
|
updateVariablesForState-Monoʳ s {sv₁} {sv₂} sv₁≼sv₂
|
||||||
|
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 {vs₁} {vs₂} vs₁≼vs₂
|
||||||
|
|
||||||
|
open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) updateVariablesForState updateVariablesForState-Monoʳ states
|
||||||
|
renaming
|
||||||
|
( f' to updateAll
|
||||||
|
; f'-Monotonic to updateAll-Mono
|
||||||
|
)
|
||||||
|
|
||||||
|
-- Finally, the whole sign analysis consists of getting the 'join'
|
||||||
|
-- of all incoming states, then applying the per-state evaluation
|
||||||
|
-- function. This is just a composition, and is trivially monotonic.
|
||||||
|
|
||||||
|
analyze : StateVariables → StateVariables
|
||||||
|
analyze = updateAll ∘ joinAll
|
||||||
|
|
||||||
|
analyze-Mono : Monotonic _≼ᵐ_ _≼ᵐ_ analyze
|
||||||
|
analyze-Mono {sv₁} {sv₂} sv₁≼sv₂ = updateAll-Mono {joinAll sv₁} {joinAll sv₂} (joinAll-Mono {sv₁} {sv₂} sv₁≼sv₂)
|
||||||
|
|
||||||
|
-- The fixed point of the 'analyze' function is our final goal.
|
||||||
|
open import Fixedpoint ≈ᵐ-dec isFiniteHeightLatticeᵐ analyze (λ {m₁} {m₂} m₁≼m₂ → analyze-Mono {m₁} {m₂} m₁≼m₂)
|
||||||
|
using ()
|
||||||
|
renaming (aᶠ to result)
|
||||||
|
public
|
||||||
|
|
@ -1,21 +1,16 @@
|
||||||
module Analysis.Sign where
|
module Analysis.Sign where
|
||||||
|
|
||||||
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.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 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)
|
||||||
open import Relation.Nullary using (¬_; Dec; yes; no)
|
open import Relation.Nullary using (yes; no)
|
||||||
open import Data.Unit using (⊤)
|
|
||||||
open import Function using (_∘_)
|
|
||||||
|
|
||||||
open import Language
|
open import Language
|
||||||
open import Lattice
|
open import Lattice
|
||||||
open import Utils using (Pairwise)
|
|
||||||
open import Showable using (Showable; show)
|
open import Showable using (Showable; show)
|
||||||
import Lattice.FiniteValueMap
|
import Analysis.Forward
|
||||||
|
|
||||||
data Sign : Set where
|
data Sign : Set where
|
||||||
+ : Sign
|
+ : Sign
|
||||||
|
|
@ -114,101 +109,10 @@ postulate minus-Monoʳ : ∀ (s₁ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ
|
||||||
module WithProg (prog : Program) where
|
module WithProg (prog : Program) where
|
||||||
open Program prog
|
open Program prog
|
||||||
|
|
||||||
-- The variable -> sign map is a finite value-map with keys strings. Use a bundle to avoid explicitly specifying operators.
|
module ForwardWithProg = Analysis.Forward.WithProg (record { isLattice = isLatticeᵍ; fixedHeight = fixedHeightᵍ }) ≈ᵍ-dec prog
|
||||||
module VariableSignsFiniteMap = Lattice.FiniteValueMap.WithKeys _≟ˢ_ isLatticeᵍ vars
|
open ForwardWithProg
|
||||||
open VariableSignsFiniteMap
|
|
||||||
using ()
|
|
||||||
renaming
|
|
||||||
( FiniteMap to VariableSigns
|
|
||||||
; isLattice to isLatticeᵛ
|
|
||||||
; _≈_ to _≈ᵛ_
|
|
||||||
; _⊔_ to _⊔ᵛ_
|
|
||||||
; _≼_ to _≼ᵛ_
|
|
||||||
; ≈₂-dec⇒≈-dec to ≈ᵍ-dec⇒≈ᵛ-dec
|
|
||||||
; _∈_ to _∈ᵛ_
|
|
||||||
; _∈k_ to _∈kᵛ_
|
|
||||||
; _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 ()
|
|
||||||
renaming
|
|
||||||
( ⊔-Monotonicˡ to ⊔ᵛ-Monotonicˡ
|
|
||||||
; ⊔-Monotonicʳ to ⊔ᵛ-Monotonicʳ
|
|
||||||
; ⊔-idemp to ⊔ᵛ-idemp
|
|
||||||
)
|
|
||||||
open Lattice.FiniteValueMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight _≟ˢ_ isLatticeᵍ vars-Unique ≈ᵍ-dec _ fixedHeightᵍ
|
|
||||||
using ()
|
|
||||||
renaming
|
|
||||||
( isFiniteHeightLattice to isFiniteHeightLatticeᵛ
|
|
||||||
)
|
|
||||||
|
|
||||||
≈ᵛ-dec = ≈ᵍ-dec⇒≈ᵛ-dec ≈ᵍ-dec
|
eval : ∀ (e : Expr) → VariableValues → SignLattice
|
||||||
joinSemilatticeᵛ = IsFiniteHeightLattice.joinSemilattice isFiniteHeightLatticeᵛ
|
|
||||||
fixedHeightᵛ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵛ
|
|
||||||
⊥ᵛ = proj₁ (proj₁ (proj₁ fixedHeightᵛ))
|
|
||||||
|
|
||||||
-- Finally, the map we care about is (state -> (variables -> sign)). Bring that in.
|
|
||||||
module StateVariablesFiniteMap = Lattice.FiniteValueMap.WithKeys _≟_ isLatticeᵛ states
|
|
||||||
open StateVariablesFiniteMap
|
|
||||||
using (_[_]; m₁≼m₂⇒m₁[ks]≼m₂[ks])
|
|
||||||
renaming
|
|
||||||
( FiniteMap to StateVariables
|
|
||||||
; isLattice to isLatticeᵐ
|
|
||||||
; _∈k_ to _∈kᵐ_
|
|
||||||
; locate to locateᵐ
|
|
||||||
; _≼_ to _≼ᵐ_
|
|
||||||
; ≈₂-dec⇒≈-dec to ≈ᵛ-dec⇒≈ᵐ-dec
|
|
||||||
; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ
|
|
||||||
)
|
|
||||||
open Lattice.FiniteValueMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight _≟_ isLatticeᵛ states-Unique ≈ᵛ-dec _ fixedHeightᵛ
|
|
||||||
using ()
|
|
||||||
renaming
|
|
||||||
( isFiniteHeightLattice to isFiniteHeightLatticeᵐ
|
|
||||||
)
|
|
||||||
|
|
||||||
≈ᵐ-dec = ≈ᵛ-dec⇒≈ᵐ-dec ≈ᵛ-dec
|
|
||||||
fixedHeightᵐ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵐ
|
|
||||||
|
|
||||||
-- build up the 'join' function, which follows from Exercise 4.26's
|
|
||||||
--
|
|
||||||
-- L₁ → (A → L₂)
|
|
||||||
--
|
|
||||||
-- Construction, with L₁ = (A → L₂), and f = id
|
|
||||||
|
|
||||||
joinForKey : State → StateVariables → VariableSigns
|
|
||||||
joinForKey k states = foldr _⊔ᵛ_ ⊥ᵛ (states [ incoming k ])
|
|
||||||
|
|
||||||
-- The per-key join is made up of map key accesses (which are monotonic)
|
|
||||||
-- and folds using the join operation (also monotonic)
|
|
||||||
|
|
||||||
joinForKey-Mono : ∀ (k : State) → Monotonic _≼ᵐ_ _≼ᵛ_ (joinForKey k)
|
|
||||||
joinForKey-Mono k {fm₁} {fm₂} fm₁≼fm₂ =
|
|
||||||
foldr-Mono joinSemilatticeᵛ joinSemilatticeᵛ (fm₁ [ incoming k ]) (fm₂ [ incoming k ]) _⊔ᵛ_ ⊥ᵛ ⊥ᵛ
|
|
||||||
(m₁≼m₂⇒m₁[ks]≼m₂[ks] fm₁ fm₂ (incoming k) 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
|
|
||||||
renaming
|
|
||||||
( f' to joinAll
|
|
||||||
; f'-Monotonic to joinAll-Mono
|
|
||||||
)
|
|
||||||
|
|
||||||
-- With 'join' in hand, we need to perform abstract evaluation.
|
|
||||||
|
|
||||||
vars-in-Map : ∀ (k : String) (vs : VariableSigns) →
|
|
||||||
k ∈ˡ vars → k ∈kᵛ vs
|
|
||||||
vars-in-Map k vs@(m , kvs≡vars) k∈vars rewrite kvs≡vars = k∈vars
|
|
||||||
|
|
||||||
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) → VariableSigns → SignLattice
|
|
||||||
eval (e₁ + e₂) vs = plus (eval e₁ vs) (eval e₂ vs)
|
eval (e₁ + e₂) vs = plus (eval e₁ vs) (eval e₂ vs)
|
||||||
eval (e₁ - e₂) vs = minus (eval e₁ vs) (eval e₂ vs)
|
eval (e₁ - e₂) vs = minus (eval e₁ vs) (eval e₂ vs)
|
||||||
eval (` k) vs
|
eval (` k) vs
|
||||||
|
|
@ -257,50 +161,7 @@ module WithProg (prog : Program) where
|
||||||
eval-Mono (# 0) _ = ≈ᵍ-refl
|
eval-Mono (# 0) _ = ≈ᵍ-refl
|
||||||
eval-Mono (# (suc n')) _ = ≈ᵍ-refl
|
eval-Mono (# (suc n')) _ = ≈ᵍ-refl
|
||||||
|
|
||||||
private module _ (k : String) (e : Expr) where
|
open ForwardWithProg.WithEvaluator eval eval-Mono using (result)
|
||||||
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
|
|
||||||
)
|
|
||||||
public
|
|
||||||
|
|
||||||
updateVariablesForState : State → StateVariables → VariableSigns
|
-- For debugging purposes, print out the result.
|
||||||
updateVariablesForState s sv
|
output = show result
|
||||||
with code s
|
|
||||||
... | k ← e =
|
|
||||||
let
|
|
||||||
(vs , s,vs∈sv) = locateᵐ {s} {sv} (states-in-Map s sv)
|
|
||||||
in
|
|
||||||
updateVariablesFromExpression k e vs
|
|
||||||
|
|
||||||
updateVariablesForState-Monoʳ : ∀ (s : State) → Monotonic _≼ᵐ_ _≼ᵛ_ (updateVariablesForState s)
|
|
||||||
updateVariablesForState-Monoʳ s {sv₁} {sv₂} sv₁≼sv₂
|
|
||||||
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 {vs₁} {vs₂} vs₁≼vs₂
|
|
||||||
|
|
||||||
open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) updateVariablesForState updateVariablesForState-Monoʳ states
|
|
||||||
renaming
|
|
||||||
( f' to updateAll
|
|
||||||
; f'-Monotonic to updateAll-Mono
|
|
||||||
)
|
|
||||||
|
|
||||||
analyze : StateVariables → StateVariables
|
|
||||||
analyze = updateAll ∘ joinAll
|
|
||||||
|
|
||||||
analyze-Mono : Monotonic _≼ᵐ_ _≼ᵐ_ analyze
|
|
||||||
analyze-Mono {sv₁} {sv₂} sv₁≼sv₂ = updateAll-Mono {joinAll sv₁} {joinAll sv₂} (joinAll-Mono {sv₁} {sv₂} sv₁≼sv₂)
|
|
||||||
|
|
||||||
open import Fixedpoint ≈ᵐ-dec isFiniteHeightLatticeᵐ analyze (λ {m₁} {m₂} m₁≼m₂ → analyze-Mono {m₁} {m₂} m₁≼m₂)
|
|
||||||
using ()
|
|
||||||
renaming (aᶠ to signs)
|
|
||||||
|
|
||||||
|
|
||||||
-- Debugging code: print the resulting map.
|
|
||||||
output = show signs
|
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue
Block a user