Tighten exported definitions in Forward.agda

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

Analysis/Forward.agda

@@ -38,6 +38,8 @@ module WithProg (prog : Program) where
 
     -- The variable -> abstract value (e.g. sign) map is a finite value-map
     -- with keys strings. Use a bundle to avoid explicitly specifying operators.
+    -- It's helpful to export these via 'public' since consumers tend to
+    -- use various variable lattice operations.
     module VariableValuesFiniteMap = Lattice.FiniteValueMap.WithKeys _≟ˢ_ isLatticeˡ vars
     open VariableValuesFiniteMap
         using ()
@@ -76,10 +78,11 @@ module WithProg (prog : Program) where
             ; ⊥-contains-bottoms to ⊥ᵛ-contains-bottoms
             )
 
-    ≈ᵛ-dec = ≈ˡ-dec⇒≈ᵛ-dec ≈ˡ-dec
-    joinSemilatticeᵛ = IsFiniteHeightLattice.joinSemilattice isFiniteHeightLatticeᵛ
-    fixedHeightᵛ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵛ
-    ⊥ᵛ = Chain.Height.⊥ fixedHeightᵛ
+    private
+        ≈ᵛ-dec = ≈ˡ-dec⇒≈ᵛ-dec ≈ˡ-dec
+        joinSemilatticeᵛ = IsFiniteHeightLattice.joinSemilattice isFiniteHeightLatticeᵛ
+        fixedHeightᵛ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵛ
+        ⊥ᵛ = Chain.Height.⊥ fixedHeightᵛ
 
     -- Finally, the map we care about is (state -> (variables -> value)). Bring that in.
     module StateVariablesFiniteMap = Lattice.FiniteValueMap.WithKeys _≟_ isLatticeᵛ states
@@ -96,7 +99,6 @@ module WithProg (prog : Program) where
             ; ≈₂-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
@@ -108,70 +110,79 @@ module WithProg (prog : Program) where
             ( ≈-sym to ≈ᵐ-sym
             )
 
-    ≈ᵐ-dec = ≈ᵛ-dec⇒≈ᵐ-dec ≈ᵛ-dec
-    fixedHeightᵐ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵐ
+    private
+        ≈ᵐ-dec = ≈ᵛ-dec⇒≈ᵐ-dec ≈ᵛ-dec
+        fixedHeightᵐ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵐ
 
-    -- We now have our (state -> (variables -> value)) map.
-    -- Define a couple of helpers to retrieve values from it. Specifically,
-    -- since the State type is as specific as possible, it's always possible to
-    -- retrieve the variable values at each state.
+        -- We now have our (state -> (variables -> value)) map.
+        -- Define a couple of helpers to retrieve values from it. Specifically,
+        -- since the State type is as specific as possible, it's always possible to
+        -- retrieve the variable values at each state.
 
-    states-in-Map : ∀ (s : State) (sv : StateVariables) → s ∈kᵐ sv
-    states-in-Map s sv@(m , ksv≡states) rewrite ksv≡states = states-complete s
+        states-in-Map : ∀ (s : State) (sv : StateVariables) → s ∈kᵐ sv
+        states-in-Map s sv@(m , ksv≡states) rewrite ksv≡states = states-complete s
 
-    variablesAt : State → StateVariables → VariableValues
-    variablesAt s sv = proj₁ (locateᵐ {s} {sv} (states-in-Map s sv))
+        variablesAt : State → StateVariables → VariableValues
+        variablesAt s sv = proj₁ (locateᵐ {s} {sv} (states-in-Map s sv))
 
-    variablesAt-∈ : ∀ (s : State) (sv : StateVariables) → (s , variablesAt s sv) ∈ᵐ sv
-    variablesAt-∈ s sv = proj₂ (locateᵐ {s} {sv} (states-in-Map s sv))
+        variablesAt-∈ : ∀ (s : State) (sv : StateVariables) → (s , variablesAt s sv) ∈ᵐ sv
+        variablesAt-∈ s sv = proj₂ (locateᵐ {s} {sv} (states-in-Map s sv))
 
-    variablesAt-≈ : ∀ s sv₁ sv₂ → sv₁ ≈ᵐ sv₂ → variablesAt s sv₁ ≈ᵛ variablesAt s sv₂
-    variablesAt-≈ s sv₁ sv₂ sv₁≈sv₂ =
-        m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ sv₁ sv₂ sv₁≈sv₂
-                               (states-in-Map s sv₁) (states-in-Map s sv₂)
+        variablesAt-≈ : ∀ s sv₁ sv₂ → sv₁ ≈ᵐ sv₂ → variablesAt s sv₁ ≈ᵛ variablesAt s sv₂
+        variablesAt-≈ s sv₁ sv₂ sv₁≈sv₂ =
+            m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ sv₁ sv₂ sv₁≈sv₂
+                                   (states-in-Map s sv₁) (states-in-Map s sv₂)
 
