Analysis/Forward.agda

@@ -1,190 +0,0 @@
-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 -> 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 ()
-        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 -> value)). 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 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

Analysis/Sign.agda

@@ -1,16 +1,20 @@
 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.Empty using (⊥; ⊥-elim)
+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 (yes; no)
+open import Relation.Nullary using (¬_; Dec; yes; no)
+open import Data.Unit using (⊤)
+open import Function using (_∘_)
 
 open import Language
 open import Lattice
+open import Utils using (Pairwise)
 open import Showable using (Showable; show)
-import Analysis.Forward
+import Lattice.FiniteValueMap
 
 data Sign : Set where
     + : Sign
@@ -57,7 +61,8 @@ open import Lattice.AboveBelow Sign _≡_ (record { ≈-refl = refl; ≈-sym = s
 -- 'sign' has no underlying lattice structure, so use the 'plain' above-below lattice.
 open AB.Plain 0ˢ using ()
     renaming
-        ( isLattice to isLatticeᵍ
+        ( finiteHeightLattice to finiteHeightLatticeᵍ
+        ; isLattice to isLatticeᵍ
         ; fixedHeight to fixedHeightᵍ
         ; _≼_ to _≼ᵍ_
         ; _⊔_ to _⊔ᵍ_
@@ -109,59 +114,196 @@ postulate minus-Monoʳ : ∀ (s₁ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ
 module WithProg (prog : Program) where
     open Program prog
 
-    module ForwardWithProg = Analysis.Forward.WithProg (record { isLattice = isLatticeᵍ; fixedHeight = fixedHeightᵍ }) ≈ᵍ-dec prog
-    open ForwardWithProg
+    -- The variable -> sign map is a finite value-map with keys strings. Use a bundle to avoid explicitly specifying operators.
+    module VariableSignsFiniteMap = Lattice.FiniteValueMap.WithKeys _≟ˢ_ isLatticeᵍ vars
+    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]ᵛ
+            )
+    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ᵛ
+            )
 
-    eval : ∀ (e : Expr) → VariableValues → SignLattice
-    eval (e₁ + e₂) vs = plus (eval e₁ vs) (eval e₂ vs)
-    eval (e₁ - e₂) vs = minus (eval e₁ vs) (eval e₂ vs)
-    eval (` k) vs
-        with ∈k-decᵛ k (proj₁ (proj₁ vs))
-    ...   | yes k∈vs = proj₁ (locateᵛ {k} {vs} k∈vs)
-    ...   | no _ = ⊤ᵍ
-    eval (# 0) _ = [ 0ˢ ]ᵍ
-    eval (# (suc n')) _ = [ + ]ᵍ
+    ≈ᵛ-dec = ≈ᵍ-dec⇒≈ᵛ-dec ≈ᵍ-dec
+    joinSemilatticeᵛ = IsFiniteHeightLattice.joinSemilattice isFiniteHeightLatticeᵛ
+    fixedHeightᵛ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵛ
+    ⊥ᵛ = proj₁ (proj₁ (proj₁ fixedHeightᵛ))
 
-    eval-Mono : ∀ (e : Expr) → Monotonic _≼ᵛ_ _≼ᵍ_ (eval e)
-    eval-Mono (e₁ + e₂) {vs₁} {vs₂} vs₁≼vs₂ =
+    -- 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) → (∀ 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')) _ _ = [ + ]ᵍ
+
+    eval-Mono : ∀ (e : Expr) (k∈e⇒k∈vars : ∀ k → k ∈ᵉ e → k ∈ˡ vars) → Monotonic _≼ᵛ_ _≼ᵍ_ (eval e k∈e⇒k∈vars)
+    eval-Mono (e₁ + e₂) k∈e⇒k∈vars {vs₁} {vs₂} vs₁≼vs₂ =
         let
             -- TODO: can this be done with less boilerplate?
-            g₁vs₁ = eval e₁ vs₁
-            g₂vs₁ = eval e₂ vs₁
-            g₁vs₂ = eval e₁ vs₂
-            g₂vs₂ = eval e₂ vs₂
+            k∈e₁⇒k∈vars = λ k k∈e₁ → k∈e⇒k∈vars k (in⁺₁ k∈e₁)
+            k∈e₂⇒k∈vars = λ k k∈e₂ → k∈e⇒k∈vars k (in⁺₂ k∈e₂)
+            g₁vs₁ = eval e₁ k∈e₁⇒k∈vars vs₁
+            g₂vs₁ = eval e₂ k∈e₂⇒k∈vars vs₁
+            g₁vs₂ = eval e₁ k∈e₁⇒k∈vars vs₂
+            g₂vs₂ = eval e₂ k∈e₂⇒k∈vars vs₂
         in
             ≼ᵍ-trans
                 {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₁ {vs₁} {vs₂} vs₁≼vs₂))
-                (plus-Monoʳ g₁vs₂ {g₂vs₁} {g₂vs₂} (eval-Mono e₂ {vs₁} {vs₂} vs₁≼vs₂))
-    eval-Mono (e₁ - 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₂ k∈e₂⇒k∈vars {vs₁} {vs₂} vs₁≼vs₂))
+    eval-Mono (e₁ - e₂) k∈e⇒k∈vars {vs₁} {vs₂} vs₁≼vs₂ =
         let
             -- TODO: here too -- can this be done with less boilerplate?
-            g₁vs₁ = eval e₁ vs₁
-            g₂vs₁ = eval e₂ vs₁
-            g₁vs₂ = eval e₁ vs₂
-            g₂vs₂ = eval e₂ vs₂
+            k∈e₁⇒k∈vars = λ k k∈e₁ → k∈e⇒k∈vars k (in⁻₁ k∈e₁)
+            k∈e₂⇒k∈vars = λ k k∈e₂ → k∈e⇒k∈vars k (in⁻₂ k∈e₂)
+            g₁vs₁ = eval e₁ k∈e₁⇒k∈vars vs₁
+            g₂vs₁ = eval e₂ k∈e₂⇒k∈vars vs₁
+            g₁vs₂ = eval e₁ k∈e₁⇒k∈vars vs₂
+            g₂vs₂ = eval e₂ k∈e₂⇒k∈vars vs₂
         in
             ≼ᵍ-trans
                 {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₁ {vs₁} {vs₂} vs₁≼vs₂))
-                (minus-Monoʳ g₁vs₂ {g₂vs₁} {g₂vs₂} (eval-Mono e₂ {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₂ =
+                (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₂ k∈e₂⇒k∈vars {vs₁} {vs₂} vs₁≼vs₂))
+    eval-Mono (` k) k∈e⇒k∈vars {vs₁} {vs₂} vs₁≼vs₂ =
+        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₂} (vars-in-Map k vs₂ (k∈e⇒k∈vars k here))
+        in
+            m₁≼m₂⇒m₁[k]ᵛ≼m₂[k]ᵛ vs₁ vs₂ vs₁≼vs₂ k,v₁∈vs₁ k,v₂∈vs₂
+    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
+        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 ∷ [])
+            renaming
+                ( f' to updateVariablesFromExpression
+                ; f'-Monotonic to updateVariablesFromExpression-Mono
+                )
+            public
+
+    updateVariablesForState : State → StateVariables → VariableSigns
+    updateVariablesForState s sv
+        -- More weirdness here. Apparently, capturing the with-equality proof
+        -- using 'in p' makes code that reasons about this function (below)
+        -- 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
-                (v₁ , k,v₁∈vs₁) = locateᵛ {k} {vs₁} k∈kvs₁
-                (v₂ , k,v₂∈vs₂) = locateᵛ {k} {vs₂} k∈kvs₂
+                (vs , s,vs∈sv) = locateᵐ {s} {sv} (states-in-Map s sv)
             in
