Analysis/Sign.agda

@@ -1,14 +1,11 @@
 module Analysis.Sign where
 
 open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
-open import Data.Product using (proj₁)
-open import Data.List using (foldr)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans)
 open import Relation.Nullary using (¬_; Dec; yes; no)
 
 open import Language
 open import Lattice
-open import Utils using (Pairwise)
 import Lattice.Bundles.FiniteValueMap
 
 private module FixedHeightFiniteMap = Lattice.Bundles.FiniteValueMap.FromFiniteHeightLattice
@@ -34,9 +31,7 @@ module _ (prog : Program) where
     open Program prog
 
     -- 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)
+    open import Lattice.AboveBelow Sign _≡_ (record { ≈-refl = refl; ≈-sym = sym; ≈-trans = trans }) _≟ᵍ_ as AB renaming (AboveBelow to SignLattice; ≈-dec to ≈ᵍ-dec)
     -- 'sign' has no underlying lattice structure, so use the 'plain' above-below lattice.
     open AB.Plain using () renaming (finiteHeightLattice to finiteHeightLatticeᵍ-if-inhabited)
 
@@ -45,61 +40,16 @@ module _ (prog : Program) where
 
     -- The variable -> sign map is a finite value-map with keys strings. Use a bundle to avoid explicitly specifying operators.
     open FixedHeightFiniteMap String SignLattice _≟ˢ_ finiteHeightLatticeᵍ vars-Unique ≈ᵍ-dec
-        using ()
         renaming
             ( finiteHeightLattice to finiteHeightLatticeᵛ
             ; FiniteMap to VariableSigns
             ; _≈_ to _≈ᵛ_
-            ; _⊔_ to _⊔ᵛ_
             ; ≈-dec to ≈ᵛ-dec
             )
-    open FiniteHeightLattice finiteHeightLatticeᵛ
-        using ()
-        renaming
-            ( ⊔-Monotonicˡ to ⊔ᵛ-Monotonicˡ
-            ; ⊔-Monotonicʳ to ⊔ᵛ-Monotonicʳ
-            ; _≼_ to _≼ᵛ_
-            ; joinSemilattice to joinSemilatticeᵛ
-            ; ⊔-idemp to ⊔ᵛ-idemp
-            )
-
-    ⊥ᵛ = proj₁ (proj₁ (proj₁ (FiniteHeightLattice.fixedHeight finiteHeightLatticeᵛ)))
 
     -- Finally, the map we care about is (state -> (variables -> sign)). Bring that in.
-    module StateVariablesFiniteMap = FixedHeightFiniteMap State VariableSigns _≟_ finiteHeightLatticeᵛ states-Unique ≈ᵛ-dec
-    open StateVariablesFiniteMap
-        using (_[_]; m₁≼m₂⇒m₁[ks]≼m₂[ks])
+    open FixedHeightFiniteMap State VariableSigns _≟_ finiteHeightLatticeᵛ states-Unique ≈ᵛ-dec
         renaming
             ( finiteHeightLattice to finiteHeightLatticeᵐ
             ; FiniteMap to StateVariables
-            ; isLattice to isLatticeᵐ
-            )
-    open FiniteHeightLattice finiteHeightLatticeᵐ
-        using ()
-        renaming (_≼_ to _≼ᵐ_)
-
-    -- 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
             )

Language.agda

@@ -3,7 +3,7 @@ module Language where
 open import Data.Nat using (ℕ; suc; pred)
 open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
 open import Data.Product using (Σ; _,_; proj₁; proj₂)
-open import Data.Vec using (Vec; foldr; lookup)
+open import Data.Vec using (Vec; foldr)
 open import Data.List using ([]; _∷_; List) renaming (foldr to foldrˡ; map to mapˡ)
 open import Data.List.Relation.Unary.All using (All; []; _∷_)
 open import Data.Fin using (Fin; suc; zero; fromℕ; inject₁) renaming (_≟_ to _≟ᶠ_)
@@ -83,9 +83,6 @@ record Program : Set where
     State : Set
     State = Fin length
 
-    code : State → Stmt
-    code = lookup stmts
-
     states : List State
     states = proj₁ (indices length)
 
@@ -94,15 +91,3 @@ record Program : Set where
 
     _≟_ : IsDecidable (_≡_ {_} {State})
     _≟_ = _≟ᶠ_
-
-    -- Computations for incoming and outgoing edged  will have to change too
-    -- when we support branching etc.
-
-    incoming : State → List State
-    incoming
-        with length
-    ...   | 0 = (λ ())
-    ...   | suc n' = (λ
-            { zero → []
-            ; (suc f') → (inject₁ f') ∷ []
-            })

Lattice.agda

@@ -124,7 +124,7 @@ module _ {a} {A : Set a}
     open IsSemilattice lA using (_≼_)
 
     id-Mono : Monotonic _≼_ _≼_ (λ x → x)
-    id-Mono {a₁} {a₂} a₁≼a₂ = a₁≼a₂
+    id-Mono a₁≼a₂ = a₁≼a₂
 
 module _ {a b} {A : Set a} {B : Set b}
          {_≈₁_ : A → A → Set a} {_⊔₁_ : A → A → A}

Lattice/FiniteMap.agda

@@ -132,24 +132,23 @@ module WithKeys (ks : List A) where
         ; isLattice = isLattice
         }
 
-    module GeneralizedUpdate
-             {l} {L : Set l}
+    module _ {l} {L : Set l}
              {_≈ˡ_ : L → L → Set l} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L}
-             (lL : IsLattice L _≈ˡ_ _⊔ˡ_ _⊓ˡ_)
-             (f : L → FiniteMap) (f-Monotonic : Monotonic (IsLattice._≼_ lL) _≼_ f)
-             (g : A → L → B) (g-Monotonicʳ : ∀ k → Monotonic (IsLattice._≼_ lL) _≼₂_ (g k))
-             (ks : List A) where
-
+             (lL : IsLattice L _≈ˡ_ _⊔ˡ_ _⊓ˡ_) where
         open IsLattice lL using () renaming (_≼_ to _≼ˡ_)
 
-        updater : L → A → B
-        updater l k = g k l
+        module _ (f : L → FiniteMap) (f-Monotonic : Monotonic _≼ˡ_ _≼_ f)
+                 (g : A → L → B) (g-Monotonicʳ : ∀ k → Monotonic _≼ˡ_ _≼₂_ (g k))
+                 (ks : List A) where
 
-        f' : L → FiniteMap
-        f' l = (f l) updating ks via (updater l)
+            updater : L → A → B
+            updater l k = g k l
 
-        f'-Monotonic : Monotonic _≼ˡ_ _≼_ f'
-        f'-Monotonic {l₁} {l₂} l₁≼l₂ = f'-Monotonicᵐ lL (proj₁ ∘ f) f-Monotonic g g-Monotonicʳ ks l₁≼l₂
+            f' : L → FiniteMap
+            f' l = (f l) updating ks via (updater l)
+
+            f'-Monotonic : Monotonic _≼ˡ_ _≼_ f'
+            f'-Monotonic {l₁} {l₂} l₁≼l₂ = f'-Monotonicᵐ lL (proj₁ ∘ f) f-Monotonic g g-Monotonicʳ ks l₁≼l₂
 
     all-equal-keys : ∀ (fm₁ fm₂ : FiniteMap) → (Map.keys (proj₁ fm₁) ≡ Map.keys (proj₁ fm₂))
     all-equal-keys (fm₁ , km₁≡ks) (fm₂ , km₂≡ks) = trans km₁≡ks (sym km₂≡ks)