-    -- build up the 'join' function, which follows from Exercise 4.26's
-    --
-    --    L₁ → (A → L₂)
-    --
-    -- Construction, with L₁ = (A → L₂), and f = id
+        -- 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 ])
+        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)
+        -- 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ˡ
+        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
+        using ()
         renaming
             ( f' to joinAll
             ; f'-Monotonic to joinAll-Mono
             ; f'-k∈ks-≡ to joinAll-k∈ks-≡
             )
 
-    variablesAt-joinAll : ∀ (s : State) (sv : StateVariables) →
-                          variablesAt s (joinAll sv) ≡ joinForKey s sv
-    variablesAt-joinAll s sv
-        with (vs , s,vs∈usv) ← locateᵐ {s} {joinAll sv} (states-in-Map s (joinAll sv)) =
-        joinAll-k∈ks-≡ {l = sv} (states-complete s) s,vs∈usv
+    private
+        variablesAt-joinAll : ∀ (s : State) (sv : StateVariables) →
+                              variablesAt s (joinAll sv) ≡ joinForKey s sv
+        variablesAt-joinAll s sv
+            with (vs , s,vs∈usv) ← locateᵐ {s} {joinAll sv} (states-in-Map s (joinAll sv)) =
+            joinAll-k∈ks-≡ {l = sv} (states-complete s) s,vs∈usv
+
+    record Evaluator : Set where
+        field
+            eval : Expr → VariableValues → L
+            eval-Mono : ∀ (e : Expr) → Monotonic _≼ᵛ_ _≼ˡ_ (eval e)
 
     -- With 'join' in hand, we need to perform abstract evaluation.
-    module WithEvaluator (eval : Expr → VariableValues → L)
-                         (eval-Mono : ∀ (e : Expr) → Monotonic _≼ᵛ_ _≼ˡ_ (eval e)) where
+    private module WithEvaluator {{evaluator : Evaluator}} where
+        open Evaluator evaluator
 
         -- 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
+        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 ∷ [])
+                using ()
                 renaming
                     ( f' to updateVariablesFromExpression
                     ; f'-Monotonic to updateVariablesFromExpression-Mono
@@ -213,11 +224,13 @@ module WithProg (prog : Program) where
                             vs₁≼vs₂
 
         open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) updateVariablesForState updateVariablesForState-Monoʳ states
+            using ()
             renaming
                 ( f' to updateAll
                 ; f'-Monotonic to updateAll-Mono
                 ; f'-k∈ks-≡ to updateAll-k∈ks-≡
                 )
+            public
 
         -- Finally, the whole analysis consists of getting the 'join'
         -- of all incoming states, then applying the per-state evaluation
@@ -243,124 +256,148 @@ module WithProg (prog : Program) where
             with (vs , s,vs∈usv) ← locateᵐ {s} {updateAll sv} (states-in-Map s (updateAll sv)) =
             updateAll-k∈ks-≡ {l = sv} (states-complete s) s,vs∈usv
 
-        module WithInterpretation (latticeInterpretationˡ : LatticeInterpretation isLatticeˡ) where
-            open LatticeInterpretation latticeInterpretationˡ
-                using ()
-                renaming
-                    ( ⟦_⟧ to ⟦_⟧ˡ
-                    ; ⟦⟧-respects-≈ to ⟦⟧ˡ-respects-≈ˡ
-                    ; ⟦⟧-⊔-∨ to ⟦⟧ˡ-⊔ˡ-∨
-                    )
+    open WithEvaluator
+    open WithEvaluator using (result; analyze; result≈analyze-result) public
 
-            ⟦_⟧ᵛ : VariableValues → Env → Set
-            ⟦_⟧ᵛ vs ρ = ∀ {k l} → (k , l) ∈ᵛ vs → ∀ {v} → (k , v) Language.∈ ρ → ⟦ l ⟧ˡ v
+    private module WithInterpretation {{latticeInterpretationˡ : LatticeInterpretation isLatticeˡ}} where
+        open LatticeInterpretation latticeInterpretationˡ
+            using ()
+            renaming
+                ( ⟦_⟧ to ⟦_⟧ˡ
+                ; ⟦⟧-respects-≈ to ⟦⟧ˡ-respects-≈ˡ
+                ; ⟦⟧-⊔-∨ to ⟦⟧ˡ-⊔ˡ-∨
+                )
+            public
 
-            ⟦⊥ᵛ⟧ᵛ∅ : ⟦ ⊥ᵛ ⟧ᵛ []
-            ⟦⊥ᵛ⟧ᵛ∅ _ ()
+        ⟦_⟧ᵛ : VariableValues → Env → Set
+        ⟦_⟧ᵛ vs ρ = ∀ {k l} → (k , l) ∈ᵛ vs → ∀ {v} → (k , v) Language.∈ ρ → ⟦ l ⟧ˡ v
 
