Analysis/Forward.agda

@@ -38,8 +38,6 @@ 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 ()
@@ -78,7 +76,6 @@ module WithProg (prog : Program) where
             ; ⊥-contains-bottoms to ⊥ᵛ-contains-bottoms
             )
 
-    private
     ≈ᵛ-dec = ≈ˡ-dec⇒≈ᵛ-dec ≈ˡ-dec
     joinSemilatticeᵛ = IsFiniteHeightLattice.joinSemilattice isFiniteHeightLatticeᵛ
     fixedHeightᵛ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵛ
@@ -99,6 +96,7 @@ 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
@@ -110,7 +108,6 @@ module WithProg (prog : Program) where
             ( ≈-sym to ≈ᵐ-sym
             )
 
-    private
     ≈ᵐ-dec = ≈ᵛ-dec⇒≈ᵐ-dec ≈ᵛ-dec
     fixedHeightᵐ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵐ
 
@@ -153,36 +150,28 @@ 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.
-    private module WithEvaluator {{evaluator : Evaluator}} where
-        open Evaluator evaluator
+    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.
 
-        module _ (k : String) (e : Expr) where
+        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 ∷ [])
-                using ()
                 renaming
                     ( f' to updateVariablesFromExpression
                     ; f'-Monotonic to updateVariablesFromExpression-Mono
@@ -224,13 +213,11 @@ 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
@@ -256,10 +243,7 @@ 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
 
-    open WithEvaluator
-    open WithEvaluator using (result; analyze; result≈analyze-result) public
-
-    private module WithInterpretation {{latticeInterpretationˡ : LatticeInterpretation isLatticeˡ}} where
+        module WithInterpretation (latticeInterpretationˡ : LatticeInterpretation isLatticeˡ) where
             open LatticeInterpretation latticeInterpretationˡ
                 using ()
                 renaming
@@ -267,7 +251,6 @@ 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
@@ -300,28 +283,10 @@ module WithProg (prog : Program) where
                 ⟦⟧ᵛ-⊔ᵛ-∨ {vs₁ = vs'} {vs₂ = foldr _⊔ᵛ_ ⊥ᵛ vss'} ρ
                          (inj₂ (⟦⟧ᵛ-foldr ⟦vs⟧ρ vs∈vss'))
 
-    open WithInterpretation
+            InterpretationValid : Set
+            InterpretationValid = ∀ {vs ρ e v} → ρ , e ⇒ᵉ v → ⟦ vs ⟧ᵛ ρ → ⟦ eval e vs ⟧ˡ v
 
-    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
+            module WithValidity (interpretationValidˡ : InterpretationValid) where
 
                 updateVariablesFromStmt-matches : ∀ {bs vs ρ₁ ρ₂} → ρ₁ , bs ⇒ᵇ ρ₂ → ⟦ vs ⟧ᵛ ρ₁ → ⟦ updateVariablesFromStmt bs vs ⟧ᵛ ρ₂
                 updateVariablesFromStmt-matches {_} {vs} {ρ₁} {ρ₁} (⇒ᵇ-noop ρ₁) ⟦vs⟧ρ₁ = ⟦vs⟧ρ₁
@@ -329,7 +294,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' =
-                valid ρ,e⇒v ⟦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'∈ρ₁ =
@@ -399,5 +364,3 @@ 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,9 +159,8 @@ s₁≢s₂⇒¬s₁∧s₂ { - } { - } +≢+ _ = ⊥-elim (+≢+ refl)
 ⟦⟧ᵍ-⊓ᵍ-∧ {[ g₁ ]ᵍ} {⊥ᵍ} x (_ , bot) = bot
 ⟦⟧ᵍ-⊓ᵍ-∧ {[ g₁ ]ᵍ} {⊤ᵍ} x (px₁ , _) = px₁
 
-instance
-    latticeInterpretationᵍ : LatticeInterpretation isLatticeᵍ
-    latticeInterpretationᵍ = record
+latticeInterpretationᵍ : LatticeInterpretation isLatticeᵍ
+latticeInterpretationᵍ = record
     { ⟦_⟧ = ⟦_⟧ᵍ
     ; ⟦⟧-respects-≈ = ⟦⟧ᵍ-respects-≈ᵍ
     ; ⟦⟧-⊔-∨ = ⟦⟧ᵍ-⊔ᵍ-∨
@@ -172,7 +171,7 @@ module WithProg (prog : Program) where
     open Program prog
 
     module ForwardWithProg = Analysis.Forward.WithProg (record { isLattice = isLatticeᵍ; fixedHeight = fixedHeightᵍ }) ≈ᵍ-dec prog
-    open ForwardWithProg hiding (analyze-correct)
+    open ForwardWithProg
 
     eval : ∀ (e : Expr) → VariableValues → SignLattice
     eval (e₁ + e₂) vs = plus (eval e₁ vs) (eval e₂ vs)
@@ -223,13 +222,15 @@ module WithProg (prog : Program) where
     eval-Mono (# 0) _ = ≈ᵍ-refl
     eval-Mono (# (suc n')) _ = ≈ᵍ-refl
 
-    instance
-        SignEval : Evaluator
-        SignEval = record { eval = eval; eval-Mono = eval-Mono }
+    module ForwardWithEval = ForwardWithProg.WithEvaluator eval eval-Mono
+    open ForwardWithEval using (result)
 
     -- 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.
@@ -280,16 +281,16 @@ module WithProg (prog : Program) where
     minus-valid {[ 0ˢ ]ᵍ} {[ 0ˢ ]ᵍ} refl refl = refl
     minus-valid {[ 0ˢ ]ᵍ} {⊤ᵍ} _ _ = tt
 
-    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⟧ρ
+    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⟧ρ
         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)
 
-    analyze-correct = ForwardWithProg.analyze-correct
+    open ForwardWithInterp.WithValidity eval-Valid using (analyze-correct) public