agda-spa/Analysis/Sign.agda

212 lines
8.5 KiB
Agda
Raw Normal View History

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.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 Language
open import Lattice
open import Utils using (Pairwise)
import Lattice.FiniteValueMap
data Sign : Set where
+ : Sign
- : Sign
: 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 ≈ᵍ-⊥ᵍ-⊥ᵍ
; ≈-- to ≈ᵍ-⊤ᵍ-⊤ᵍ
; ≈-lift to ≈ᵍ-lift
; ≈-refl to ≈ᵍ-refl
)
-- '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ᵍ
; fixedHeight to fixedHeightᵍ
; _≼_ to _≼ᵍ_
; _⊔_ to _⊔ᵍ_
)
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₁)
minus : SignLattice SignLattice SignLattice
minus ⊥ᵍ _ = ⊥ᵍ
minus _ ⊥ᵍ = ⊥ᵍ
minus ⊤ᵍ _ = ⊤ᵍ
minus _ ⊤ᵍ = ⊤ᵍ
minus [ + ]ᵍ [ + ]ᵍ = ⊤ᵍ
minus [ + ]ᵍ [ - ]ᵍ = [ + ]ᵍ
minus [ + ]ᵍ [ 0ˢ ]ᵍ = [ + ]ᵍ
minus [ - ]ᵍ [ + ]ᵍ = [ - ]ᵍ
minus [ - ]ᵍ [ - ]ᵍ = ⊤ᵍ
minus [ - ]ᵍ [ 0ˢ ]ᵍ = [ - ]ᵍ
minus [ 0ˢ ]ᵍ [ + ]ᵍ = [ - ]ᵍ
minus [ 0ˢ ]ᵍ [ - ]ᵍ = [ + ]ᵍ
minus [ 0ˢ ]ᵍ [ 0ˢ ]ᵍ = [ 0ˢ ]ᵍ
postulate minus-Monoˡ : (s₂ : SignLattice) Monotonic _≼ᵍ_ _≼ᵍ_ (λ s₁ minus s₁ s₂)
postulate minus-Monoʳ : (s₁ : SignLattice) Monotonic _≼ᵍ_ _≼ᵍ_ (minus 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 Lattice.FiniteValueMap.WithKeys _≟ˢ_ isLatticeᵍ vars
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ᵛ
)
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 _≼ᵐ_
)
open Lattice.FiniteValueMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight _≟_ isLatticeᵛ states-Unique ≈ᵛ-dec _ fixedHeightᵛ
using ()
renaming
( isFiniteHeightLattice to 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) ( 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')) _ _ = [ + ]ᵍ
updateForState : State StateVariables VariableSigns
updateForState s sv
with code s in p
... | k e =
let
(vs , s,vs∈sv) = locateᵐ {s} {sv} (states-in-Map s sv)
k∈e⇒k∈codes = λ k k∈e subst (λ stmt k ∈ᵗ stmt) (sym p) (in←₂ k∈e)
k∈e⇒k∈vars = λ k k∈e vars-complete s (k∈e⇒k∈codes k k∈e)
in
vs updatingᵛ (k []) via (λ _ eval e k∈e⇒k∈vars vs)
open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ (λ x x) (λ a₁≼a₂ a₁≼a₂) updateForState {!!} states
renaming
( f' to updateAll
; f'-Monotonic to updateAll-Mono
)