-                m₁≼m₂⇒m₁[k]ᵛ≼m₂[k]ᵛ vs₁ vs₂ vs₁≼vs₂ k,v₁∈vs₁ k,v₂∈vs₂
-    ...   | yes k∈kvs₁ | no k∉kvs₂ = ⊥-elim (k∉kvs₂ (subst (λ l → k ∈ˡ l) (all-equal-keysᵛ vs₁ vs₂) k∈kvs₁))
-    ...   | 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
+                updateVariablesFromExpression k e (λ k k∈e → k∈codes⇒k∈vars k (in←₂ k∈e)) vs
 
-    open ForwardWithProg.WithEvaluator eval eval-Mono using (result)
+    updateVariablesForState-Monoʳ : ∀ (s : State) → Monotonic _≼ᵐ_ _≼ᵛ_ (updateVariablesForState s)
+    updateVariablesForState-Monoʳ s {sv₁} {sv₂} sv₁≼sv₂
+        with code s | (λ k → vars-complete {k} s)
+    ...   | k ← e | k∈codes⇒k∈vars =
+            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 (λ k k∈e → k∈codes⇒k∈vars k (in←₂ k∈e)) {vs₁} {vs₂} vs₁≼vs₂
 
-    -- For debugging purposes, print out the result.
-    output = show result
+    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

Lattice/FiniteMap.agda

@@ -12,7 +12,7 @@ module Lattice.FiniteMap {a b : Level} {A : Set a} {B : Set b}
 
 open IsLattice lB using () renaming (_≼_ to _≼₂_)
 open import Lattice.Map ≡-dec-A lB as Map
-    using (Map; ⊔-equal-keys; ⊓-equal-keys)
+    using (Map; ⊔-equal-keys; ⊓-equal-keys; ∈k-dec)
     renaming
         ( _≈_ to _≈ᵐ_
         ; _⊔_ to _⊔ᵐ_
@@ -37,7 +37,6 @@ open import Lattice.Map ≡-dec-A lB as Map
         ; updating-via-keys-≡ to updatingᵐ-via-keys-≡
         ; f'-Monotonic to f'-Monotonicᵐ
         ; _≼_ to _≼ᵐ_
-        ; ∈k-dec to ∈k-decᵐ
         )
 open import Data.List.Membership.Propositional using () renaming (_∈_ to _∈ˡ_)
 open import Data.Product using (_×_; _,_; Σ; proj₁ ; proj₂)
@@ -83,8 +82,6 @@ module WithKeys (ks : List A) where
     _∈k_ : A → FiniteMap → Set a
     _∈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} {fm = (m , _)} k∈kfm = locateᵐ {k} {m} k∈kfm
 
@@ -185,7 +182,7 @@ module WithKeys (ks : List A) where
                           fm₁ ≼ fm₂ → Pairwise _≼₂_ (fm₁ [ ks' ]) (fm₂ [ 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₂
-        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₂ =
             let
                 (v₁ , k,v₁∈m₁) = locateᵐ {m = m₁} k∈km₁