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,6 +78,7 @@ module WithProg (prog : Program) where
             ; ⊥-contains-bottoms to ⊥ᵛ-contains-bottoms
             )
 
+    private
         ≈ᵛ-dec = ≈ˡ-dec⇒≈ᵛ-dec ≈ˡ-dec
         joinSemilatticeᵛ = IsFiniteHeightLattice.joinSemilattice isFiniteHeightLatticeᵛ
         fixedHeightᵛ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵛ
@@ -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,6 +110,7 @@ module WithProg (prog : Program) where
             ( ≈-sym to ≈ᵐ-sym
             )
 
+    private
         ≈ᵐ-dec = ≈ᵛ-dec⇒≈ᵐ-dec ≈ᵛ-dec
         fixedHeightᵐ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵐ
 
@@ -150,28 +153,36 @@ module WithProg (prog : Program) where
 
     -- 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-≡
             )
 
+    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)
+    private module WithEvaluator {{evaluator : Evaluator}} where
-                         (eval-Mono : ∀ (e : Expr) → Monotonic _≼ᵛ_ _≼ˡ_ (eval e)) 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,7 +256,10 @@ 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 WithEvaluator
+    open WithEvaluator using (result; analyze; result≈analyze-result) public
+
+    private module WithInterpretation {{latticeInterpretationˡ : LatticeInterpretation isLatticeˡ}} where
         open LatticeInterpretation latticeInterpretationˡ
             using ()
             renaming
@@ -251,6 +267,7 @@ module WithProg (prog : Program) where
                 ; ⟦⟧-respects-≈ to ⟦⟧ˡ-respects-≈ˡ
                 ; ⟦⟧-⊔-∨ to ⟦⟧ˡ-⊔ˡ-∨
                 )
+            public
 
         ⟦_⟧ᵛ : VariableValues → Env → Set
         ⟦_⟧ᵛ vs ρ = ∀ {k l} → (k , l) ∈ᵛ vs → ∀ {v} → (k , v) Language.∈ ρ → ⟦ l ⟧ˡ v
@@ -283,10 +300,28 @@ module WithProg (prog : Program) where
             ⟦⟧ᵛ-⊔ᵛ-∨ {vs₁ = vs'} {vs₂ = foldr _⊔ᵛ_ ⊥ᵛ vss'} ρ
                      (inj₂ (⟦⟧ᵛ-foldr ⟦vs⟧ρ vs∈vss'))
 
-            InterpretationValid : Set
+    open WithInterpretation
-            InterpretationValid = ∀ {vs ρ e v} → ρ , e ⇒ᵉ v → ⟦ vs ⟧ᵛ ρ → ⟦ eval e vs ⟧ˡ v
 
-            module WithValidity (interpretationValidˡ : InterpretationValid) where
+    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⟧ρ₁
@@ -294,7 +329,7 @@ module WithProg (prog : Program) where
             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⟧ρ₁
+                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'∈ρ₁ =
@@ -364,3 +399,5 @@ module WithProg (prog : Program) where
 
         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,6 +159,7 @@ s₁≢s₂⇒¬s₁∧s₂ { - } { - } +≢+ _ = ⊥-elim (+≢+ refl)
 ⟦⟧ᵍ-⊓ᵍ-∧ {[ g₁ ]ᵍ} {⊥ᵍ} x (_ , bot) = bot
 ⟦⟧ᵍ-⊓ᵍ-∧ {[ g₁ ]ᵍ} {⊤ᵍ} x (px₁ , _) = px₁
 
+instance
     latticeInterpretationᵍ : LatticeInterpretation isLatticeᵍ
     latticeInterpretationᵍ = record
         { ⟦_⟧ = ⟦_⟧ᵍ
@@ -171,7 +172,7 @@ 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
+    instance
-    open ForwardWithEval using (result)
+        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 : IsValid
-    eval-Valid (⇒ᵉ-+ ρ e₁ e₂ z₁ z₂ ρ,e₁⇒z₁ ρ,e₂⇒z₂) ⟦vs⟧ρ =
+    eval-valid (⇒ᵉ-+ ρ e₁ e₂ z₁ z₂ ρ,e₁⇒z₁ ρ,e₂⇒z₂) ⟦vs⟧ρ =
-        plus-valid (eval-Valid ρ,e₁⇒z₁ ⟦vs⟧ρ) (eval-Valid ρ,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⟧ρ =
+    eval-valid (⇒ᵉ-- ρ e₁ e₂ z₁ z₂ ρ,e₁⇒z₁ ρ,e₂⇒z₂) ⟦vs⟧ρ =
-        minus-valid (eval-Valid ρ,e₁⇒z₁ ⟦vs⟧ρ) (eval-Valid ρ,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 {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 (⇒ᵉ-ℕ ρ 0) _ = refl
-    eval-Valid (⇒ᵉ-ℕ ρ (suc n')) _ = (n' , refl)
+    eval-valid (⇒ᵉ-ℕ ρ (suc n')) _ = (n' , refl)
 
-    open ForwardWithInterp.WithValidity eval-Valid using (analyze-correct) public
+    analyze-correct = ForwardWithProg.analyze-correct