-            ⟦⟧ᵛ-respects-≈ᵛ : ∀ {vs₁ vs₂ : VariableValues} → vs₁ ≈ᵛ vs₂ → ⟦ vs₁ ⟧ᵛ ⇒ ⟦ vs₂ ⟧ᵛ
-            ⟦⟧ᵛ-respects-≈ᵛ {m₁ , _} {m₂ , _}
-                            (m₁⊆m₂ , m₂⊆m₁) ρ ⟦vs₁⟧ρ {k} {l} k,l∈m₂ {v} k,v∈ρ =
+        ⟦⊥ᵛ⟧ᵛ∅ : ⟦ ⊥ᵛ ⟧ᵛ []
+        ⟦⊥ᵛ⟧ᵛ∅ _ ()
+
+        ⟦⟧ᵛ-respects-≈ᵛ : ∀ {vs₁ vs₂ : VariableValues} → vs₁ ≈ᵛ vs₂ → ⟦ vs₁ ⟧ᵛ ⇒ ⟦ vs₂ ⟧ᵛ
+        ⟦⟧ᵛ-respects-≈ᵛ {m₁ , _} {m₂ , _}
+                        (m₁⊆m₂ , m₂⊆m₁) ρ ⟦vs₁⟧ρ {k} {l} k,l∈m₂ {v} k,v∈ρ =
+            let
+                (l' , (l≈l' , k,l'∈m₁)) = m₂⊆m₁ _ _ k,l∈m₂
+                ⟦l'⟧v = ⟦vs₁⟧ρ k,l'∈m₁ k,v∈ρ
+            in
+                ⟦⟧ˡ-respects-≈ˡ (≈ˡ-sym l≈l') v ⟦l'⟧v
+
+        ⟦⟧ᵛ-⊔ᵛ-∨ : ∀ {vs₁ vs₂ : VariableValues} → (⟦ vs₁ ⟧ᵛ ∨ ⟦ vs₂ ⟧ᵛ) ⇒ ⟦ vs₁ ⊔ᵛ vs₂ ⟧ᵛ
+        ⟦⟧ᵛ-⊔ᵛ-∨ {vs₁} {vs₂} ρ ⟦vs₁⟧ρ∨⟦vs₂⟧ρ {k} {l} k,l∈vs₁₂ {v} k,v∈ρ
+            with ((l₁ , l₂) , (refl , (k,l₁∈vs₁ , k,l₂∈vs₂)))
+                 ← Provenance-unionᵐ vs₁ vs₂ k,l∈vs₁₂
+            with ⟦vs₁⟧ρ∨⟦vs₂⟧ρ
+        ...   | inj₁ ⟦vs₁⟧ρ = ⟦⟧ˡ-⊔ˡ-∨ {l₁} {l₂} v (inj₁ (⟦vs₁⟧ρ k,l₁∈vs₁ k,v∈ρ))
+        ...   | inj₂ ⟦vs₂⟧ρ = ⟦⟧ˡ-⊔ˡ-∨ {l₁} {l₂} v (inj₂ (⟦vs₂⟧ρ k,l₂∈vs₂ k,v∈ρ))
+
+        ⟦⟧ᵛ-foldr : ∀ {vs : VariableValues} {vss : List VariableValues} {ρ : Env} →
+                    ⟦ vs ⟧ᵛ ρ → vs ∈ˡ vss → ⟦ foldr _⊔ᵛ_ ⊥ᵛ vss ⟧ᵛ ρ
+        ⟦⟧ᵛ-foldr {vs} {vs ∷ vss'} {ρ = ρ} ⟦vs⟧ρ (Any.here refl) =
+            ⟦⟧ᵛ-⊔ᵛ-∨ {vs₁ = vs} {vs₂ = foldr _⊔ᵛ_ ⊥ᵛ vss'} ρ (inj₁ ⟦vs⟧ρ)
+        ⟦⟧ᵛ-foldr {vs} {vs' ∷ vss'} {ρ = ρ} ⟦vs⟧ρ (Any.there vs∈vss') =
+            ⟦⟧ᵛ-⊔ᵛ-∨ {vs₁ = vs'} {vs₂ = foldr _⊔ᵛ_ ⊥ᵛ vss'} ρ
+                     (inj₂ (⟦⟧ᵛ-foldr ⟦vs⟧ρ vs∈vss'))
+
+    open WithInterpretation
+
+    module _ {{evaluator : Evaluator}} {{interpretation : LatticeInterpretation isLatticeˡ}} where
+        open Evaluator evaluator
+        open LatticeInterpretation interpretation
+
+        IsValid : Set
+        IsValid = ∀ {vs ρ e v} → ρ , e ⇒ᵉ v → ⟦ vs ⟧ᵛ ρ → ⟦ eval e vs ⟧ˡ v
+
+    record ValidInterpretation : Set₁ where
+        field
+            {{evaluator}} : Evaluator
+            {{interpretation}} : LatticeInterpretation isLatticeˡ
+
+        open Evaluator evaluator
+        open LatticeInterpretation interpretation
+
+        field
+            valid : IsValid
+
+    module WithValidInterpretation {{validInterpretation : ValidInterpretation}} where
+        open ValidInterpretation validInterpretation
+
+        updateVariablesFromStmt-matches : ∀ {bs vs ρ₁ ρ₂} → ρ₁ , bs ⇒ᵇ ρ₂ → ⟦ vs ⟧ᵛ ρ₁ → ⟦ updateVariablesFromStmt bs vs ⟧ᵛ ρ₂
+        updateVariablesFromStmt-matches {_} {vs} {ρ₁} {ρ₁} (⇒ᵇ-noop ρ₁) ⟦vs⟧ρ₁ = ⟦vs⟧ρ₁
+        updateVariablesFromStmt-matches {_} {vs} {ρ₁} {_} (⇒ᵇ-← ρ₁ k e v ρ,e⇒v) ⟦vs⟧ρ₁ {k'} {l} k',l∈vs' {v'} k',v'∈ρ₂
+            with k ≟ˢ k' | k',v'∈ρ₂
+        ...   | yes refl | here _ v _
+                rewrite updateVariablesFromExpression-k∈ks-≡ k e {l = vs} (Any.here refl) k',l∈vs' =
+                valid ρ,e⇒v ⟦vs⟧ρ₁
+        ...   | yes k≡k' | there _ _ _ _ _ k'≢k _ = ⊥-elim (k'≢k (sym k≡k'))
+        ...   | no k≢k' | here _ _ _ = ⊥-elim (k≢k' refl)
+        ...   | no k≢k'  | there _ _ _ _ _ _ k',v'∈ρ₁ =
                 let
-                    (l' , (l≈l' , k,l'∈m₁)) = m₂⊆m₁ _ _ k,l∈m₂
-                    ⟦l'⟧v = ⟦vs₁⟧ρ k,l'∈m₁ k,v∈ρ
+                    k'∉[k] = (λ { (Any.here refl) → k≢k' refl })
+                    k',l∈vs = updateVariablesFromExpression-k∉ks-backward k e {l = vs} k'∉[k] k',l∈vs'
                 in
-                    ⟦⟧ˡ-respects-≈ˡ (≈ˡ-sym l≈l') v ⟦l'⟧v
+                    ⟦vs⟧ρ₁ k',l∈vs k',v'∈ρ₁
 
-            ⟦⟧ᵛ-⊔ᵛ-∨ : ∀ {vs₁ vs₂ : VariableValues} → (⟦ vs₁ ⟧ᵛ ∨ ⟦ vs₂ ⟧ᵛ) ⇒ ⟦ vs₁ ⊔ᵛ vs₂ ⟧ᵛ
-            ⟦⟧ᵛ-⊔ᵛ-∨ {vs₁} {vs₂} ρ ⟦vs₁⟧ρ∨⟦vs₂⟧ρ {k} {l} k,l∈vs₁₂ {v} k,v∈ρ
-                with ((l₁ , l₂) , (refl , (k,l₁∈vs₁ , k,l₂∈vs₂)))
-                     ← Provenance-unionᵐ vs₁ vs₂ k,l∈vs₁₂
-                with ⟦vs₁⟧ρ∨⟦vs₂⟧ρ
-            ...   | inj₁ ⟦vs₁⟧ρ = ⟦⟧ˡ-⊔ˡ-∨ {l₁} {l₂} v (inj₁ (⟦vs₁⟧ρ k,l₁∈vs₁ k,v∈ρ))
-            ...   | inj₂ ⟦vs₂⟧ρ = ⟦⟧ˡ-⊔ˡ-∨ {l₁} {l₂} v (inj₂ (⟦vs₂⟧ρ k,l₂∈vs₂ k,v∈ρ))
+        updateVariablesFromStmt-fold-matches : ∀ {bss vs ρ₁ ρ₂} → ρ₁ , bss ⇒ᵇˢ ρ₂ → ⟦ vs ⟧ᵛ ρ₁ → ⟦ foldl (flip updateVariablesFromStmt) vs bss ⟧ᵛ ρ₂
+        updateVariablesFromStmt-fold-matches [] ⟦vs⟧ρ = ⟦vs⟧ρ
+        updateVariablesFromStmt-fold-matches {bs ∷ bss'} {vs} {ρ₁} {ρ₂} (ρ₁,bs⇒ρ ∷ ρ,bss'⇒ρ₂) ⟦vs⟧ρ₁ =
+            updateVariablesFromStmt-fold-matches
+                {bss'} {updateVariablesFromStmt bs vs} ρ,bss'⇒ρ₂
+                (updateVariablesFromStmt-matches ρ₁,bs⇒ρ ⟦vs⟧ρ₁)
 
-            ⟦⟧ᵛ-foldr : ∀ {vs : VariableValues} {vss : List VariableValues} {ρ : Env} →
-                        ⟦ vs ⟧ᵛ ρ → vs ∈ˡ vss → ⟦ foldr _⊔ᵛ_ ⊥ᵛ vss ⟧ᵛ ρ
-            ⟦⟧ᵛ-foldr {vs} {vs ∷ vss'} {ρ = ρ} ⟦vs⟧ρ (Any.here refl) =
-                ⟦⟧ᵛ-⊔ᵛ-∨ {vs₁ = vs} {vs₂ = foldr _⊔ᵛ_ ⊥ᵛ vss'} ρ (inj₁ ⟦vs⟧ρ)
-            ⟦⟧ᵛ-foldr {vs} {vs' ∷ vss'} {ρ = ρ} ⟦vs⟧ρ (Any.there vs∈vss') =
-                ⟦⟧ᵛ-⊔ᵛ-∨ {vs₁ = vs'} {vs₂ = foldr _⊔ᵛ_ ⊥ᵛ vss'} ρ
-                         (inj₂ (⟦⟧ᵛ-foldr ⟦vs⟧ρ vs∈vss'))
+        updateVariablesForState-matches : ∀ {s sv ρ₁ ρ₂} → ρ₁ , (code s) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s sv ⟧ᵛ ρ₁ → ⟦ updateVariablesForState s sv ⟧ᵛ ρ₂
+        updateVariablesForState-matches =
+            updateVariablesFromStmt-fold-matches
 
-            InterpretationValid : Set
-            InterpretationValid = ∀ {vs ρ e v} → ρ , e ⇒ᵉ v → ⟦ vs ⟧ᵛ ρ → ⟦ eval e vs ⟧ˡ v
-
-            module WithValidity (interpretationValidˡ : InterpretationValid) where
-
-                updateVariablesFromStmt-matches : ∀ {bs vs ρ₁ ρ₂} → ρ₁ , bs ⇒ᵇ ρ₂ → ⟦ vs ⟧ᵛ ρ₁ → ⟦ updateVariablesFromStmt bs vs ⟧ᵛ ρ₂
-                updateVariablesFromStmt-matches {_} {vs} {ρ₁} {ρ₁} (⇒ᵇ-noop ρ₁) ⟦vs⟧ρ₁ = ⟦vs⟧ρ₁
-                updateVariablesFromStmt-matches {_} {vs} {ρ₁} {_} (⇒ᵇ-← ρ₁ k e v ρ,e⇒v) ⟦vs⟧ρ₁ {k'} {l} k',l∈vs' {v'} k',v'∈ρ₂
-                    with k ≟ˢ k' | k',v'∈ρ₂
-                ...   | yes refl | here _ v _
-                        rewrite updateVariablesFromExpression-k∈ks-≡ k e {l = vs} (Any.here refl) k',l∈vs' =
-                        interpretationValidˡ ρ,e⇒v ⟦vs⟧ρ₁
-                ...   | yes k≡k' | there _ _ _ _ _ k'≢k _ = ⊥-elim (k'≢k (sym k≡k'))
-                ...   | no k≢k' | here _ _ _ = ⊥-elim (k≢k' refl)
-                ...   | no k≢k'  | there _ _ _ _ _ _ k',v'∈ρ₁ =
-                        let
-                            k'∉[k] = (λ { (Any.here refl) → k≢k' refl })
-                            k',l∈vs = updateVariablesFromExpression-k∉ks-backward k e {l = vs} k'∉[k] k',l∈vs'
-                        in
-                            ⟦vs⟧ρ₁ k',l∈vs k',v'∈ρ₁
-
-                updateVariablesFromStmt-fold-matches : ∀ {bss vs ρ₁ ρ₂} → ρ₁ , bss ⇒ᵇˢ ρ₂ → ⟦ vs ⟧ᵛ ρ₁ → ⟦ foldl (flip updateVariablesFromStmt) vs bss ⟧ᵛ ρ₂
-                updateVariablesFromStmt-fold-matches [] ⟦vs⟧ρ = ⟦vs⟧ρ
-                updateVariablesFromStmt-fold-matches {bs ∷ bss'} {vs} {ρ₁} {ρ₂} (ρ₁,bs⇒ρ ∷ ρ,bss'⇒ρ₂) ⟦vs⟧ρ₁ =
-                    updateVariablesFromStmt-fold-matches
-                        {bss'} {updateVariablesFromStmt bs vs} ρ,bss'⇒ρ₂
-                        (updateVariablesFromStmt-matches ρ₁,bs⇒ρ ⟦vs⟧ρ₁)
-
-                updateVariablesForState-matches : ∀ {s sv ρ₁ ρ₂} → ρ₁ , (code s) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s sv ⟧ᵛ ρ₁ → ⟦ updateVariablesForState s sv ⟧ᵛ ρ₂
-                updateVariablesForState-matches =
-                    updateVariablesFromStmt-fold-matches
-
-                updateAll-matches : ∀ {s sv ρ₁ ρ₂} → ρ₁ , (code s) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s sv ⟧ᵛ ρ₁ → ⟦ variablesAt s (updateAll sv) ⟧ᵛ ρ₂
-                updateAll-matches {s} {sv} ρ₁,bss⇒ρ₂ ⟦vs⟧ρ₁
-                    rewrite variablesAt-updateAll s sv =
-                    updateVariablesForState-matches {s} {sv} ρ₁,bss⇒ρ₂ ⟦vs⟧ρ₁
+        updateAll-matches : ∀ {s sv ρ₁ ρ₂} → ρ₁ , (code s) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s sv ⟧ᵛ ρ₁ → ⟦ variablesAt s (updateAll sv) ⟧ᵛ ρ₂
+        updateAll-matches {s} {sv} ρ₁,bss⇒ρ₂ ⟦vs⟧ρ₁
+            rewrite variablesAt-updateAll s sv =
+            updateVariablesForState-matches {s} {sv} ρ₁,bss⇒ρ₂ ⟦vs⟧ρ₁
 
 
-                stepTrace : ∀ {s₁ ρ₁ ρ₂} → ⟦ joinForKey s₁ result ⟧ᵛ ρ₁ → ρ₁ , (code s₁) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s₁ result ⟧ᵛ ρ₂
-                stepTrace {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ ρ₁,bss⇒ρ₂ =
-                        let
-                            -- I'd use rewrite, but Agda gets a memory overflow (?!).
-                            ⟦joinAll-result⟧ρ₁ =
-                                subst (λ vs → ⟦ vs ⟧ᵛ ρ₁)
-                                      (sym (variablesAt-joinAll s₁ result))
-                                      ⟦joinForKey-s₁⟧ρ₁
-                            ⟦analyze-result⟧ρ₂ =
-                                updateAll-matches {sv = joinAll result}
-                                                  ρ₁,bss⇒ρ₂ ⟦joinAll-result⟧ρ₁
-                            analyze-result≈result =
-                                ≈ᵐ-sym {result} {updateAll (joinAll result)}
-                                       result≈analyze-result
-                            analyze-s₁≈s₁ =
-                                variablesAt-≈ s₁ (updateAll (joinAll result))
-                                                 result (analyze-result≈result)
-                        in
-                            ⟦⟧ᵛ-respects-≈ᵛ {variablesAt s₁ (updateAll (joinAll result))} {variablesAt s₁ result} (analyze-s₁≈s₁) ρ₂ ⟦analyze-result⟧ρ₂
+        stepTrace : ∀ {s₁ ρ₁ ρ₂} → ⟦ joinForKey s₁ result ⟧ᵛ ρ₁ → ρ₁ , (code s₁) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s₁ result ⟧ᵛ ρ₂
+        stepTrace {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ ρ₁,bss⇒ρ₂ =
+                let
+                    -- I'd use rewrite, but Agda gets a memory overflow (?!).
+                    ⟦joinAll-result⟧ρ₁ =
+                        subst (λ vs → ⟦ vs ⟧ᵛ ρ₁)
+                              (sym (variablesAt-joinAll s₁ result))
+                              ⟦joinForKey-s₁⟧ρ₁
+                    ⟦analyze-result⟧ρ₂ =
+                        updateAll-matches {sv = joinAll result}
+                                          ρ₁,bss⇒ρ₂ ⟦joinAll-result⟧ρ₁
+                    analyze-result≈result =
+                        ≈ᵐ-sym {result} {updateAll (joinAll result)}
+                               result≈analyze-result
+                    analyze-s₁≈s₁ =
+                        variablesAt-≈ s₁ (updateAll (joinAll result))
+                                         result (analyze-result≈result)
+                in
+                    ⟦⟧ᵛ-respects-≈ᵛ {variablesAt s₁ (updateAll (joinAll result))} {variablesAt s₁ result} (analyze-s₁≈s₁) ρ₂ ⟦analyze-result⟧ρ₂
 
-                walkTrace : ∀ {s₁ s₂ ρ₁ ρ₂} → ⟦ joinForKey s₁ result ⟧ᵛ ρ₁ → Trace {graph} s₁ s₂ ρ₁ ρ₂ → ⟦ variablesAt s₂ result ⟧ᵛ ρ₂
-                walkTrace {s₁} {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ (Trace-single ρ₁,bss⇒ρ₂) =
-                    stepTrace {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ ρ₁,bss⇒ρ₂
-                walkTrace {s₁} {s₂} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ (Trace-edge {ρ₂ = ρ} {idx₂ = s} ρ₁,bss⇒ρ s₁→s₂ tr) =
-                    let
-                        ⟦result-s₁⟧ρ =
-                            stepTrace {s₁} {ρ₁} {ρ} ⟦joinForKey-s₁⟧ρ₁ ρ₁,bss⇒ρ
-                        s₁∈incomingStates =
-                            []-∈ result (edge⇒incoming s₁→s₂)
-                                        (variablesAt-∈ s₁ result)
-                        ⟦joinForKey-s⟧ρ =
-                            ⟦⟧ᵛ-foldr ⟦result-s₁⟧ρ s₁∈incomingStates
-                    in
-                        walkTrace ⟦joinForKey-s⟧ρ tr
+        walkTrace : ∀ {s₁ s₂ ρ₁ ρ₂} → ⟦ joinForKey s₁ result ⟧ᵛ ρ₁ → Trace {graph} s₁ s₂ ρ₁ ρ₂ → ⟦ variablesAt s₂ result ⟧ᵛ ρ₂
+        walkTrace {s₁} {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ (Trace-single ρ₁,bss⇒ρ₂) =
+            stepTrace {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ ρ₁,bss⇒ρ₂
+        walkTrace {s₁} {s₂} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ (Trace-edge {ρ₂ = ρ} {idx₂ = s} ρ₁,bss⇒ρ s₁→s₂ tr) =
+            let
+                ⟦result-s₁⟧ρ =
+                    stepTrace {s₁} {ρ₁} {ρ} ⟦joinForKey-s₁⟧ρ₁ ρ₁,bss⇒ρ
+                s₁∈incomingStates =
+                    []-∈ result (edge⇒incoming s₁→s₂)
+                                (variablesAt-∈ s₁ result)
+                ⟦joinForKey-s⟧ρ =
+                    ⟦⟧ᵛ-foldr ⟦result-s₁⟧ρ s₁∈incomingStates
+            in
+                walkTrace ⟦joinForKey-s⟧ρ tr
 
-                joinForKey-initialState-⊥ᵛ : joinForKey initialState result ≡ ⊥ᵛ
-                joinForKey-initialState-⊥ᵛ = cong (λ ins → foldr _⊔ᵛ_ ⊥ᵛ (result [ ins ])) initialState-pred-∅
+        joinForKey-initialState-⊥ᵛ : joinForKey initialState result ≡ ⊥ᵛ
+        joinForKey-initialState-⊥ᵛ = cong (λ ins → foldr _⊔ᵛ_ ⊥ᵛ (result [ ins ])) initialState-pred-∅
 
-                ⟦joinAll-initialState⟧ᵛ∅ : ⟦ joinForKey initialState result ⟧ᵛ []
-                ⟦joinAll-initialState⟧ᵛ∅ = subst (λ vs → ⟦ vs ⟧ᵛ []) (sym joinForKey-initialState-⊥ᵛ) ⟦⊥ᵛ⟧ᵛ∅
+        ⟦joinAll-initialState⟧ᵛ∅ : ⟦ joinForKey initialState result ⟧ᵛ []
+        ⟦joinAll-initialState⟧ᵛ∅ = subst (λ vs → ⟦ vs ⟧ᵛ []) (sym joinForKey-initialState-⊥ᵛ) ⟦⊥ᵛ⟧ᵛ∅
 
-                analyze-correct : ∀ {ρ : Env} → [] , rootStmt ⇒ˢ ρ → ⟦ variablesAt finalState result ⟧ᵛ ρ
-                analyze-correct {ρ} ∅,s⇒ρ = walkTrace {initialState} {finalState} {[]} {ρ} ⟦joinAll-initialState⟧ᵛ∅ (trace ∅,s⇒ρ)
+        analyze-correct : ∀ {ρ : Env} → [] , rootStmt ⇒ˢ ρ → ⟦ variablesAt finalState result ⟧ᵛ ρ
+        analyze-correct {ρ} ∅,s⇒ρ = walkTrace {initialState} {finalState} {[]} {ρ} ⟦joinAll-initialState⟧ᵛ∅ (trace ∅,s⇒ρ)
+
+    open WithValidInterpretation using (analyze-correct) public

Analysis/Sign.agda

@@ -159,19 +159,20 @@ s₁≢s₂⇒¬s₁∧s₂ { - } { - } +≢+ _ = ⊥-elim (+≢+ refl)
 ⟦⟧ᵍ-⊓ᵍ-∧ {[ g₁ ]ᵍ} {⊥ᵍ} x (_ , bot) = bot
 ⟦⟧ᵍ-⊓ᵍ-∧ {[ g₁ ]ᵍ} {⊤ᵍ} x (px₁ , _) = px₁
 
-latticeInterpretationᵍ : LatticeInterpretation isLatticeᵍ
-latticeInterpretationᵍ = record
-    { ⟦_⟧ = ⟦_⟧ᵍ
-    ; ⟦⟧-respects-≈ = ⟦⟧ᵍ-respects-≈ᵍ
-    ; ⟦⟧-⊔-∨ = ⟦⟧ᵍ-⊔ᵍ-∨
-    ; ⟦⟧-⊓-∧ = ⟦⟧ᵍ-⊓ᵍ-∧
-    }
+instance
+    latticeInterpretationᵍ : LatticeInterpretation isLatticeᵍ
+    latticeInterpretationᵍ = record
+        { ⟦_⟧ = ⟦_⟧ᵍ
+        ; ⟦⟧-respects-≈ = ⟦⟧ᵍ-respects-≈ᵍ
+        ; ⟦⟧-⊔-∨ = ⟦⟧ᵍ-⊔ᵍ-∨
+        ; ⟦⟧-⊓-∧ = ⟦⟧ᵍ-⊓ᵍ-∧
+        }
 
 module WithProg (prog : Program) where
     open Program prog
 
     module ForwardWithProg = Analysis.Forward.WithProg (record { isLattice = isLatticeᵍ; fixedHeight = fixedHeightᵍ }) ≈ᵍ-dec prog
-    open ForwardWithProg
+    open ForwardWithProg hiding (analyze-correct)
 
     eval : ∀ (e : Expr) → VariableValues → SignLattice
     eval (e₁ + e₂) vs = plus (eval e₁ vs) (eval e₂ vs)
@@ -222,15 +223,13 @@ module WithProg (prog : Program) where
     eval-Mono (# 0) _ = ≈ᵍ-refl
     eval-Mono (# (suc n')) _ = ≈ᵍ-refl
 
-    module ForwardWithEval = ForwardWithProg.WithEvaluator eval eval-Mono
-    open ForwardWithEval using (result)
+    instance
+        SignEval : Evaluator
+        SignEval = record { eval = eval; eval-Mono = eval-Mono }
 
     -- For debugging purposes, print out the result.
     output = show result
 
-    module ForwardWithInterp = ForwardWithEval.WithInterpretation latticeInterpretationᵍ
-    open ForwardWithInterp using (⟦_⟧ᵛ; InterpretationValid)
-
     -- This should have fewer cases -- the same number as the actual 'plus' above.
     -- But agda only simplifies on first argument, apparently, so we are stuck
     -- listing them all.
@@ -281,16 +280,16 @@ module WithProg (prog : Program) where
     minus-valid {[ 0ˢ ]ᵍ} {[ 0ˢ ]ᵍ} refl refl = refl
     minus-valid {[ 0ˢ ]ᵍ} {⊤ᵍ} _ _ = tt
 
-    eval-Valid : InterpretationValid
-    eval-Valid (⇒ᵉ-+ ρ e₁ e₂ z₁ z₂ ρ,e₁⇒z₁ ρ,e₂⇒z₂) ⟦vs⟧ρ =
-        plus-valid (eval-Valid ρ,e₁⇒z₁ ⟦vs⟧ρ) (eval-Valid ρ,e₂⇒z₂ ⟦vs⟧ρ)
-    eval-Valid (⇒ᵉ-- ρ e₁ e₂ z₁ z₂ ρ,e₁⇒z₁ ρ,e₂⇒z₂) ⟦vs⟧ρ =
-        minus-valid (eval-Valid ρ,e₁⇒z₁ ⟦vs⟧ρ) (eval-Valid ρ,e₂⇒z₂ ⟦vs⟧ρ)
-    eval-Valid {vs} (⇒ᵉ-Var ρ x v x,v∈ρ) ⟦vs⟧ρ
+    eval-valid : IsValid
+    eval-valid (⇒ᵉ-+ ρ e₁ e₂ z₁ z₂ ρ,e₁⇒z₁ ρ,e₂⇒z₂) ⟦vs⟧ρ =
+        plus-valid (eval-valid ρ,e₁⇒z₁ ⟦vs⟧ρ) (eval-valid ρ,e₂⇒z₂ ⟦vs⟧ρ)
+    eval-valid (⇒ᵉ-- ρ e₁ e₂ z₁ z₂ ρ,e₁⇒z₁ ρ,e₂⇒z₂) ⟦vs⟧ρ =
+        minus-valid (eval-valid ρ,e₁⇒z₁ ⟦vs⟧ρ) (eval-valid ρ,e₂⇒z₂ ⟦vs⟧ρ)
+    eval-valid {vs} (⇒ᵉ-Var ρ x v x,v∈ρ) ⟦vs⟧ρ
         with ∈k-decᵛ x (proj₁ (proj₁ vs))
     ...   | yes x∈kvs = ⟦vs⟧ρ (proj₂ (locateᵛ {x} {vs} x∈kvs)) x,v∈ρ
     ...   | no x∉kvs = tt
-    eval-Valid (⇒ᵉ-ℕ ρ 0) _ = refl
-    eval-Valid (⇒ᵉ-ℕ ρ (suc n')) _ = (n' , refl)
+    eval-valid (⇒ᵉ-ℕ ρ 0) _ = refl
+    eval-valid (⇒ᵉ-ℕ ρ (suc n')) _ = (n' , refl)
 
-    open ForwardWithInterp.WithValidity eval-Valid using (analyze-correct) public
+    analyze-correct = ForwardWithProg.analyze-correct