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

Fix comments in Forward.agda 

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-03-23 12:09:14 -07:00
parent 2e096bd64e
commit 5d56a7ce2d
1 changed files with 7 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
Analysis/Forward.agda
View File

@ -31,7 +31,8 @@ open IsFiniteHeightLattice isFiniteHeightLatticeˡ
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.
-- The variable -> abstract value (e.g. 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 ()
@ -69,7 +70,7 @@ module WithProg (prog : Program) where
fixedHeightᵛ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵛ
⊥ᵛ = proj₁ (proj₁ (proj₁ fixedHeightᵛ))
-- Finally, the map we care about is (state -> (variables -> sign)). Bring that in.
-- 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])
@ -170,7 +171,7 @@ module WithProg (prog : Program) where
; f'-Monotonic to updateAll-Mono
)
-- Finally, the whole sign analysis consists of getting the 'join'
-- Finally, the whole 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.
@ -178,7 +179,9 @@ module WithProg (prog : Program) where
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₂)
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₂)