144 lines
5.4 KiB
Agda
144 lines
5.4 KiB
Agda
module Analysis.Sign where
|
||
|
||
open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
|
||
open import Data.Product using (_×_; proj₁; _,_)
|
||
open import Data.List using (List; _∷_; []; foldr; cartesianProduct; cartesianProductWith)
|
||
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans)
|
||
open import Relation.Nullary using (¬_; Dec; yes; no)
|
||
open import Data.Unit using (⊤)
|
||
|
||
open import Language
|
||
open import Lattice
|
||
open import Utils using (Pairwise)
|
||
import Lattice.Bundles.FiniteValueMap
|
||
|
||
private module FixedHeightFiniteMap = Lattice.Bundles.FiniteValueMap.FromFiniteHeightLattice
|
||
|
||
data Sign : Set where
|
||
+ : Sign
|
||
- : Sign
|
||
0ˢ : Sign
|
||
|
||
-- g for siGn; s is used for strings and i is not very descriptive.
|
||
_≟ᵍ_ : IsDecidable (_≡_ {_} {Sign})
|
||
_≟ᵍ_ + + = yes refl
|
||
_≟ᵍ_ + - = no (λ ())
|
||
_≟ᵍ_ + 0ˢ = no (λ ())
|
||
_≟ᵍ_ - + = no (λ ())
|
||
_≟ᵍ_ - - = yes refl
|
||
_≟ᵍ_ - 0ˢ = no (λ ())
|
||
_≟ᵍ_ 0ˢ + = no (λ ())
|
||
_≟ᵍ_ 0ˢ - = no (λ ())
|
||
_≟ᵍ_ 0ˢ 0ˢ = yes refl
|
||
|
||
-- embelish 'sign' with a top and bottom element.
|
||
open import Lattice.AboveBelow Sign _≡_ (record { ≈-refl = refl; ≈-sym = sym; ≈-trans = trans }) _≟ᵍ_ as AB
|
||
using ()
|
||
renaming
|
||
( AboveBelow to SignLattice
|
||
; ≈-dec to ≈ᵍ-dec
|
||
; ⊥ to ⊥ᵍ
|
||
; ⊤ to ⊤ᵍ
|
||
; [_] to [_]ᵍ
|
||
; ≈-⊥-⊥ to ≈ᵍ-⊥ᵍ-⊥ᵍ
|
||
; ≈-⊤-⊤ to ≈ᵍ-⊤ᵍ-⊤ᵍ
|
||
; ≈-lift to ≈ᵍ-lift
|
||
)
|
||
-- 'sign' has no underlying lattice structure, so use the 'plain' above-below lattice.
|
||
open AB.Plain using () renaming (finiteHeightLattice to finiteHeightLatticeᵍ-if-inhabited)
|
||
|
||
finiteHeightLatticeᵍ = finiteHeightLatticeᵍ-if-inhabited 0ˢ
|
||
|
||
open FiniteHeightLattice finiteHeightLatticeᵍ
|
||
using ()
|
||
renaming
|
||
( _≼_ to _≼ᵍ_
|
||
; _≈_ to _≈ᵍ_
|
||
; _⊔_ to _⊔ᵍ_
|
||
; ≈-refl to ≈ᵍ-refl
|
||
)
|
||
|
||
plus : SignLattice → SignLattice → SignLattice
|
||
plus ⊥ᵍ _ = ⊥ᵍ
|
||
plus _ ⊥ᵍ = ⊥ᵍ
|
||
plus ⊤ᵍ _ = ⊤ᵍ
|
||
plus _ ⊤ᵍ = ⊤ᵍ
|
||
plus [ + ]ᵍ [ + ]ᵍ = [ + ]ᵍ
|
||
plus [ + ]ᵍ [ - ]ᵍ = ⊤ᵍ
|
||
plus [ + ]ᵍ [ 0ˢ ]ᵍ = [ + ]ᵍ
|
||
plus [ - ]ᵍ [ + ]ᵍ = ⊤ᵍ
|
||
plus [ - ]ᵍ [ - ]ᵍ = [ - ]ᵍ
|
||
plus [ - ]ᵍ [ 0ˢ ]ᵍ = [ - ]ᵍ
|
||
plus [ 0ˢ ]ᵍ [ + ]ᵍ = [ + ]ᵍ
|
||
plus [ 0ˢ ]ᵍ [ - ]ᵍ = [ - ]ᵍ
|
||
plus [ 0ˢ ]ᵍ [ 0ˢ ]ᵍ = [ 0ˢ ]ᵍ
|
||
|
||
-- this is incredibly tedious: 125 cases per monotonicity proof, and tactics
|
||
-- are hard. postulate for now.
|
||
postulate plus-Monoˡ : ∀ (s₂ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ_ (λ s₁ → plus s₁ s₂)
|
||
postulate plus-Monoʳ : ∀ (s₁ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ_ (plus s₁)
|
||
|
||
module _ (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.
|
||
open FixedHeightFiniteMap String SignLattice _≟ˢ_ finiteHeightLatticeᵍ vars-Unique ≈ᵍ-dec
|
||
using ()
|
||
renaming
|
||
( finiteHeightLattice to finiteHeightLatticeᵛ
|
||
; FiniteMap to VariableSigns
|
||
; _≈_ to _≈ᵛ_
|
||
; _⊔_ to _⊔ᵛ_
|
||
; ≈-dec to ≈ᵛ-dec
|
||
)
|
||
open FiniteHeightLattice finiteHeightLatticeᵛ
|
||
using ()
|
||
renaming
|
||
( ⊔-Monotonicˡ to ⊔ᵛ-Monotonicˡ
|
||
; ⊔-Monotonicʳ to ⊔ᵛ-Monotonicʳ
|
||
; _≼_ to _≼ᵛ_
|
||
; joinSemilattice to joinSemilatticeᵛ
|
||
; ⊔-idemp to ⊔ᵛ-idemp
|
||
)
|
||
|
||
⊥ᵛ = proj₁ (proj₁ (proj₁ (FiniteHeightLattice.fixedHeight finiteHeightLatticeᵛ)))
|
||
|
||
-- Finally, the map we care about is (state -> (variables -> sign)). Bring that in.
|
||
module StateVariablesFiniteMap = FixedHeightFiniteMap State VariableSigns _≟_ finiteHeightLatticeᵛ states-Unique ≈ᵛ-dec
|
||
open StateVariablesFiniteMap
|
||
using (_[_]; m₁≼m₂⇒m₁[ks]≼m₂[ks])
|
||
renaming
|
||
( finiteHeightLattice to finiteHeightLatticeᵐ
|
||
; FiniteMap to StateVariables
|
||
; isLattice to isLatticeᵐ
|
||
)
|
||
open FiniteHeightLattice finiteHeightLatticeᵐ
|
||
using ()
|
||
renaming (_≼_ to _≼ᵐ_)
|
||
|
||
-- 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
|
||
)
|