Analysis/Sign.agda

@@ -1,19 +1,17 @@
 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.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 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 Data.Unit using (⊤)
-open import Function using (_∘_)
 
 open import Language
 open import Lattice
 open import Utils using (Pairwise)
-import Lattice.FiniteValueMap
+import Lattice.Bundles.FiniteValueMap
+
+private module FixedHeightFiniteMap = Lattice.Bundles.FiniteValueMap.FromFiniteHeightLattice
 
 data Sign : Set where
     + : Sign
@@ -32,133 +30,53 @@ _≟ᵍ_ 0ˢ + = no (λ ())
 _≟ᵍ_ 0ˢ - = no (λ ())
 _≟ᵍ_ 0ˢ 0ˢ = yes refl
 
--- 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
-        ; ⊥ to ⊥ᵍ
-        ; ⊤ to ⊤ᵍ
-        ; [_] to [_]ᵍ
-        ; _≈_ to _≈ᵍ_
-        ; ≈-⊥-⊥ to ≈ᵍ-⊥ᵍ-⊥ᵍ
-        ; ≈-⊤-⊤ to ≈ᵍ-⊤ᵍ-⊤ᵍ
-        ; ≈-lift to ≈ᵍ-lift
-        ; ≈-refl to ≈ᵍ-refl
-        )
--- 'sign' has no underlying lattice structure, so use the 'plain' above-below lattice.
-open AB.Plain 0ˢ using ()
-    renaming
-        ( finiteHeightLattice to finiteHeightLatticeᵍ
-        ; isLattice to isLatticeᵍ
-        ; fixedHeight to fixedHeightᵍ
-        ; _≼_ to _≼ᵍ_
-        ; _⊔_ to _⊔ᵍ_
-        )
-
-open IsLattice isLatticeᵍ using ()
-    renaming
-        ( ≼-trans to ≼ᵍ-trans
-        )
-
-plus : SignLattice → SignLattice → SignLattice
-plus ⊥ᵍ _ = ⊥ᵍ
-plus _ ⊥ᵍ = ⊥ᵍ
-plus ⊤ᵍ _ = ⊤ᵍ
-plus _ ⊤ᵍ = ⊤ᵍ
-plus [ + ]ᵍ [ + ]ᵍ = [ + ]ᵍ
-plus [ + ]ᵍ [ - ]ᵍ = ⊤ᵍ
-plus [ + ]ᵍ [ 0ˢ ]ᵍ = [ + ]ᵍ
-plus [ - ]ᵍ [ + ]ᵍ = ⊤ᵍ
-plus [ - ]ᵍ [ - ]ᵍ = [ - ]ᵍ
-plus [ - ]ᵍ [ 0ˢ ]ᵍ = [ - ]ᵍ
-plus [ 0ˢ ]ᵍ [ + ]ᵍ = [ + ]ᵍ
-plus [ 0ˢ ]ᵍ [ - ]ᵍ = [ - ]ᵍ
-plus [ 0ˢ ]ᵍ [ 0ˢ ]ᵍ = [ 0ˢ ]ᵍ
-
--- this is incredibly tedious: 125 cases per monotonicity proof, and tactics
--- are hard. postulate for now.
-postulate plus-Monoˡ : ∀ (s₂ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ_ (λ s₁ → plus s₁ s₂)
-postulate plus-Monoʳ : ∀ (s₁ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ_ (plus s₁)
-
-minus : SignLattice → SignLattice → SignLattice
-minus ⊥ᵍ _ = ⊥ᵍ
-minus _ ⊥ᵍ = ⊥ᵍ
-minus ⊤ᵍ _ = ⊤ᵍ
-minus _ ⊤ᵍ = ⊤ᵍ
-minus [ + ]ᵍ [ + ]ᵍ = ⊤ᵍ
-minus [ + ]ᵍ [ - ]ᵍ = [ + ]ᵍ
-minus [ + ]ᵍ [ 0ˢ ]ᵍ = [ + ]ᵍ
-minus [ - ]ᵍ [ + ]ᵍ = [ - ]ᵍ
-minus [ - ]ᵍ [ - ]ᵍ = ⊤ᵍ
-minus [ - ]ᵍ [ 0ˢ ]ᵍ = [ - ]ᵍ
-minus [ 0ˢ ]ᵍ [ + ]ᵍ = [ - ]ᵍ
-minus [ 0ˢ ]ᵍ [ - ]ᵍ = [ + ]ᵍ
-minus [ 0ˢ ]ᵍ [ 0ˢ ]ᵍ = [ 0ˢ ]ᵍ
-
-postulate minus-Monoˡ : ∀ (s₂ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ_ (λ s₁ → minus s₁ s₂)
-postulate minus-Monoʳ : ∀ (s₁ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ_ (minus s₁)
-
-module WithProg (prog : Program) where
+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)
+    -- 'sign' has no underlying lattice structure, so use the 'plain' above-below lattice.
+    open AB.Plain using () renaming (finiteHeightLattice to finiteHeightLatticeᵍ-if-inhabited)
+
+
+    finiteHeightLatticeᵍ = finiteHeightLatticeᵍ-if-inhabited 0ˢ
+
     -- 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
+    open FixedHeightFiniteMap String SignLattice _≟ˢ_ finiteHeightLatticeᵍ vars-Unique ≈ᵍ-dec
         using ()
         renaming
-            ( FiniteMap to VariableSigns
-            ; isLattice to isLatticeᵛ
+            ( finiteHeightLattice to finiteHeightLatticeᵛ
+            ; FiniteMap to VariableSigns
             ; _≈_ 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]ᵛ
+            ; ≈-dec to ≈ᵛ-dec
             )
-    open IsLattice isLatticeᵛ
+    open FiniteHeightLattice finiteHeightLatticeᵛ
         using ()
         renaming
             ( ⊔-Monotonicˡ to ⊔ᵛ-Monotonicˡ
             ; ⊔-Monotonicʳ to ⊔ᵛ-Monotonicʳ
+            ; _≼_ to _≼ᵛ_
+            ; joinSemilattice to joinSemilatticeᵛ
             ; ⊔-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ᵛ))
+    ⊥ᵛ = proj₁ (proj₁ (proj₁ (FiniteHeightLattice.fixedHeight finiteHeightLatticeᵛ)))
 
     -- Finally, the map we care about is (state -> (variables -> sign)). Bring that in.
-    module StateVariablesFiniteMap = Lattice.FiniteValueMap.WithKeys _≟_ isLatticeᵛ states
+    module StateVariablesFiniteMap = FixedHeightFiniteMap State VariableSigns _≟_ finiteHeightLatticeᵛ states-Unique ≈ᵛ-dec
     open StateVariablesFiniteMap
         using (_[_]; m₁≼m₂⇒m₁[ks]≼m₂[ks])
         renaming
-            ( FiniteMap to StateVariables
+            ( finiteHeightLattice to finiteHeightLatticeᵐ
+            ; 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ᵛ
+    open FiniteHeightLattice finiteHeightLatticeᵐ
         using ()
-        renaming
-            ( isFiniteHeightLattice to isFiniteHeightLatticeᵐ
-            )
-
-    ≈ᵐ-dec = ≈ᵛ-dec⇒≈ᵐ-dec ≈ᵛ-dec
-    fixedHeightᵐ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵐ
+        renaming (_≼_ to _≼ᵐ_)
 
     -- build up the 'join' function, which follows from Exercise 4.26's
     --
@@ -185,157 +103,3 @@ module WithProg (prog : Program) where
             ( 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?
-            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₁ 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?
-            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₁ 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
-                (vs , s,vs∈sv) = locateᵐ {s} {sv} (states-in-Map s sv)
-            in
-                updateVariablesFromExpression k e (λ k k∈e → k∈codes⇒k∈vars k (in←₂ k∈e)) vs
-
-    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₂
-
-    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.
-    open import Data.Fin using (suc; zero)
-    open import Data.Fin.Show using () renaming (show to showFin)
-    open import Data.Nat.Show using () renaming (show to showNat)
-    open import Data.String using (_++_)
-    open import Data.List using () renaming (length to lengthˡ)
-
-    showAboveBelow : AB.AboveBelow → String
-    showAboveBelow AB.⊤ = "⊤"
-    showAboveBelow AB.⊥ = "⊥"
-    showAboveBelow (AB.[_] +) = "+"
-    showAboveBelow (AB.[_] -) = "-"
-    showAboveBelow (AB.[_] 0ˢ) = "0"
-
-    showVarSigns : VariableSigns → String
-    showVarSigns ((kvs , _) , _) = "{" ++ foldr (λ (x , y) rest → x ++ " ↦ " ++ showAboveBelow y ++ ", " ++ rest) "" kvs ++ "}"
-
-    showStateVars : StateVariables → String
-    showStateVars ((kvs , _) , _) = "{" ++ foldr (λ (x , y) rest → (showFin x) ++ " ↦ " ++ showVarSigns y ++ ", " ++ rest) "" kvs ++ "}"
-
-    output = showStateVars signs
-
-
--- Debugging code: construct and run a program.
-open import Data.Vec using (Vec; _∷_; [])
-open import IO
-open import Level using (0ℓ)
-
-testCode : Vec Stmt _
-testCode =
-    ("zero" ← (# 0)) ∷
-    ("pos" ← ((` "zero") Expr.+ (# 1))) ∷
-    ("neg" ← ((` "zero") Expr.- (# 1))) ∷
-    ("unknown" ← ((` "pos") Expr.+ (` "neg"))) ∷
-    []
-
-testProgram : Program
-testProgram = record
-    { length = _
-    ; stmts = testCode
-    }
-
-open WithProg testProgram using (output)
-
-main = run {0ℓ} (putStrLn output)

Language.agda

@@ -3,19 +3,17 @@ 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; lookup)
 open import Data.List using ([]; _∷_; List) renaming (foldr to foldrˡ; map to mapˡ)
-open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_)
 open import Data.List.Relation.Unary.All using (All; []; _∷_)
-open import Data.List.Relation.Unary.Any as RelAny using ()
 open import Data.Fin using (Fin; suc; zero; fromℕ; inject₁) renaming (_≟_ to _≟ᶠ_)
 open import Data.Fin.Properties using (suc-injective)
-open import Relation.Binary.PropositionalEquality using (cong; _≡_; refl)
+open import Relation.Binary.PropositionalEquality using (cong; _≡_)
 open import Relation.Nullary using (¬_)
 open import Function using (_∘_)
 
 open import Lattice
-open import Utils using (Unique; Unique-map; empty; push; x∈xs⇒fx∈fxs)
+open import Utils using (Unique; Unique-map; empty; push)
 
 data Expr : Set where
     _+_ : Expr → Expr → Expr
@@ -26,116 +24,24 @@ data Expr : Set where
 data Stmt : Set where
     _←_ : String → Expr → Stmt
 
-open import Lattice.MapSet _≟ˢ_
+open import Lattice.MapSet String _≟ˢ_
     renaming
         ( MapSet to StringSet
         ; insert to insertˢ
         ; to-List to to-Listˢ
         ; empty to emptyˢ
-        ; singleton to singletonˢ
         ; _⊔_ to _⊔ˢ_
-        ; `_ to `ˢ_
-        ; _∈_ to _∈ˢ_
-        ; ⊔-preserves-∈k₁ to ⊔ˢ-preserves-∈k₁
-        ; ⊔-preserves-∈k₂ to ⊔ˢ-preserves-∈k₂
         )
 
-data _∈ᵉ_ : String → Expr → Set where
-    in⁺₁ : ∀ {e₁ e₂ : Expr} {k : String} → k ∈ᵉ e₁ → k ∈ᵉ (e₁ + e₂)
-    in⁺₂ : ∀ {e₁ e₂ : Expr} {k : String} → k ∈ᵉ e₂ → k ∈ᵉ (e₁ + e₂)
-    in⁻₁ : ∀ {e₁ e₂ : Expr} {k : String} → k ∈ᵉ e₁ → k ∈ᵉ (e₁ - e₂)
-    in⁻₂ : ∀ {e₁ e₂ : Expr} {k : String} → k ∈ᵉ e₂ → k ∈ᵉ (e₁ - e₂)
-    here : ∀ {k : String} → k ∈ᵉ (` k)
-
-data _∈ᵗ_ : String → Stmt → Set where
-    in←₁ : ∀ {k : String} {e : Expr} → k ∈ᵗ (k ← e)
-    in←₂ : ∀ {k k' : String} {e : Expr} → k ∈ᵉ e → k ∈ᵗ (k' ← e)
-
 private
     Expr-vars : Expr → StringSet
     Expr-vars (l + r) = Expr-vars l ⊔ˢ Expr-vars r
     Expr-vars (l - r) = Expr-vars l ⊔ˢ Expr-vars r
-    Expr-vars (` s) = singletonˢ s
+    Expr-vars (` s) = insertˢ s emptyˢ
     Expr-vars (# _) = emptyˢ
 
-    ∈-Expr-vars⇒∈ : ∀ {k : String} (e : Expr) → k ∈ˢ (Expr-vars e) → k ∈ᵉ e
-    ∈-Expr-vars⇒∈ {k} (e₁ + e₂) k∈vs
-        with Expr-Provenance k ((`ˢ (Expr-vars e₁)) ∪ (`ˢ (Expr-vars e₂))) k∈vs
-    ...   | in₁ (single k,tt∈vs₁) _ = (in⁺₁ (∈-Expr-vars⇒∈ e₁ (forget k,tt∈vs₁)))
-    ...   | in₂ _ (single k,tt∈vs₂) = (in⁺₂ (∈-Expr-vars⇒∈ e₂ (forget k,tt∈vs₂)))
-    ...   | bothᵘ (single k,tt∈vs₁) _ = (in⁺₁ (∈-Expr-vars⇒∈ e₁ (forget k,tt∈vs₁)))
-    ∈-Expr-vars⇒∈ {k} (e₁ - e₂) k∈vs
-        with Expr-Provenance k ((`ˢ (Expr-vars e₁)) ∪ (`ˢ (Expr-vars e₂))) k∈vs
-    ...   | in₁ (single k,tt∈vs₁) _ = (in⁻₁ (∈-Expr-vars⇒∈ e₁ (forget k,tt∈vs₁)))
-    ...   | in₂ _ (single k,tt∈vs₂) = (in⁻₂ (∈-Expr-vars⇒∈ e₂ (forget k,tt∈vs₂)))
-    ...   | bothᵘ (single k,tt∈vs₁) _ = (in⁻₁ (∈-Expr-vars⇒∈ e₁ (forget k,tt∈vs₁)))
-    ∈-Expr-vars⇒∈ {k} (` k) (RelAny.here refl) = here
-
-    ∈⇒∈-Expr-vars : ∀ {k : String} {e : Expr} → k ∈ᵉ e → k ∈ˢ (Expr-vars e)
-    ∈⇒∈-Expr-vars {k} {e₁ + e₂} (in⁺₁ k∈e₁) =
-        ⊔ˢ-preserves-∈k₁ {m₁ = Expr-vars e₁}
-                         {m₂ = Expr-vars e₂}
-                         (∈⇒∈-Expr-vars k∈e₁)
-    ∈⇒∈-Expr-vars {k} {e₁ + e₂} (in⁺₂ k∈e₂) =
-        ⊔ˢ-preserves-∈k₂ {m₁ = Expr-vars e₁}
-                         {m₂ = Expr-vars e₂}
-                         (∈⇒∈-Expr-vars k∈e₂)
-    ∈⇒∈-Expr-vars {k} {e₁ - e₂} (in⁻₁ k∈e₁) =
-        ⊔ˢ-preserves-∈k₁ {m₁ = Expr-vars e₁}
-                         {m₂ = Expr-vars e₂}
-                         (∈⇒∈-Expr-vars k∈e₁)
-    ∈⇒∈-Expr-vars {k} {e₁ - e₂} (in⁻₂ k∈e₂) =
-        ⊔ˢ-preserves-∈k₂ {m₁ = Expr-vars e₁}
-                         {m₂ = Expr-vars e₂}
-                         (∈⇒∈-Expr-vars k∈e₂)
-    ∈⇒∈-Expr-vars here = RelAny.here refl
-
     Stmt-vars : Stmt → StringSet
-    Stmt-vars (x ← e) = (singletonˢ x) ⊔ˢ (Expr-vars e)
-
-    ∈-Stmt-vars⇒∈ : ∀ {k : String} (s : Stmt) → k ∈ˢ (Stmt-vars s) → k ∈ᵗ s
-    ∈-Stmt-vars⇒∈ {k} (k' ← e) k∈vs
-        with Expr-Provenance k ((`ˢ (singletonˢ k')) ∪ (`ˢ (Expr-vars e))) k∈vs
-    ...   | in₁ (single (RelAny.here refl)) _ = in←₁
-    ...   | in₂ _ (single k,tt∈vs') = in←₂ (∈-Expr-vars⇒∈ e (forget k,tt∈vs'))
-    ...   | bothᵘ (single (RelAny.here refl)) _ = in←₁
-
-    ∈⇒∈-Stmt-vars : ∀ {k : String} {s : Stmt} → k ∈ᵗ s → k ∈ˢ (Stmt-vars s)
-    ∈⇒∈-Stmt-vars {k} {k ← e} in←₁ =
-        ⊔ˢ-preserves-∈k₁ {m₁ = singletonˢ k}
-                         {m₂ = Expr-vars e}
-                         (RelAny.here refl)
-    ∈⇒∈-Stmt-vars {k} {k' ← e} (in←₂ k∈e) =
-        ⊔ˢ-preserves-∈k₂ {m₁ = singletonˢ k'}
-                         {m₂ = Expr-vars e}
-                         (∈⇒∈-Expr-vars k∈e)
-
-    Stmts-vars : ∀ {n : ℕ} → Vec Stmt n → StringSet
-    Stmts-vars = foldr (λ n → StringSet)
-                       (λ {k} stmt acc → (Stmt-vars stmt) ⊔ˢ acc) emptyˢ
-
-    ∈-Stmts-vars⇒∈ : ∀ {n : ℕ} {k : String} (ss : Vec Stmt n) →
-                     k ∈ˢ (Stmts-vars ss) → Σ (Fin n) (λ f → k ∈ᵗ lookup ss f)
-    ∈-Stmts-vars⇒∈ {suc n'} {k} (s ∷ ss') k∈vss
-        with Expr-Provenance k ((`ˢ (Stmt-vars s)) ∪ (`ˢ (Stmts-vars ss'))) k∈vss
-    ...   | in₁ (single k,tt∈vs) _ = (zero , ∈-Stmt-vars⇒∈ s (forget k,tt∈vs))
-    ...   | in₂ _ (single k,tt∈vss') =
-            let
-                (f' , k∈s') = ∈-Stmts-vars⇒∈ ss' (forget k,tt∈vss')
-            in
-                (suc f' , k∈s')
-    ...   | bothᵘ (single k,tt∈vs) _ = (zero , ∈-Stmt-vars⇒∈ s (forget k,tt∈vs))
-
-    ∈⇒∈-Stmts-vars : ∀ {n : ℕ} {k : String} {ss : Vec Stmt n} {f : Fin n} →
-                     k ∈ᵗ lookup ss f → k ∈ˢ (Stmts-vars ss)
-    ∈⇒∈-Stmts-vars {suc n} {k} {s ∷ ss'} {zero} k∈s =
-        ⊔ˢ-preserves-∈k₁ {m₁ = Stmt-vars s}
-                         {m₂ = Stmts-vars ss'}
-                         (∈⇒∈-Stmt-vars k∈s)
-    ∈⇒∈-Stmts-vars {suc n} {k} {s ∷ ss'} {suc f'} k∈ss' =
-        ⊔ˢ-preserves-∈k₂ {m₁ = Stmt-vars s}
-                         {m₂ = Stmts-vars ss'}
-                         (∈⇒∈-Stmts-vars {n} {k} {ss'} {f'} k∈ss')
+    Stmt-vars (x ← e) = insertˢ x (Expr-vars e)
 
     -- Creating a new number from a natural number can never create one
     -- equal to one you get from weakening the bounds on another number.
@@ -156,10 +62,6 @@ private
             , push (z≢mapsfs inds') (Unique-map suc suc-injective unids')
             )
 
-    indices-complete : ∀ (n : ℕ) (f : Fin n) → f ∈ˡ (proj₁ (indices n))
-    indices-complete (suc n') zero = RelAny.here refl
-    indices-complete (suc n') (suc f') = RelAny.there (x∈xs⇒fx∈fxs suc (indices-complete n' f'))
-
 
 -- For now, just represent the program and CFG as one type, without branching.
 record Program : Set where
@@ -169,7 +71,8 @@ record Program : Set where
 
     private
         vars-Set : StringSet
-        vars-Set = Stmts-vars stmts
+        vars-Set = foldr (λ n → StringSet)
+                         (λ {k} stmt acc → (Stmt-vars stmt) ⊔ˢ acc) emptyˢ stmts
 
     vars : List String
     vars = to-Listˢ vars-Set
@@ -180,25 +83,19 @@ record Program : Set where
     State : Set
     State = Fin length
 
+    code : State → Stmt
+    code = lookup stmts
+
     states : List State
     states = proj₁ (indices length)
 
-    states-complete : ∀ (s : State) → s ∈ˡ states
-    states-complete = indices-complete length
-
     states-Unique : Unique states
     states-Unique = proj₂ (indices length)
 
-    code : State → Stmt
-    code = lookup stmts
-
-    vars-complete : ∀ {k : String} (s : State) → k ∈ᵗ (code s) → k ∈ˡ vars
-    vars-complete {k} s = ∈⇒∈-Stmts-vars {length} {k} {stmts} {s}
-
     _≟_ : IsDecidable (_≡_ {_} {State})
     _≟_ = _≟ᶠ_
 
-    -- Computations for incoming and outgoing edges will have to change too
+    -- Computations for incoming and outgoing edged  will have to change too
     -- when we support branching etc.
 
     incoming : State → List State

Lattice/AboveBelow.agda

@@ -68,10 +68,7 @@ data _≈_ : AboveBelow → AboveBelow → Set a where
 -- Any object can be wrapped in an 'above below' to make it a lattice,
 -- since ⊤ and ⊥ are the largest and least elements, and the rest are left
 -- unordered. That's what this module does.
---
--- For convenience, ask for the underlying type to always be inhabited, to
--- avoid requiring additional constraints in some of the proofs below.
-module Plain (x : A) where
+module Plain where
     _⊔_ : AboveBelow → AboveBelow → AboveBelow
     ⊥ ⊔ x = x
     ⊤ ⊔ x = ⊤
@@ -299,7 +296,7 @@ module Plain (x : A) where
         ; isLattice = isLattice
         }
 
-    open IsLattice isLattice using (_≼_; _≺_; ⊔-Monotonicˡ; ⊔-Monotonicʳ) public
+    open IsLattice isLattice using (_≼_; _≺_)
 
     ⊥≺[x] : ∀ (x : A) → ⊥ ≺ [ x ]
     ⊥≺[x] x = (≈-refl , λ ())
@@ -325,38 +322,36 @@ module Plain (x : A) where
 
     open Chain _≈_ ≈-equiv (IsLattice._≺_ isLattice) (IsLattice.≺-cong isLattice)
 
-    longestChain : Chain ⊥ ⊤ 2
-    longestChain = step (⊥≺[x] x) ≈-refl (step ([x]≺⊤ x) ≈-⊤-⊤ (done ≈-⊤-⊤))
+    module _ (x : A) where
+        longestChain : Chain ⊥ ⊤ 2
+        longestChain = step (⊥≺[x] x) ≈-refl (step ([x]≺⊤ x) ≈-⊤-⊤ (done ≈-⊤-⊤))
 
-    ¬-Chain-⊤ : ∀ {ab : AboveBelow} {n : ℕ} → ¬ Chain ⊤ ab (suc n)
-    ¬-Chain-⊤ {x} (step (⊤⊔x≈x , ⊤̷≈x) _ _) rewrite ⊤⊔x≡⊤ x = ⊥-elim (⊤̷≈x ⊤⊔x≈x)
+        ¬-Chain-⊤ : ∀ {ab : AboveBelow} {n : ℕ} → ¬ Chain ⊤ ab (suc n)
+        ¬-Chain-⊤ {x} (step (⊤⊔x≈x , ⊤̷≈x) _ _) rewrite ⊤⊔x≡⊤ x = ⊥-elim (⊤̷≈x ⊤⊔x≈x)
 
-    isLongest : ∀ {ab₁ ab₂ : AboveBelow} {n : ℕ} → Chain ab₁ ab₂ n → n ≤ 2
-    isLongest (done _) = z≤n
-    isLongest (step _ _ (done _)) = s≤s z≤n
-    isLongest (step _ _ (step _ _ (done _))) = s≤s (s≤s z≤n)
-    isLongest {⊤} c@(step _ _ _) = ⊥-elim (¬-Chain-⊤ c)
-    isLongest {[ x ]} (step {_} {y} [x]≺y y≈y' c@(step _ _ _))
-        rewrite [x]≺y⇒y≡⊤ x y [x]≺y with ≈-⊤-⊤ ← y≈y' = ⊥-elim (¬-Chain-⊤ c)
-    isLongest {⊥} (step {_} {⊥} (_ , ⊥̷≈⊥) _ _) = ⊥-elim (⊥̷≈⊥ ≈-⊥-⊥)
-    isLongest {⊥} (step {_} {⊤} _ ≈-⊤-⊤ c@(step _ _ _)) = ⊥-elim (¬-Chain-⊤ c)
-    isLongest {⊥} (step {_} {[ x ]} _ (≈-lift _) (step [x]≺y y≈z c@(step _ _ _)))
-        rewrite [x]≺y⇒y≡⊤ _ _ [x]≺y with ≈-⊤-⊤ ← y≈z = ⊥-elim (¬-Chain-⊤ c)
+        isLongest : ∀ {ab₁ ab₂ : AboveBelow} {n : ℕ} → Chain ab₁ ab₂ n → n ≤ 2
+        isLongest (done _) = z≤n
+        isLongest (step _ _ (done _)) = s≤s z≤n
+        isLongest (step _ _ (step _ _ (done _))) = s≤s (s≤s z≤n)
+        isLongest {⊤} c@(step _ _ _) = ⊥-elim (¬-Chain-⊤ c)
+        isLongest {[ x ]} (step {_} {y} [x]≺y y≈y' c@(step _ _ _))
+            rewrite [x]≺y⇒y≡⊤ x y [x]≺y with ≈-⊤-⊤ ← y≈y' = ⊥-elim (¬-Chain-⊤ c)
+        isLongest {⊥} (step {_} {⊥} (_ , ⊥̷≈⊥) _ _) = ⊥-elim (⊥̷≈⊥ ≈-⊥-⊥)
+        isLongest {⊥} (step {_} {⊤} _ ≈-⊤-⊤ c@(step _ _ _)) = ⊥-elim (¬-Chain-⊤ c)
+        isLongest {⊥} (step {_} {[ x ]} _ (≈-lift _) (step [x]≺y y≈z c@(step _ _ _)))
+            rewrite [x]≺y⇒y≡⊤ _ _ [x]≺y with ≈-⊤-⊤ ← y≈z = ⊥-elim (¬-Chain-⊤ c)
 
-    fixedHeight : IsLattice.FixedHeight isLattice 2
-    fixedHeight = (((⊥ , ⊤) , longestChain) , isLongest)
+        isFiniteHeightLattice : IsFiniteHeightLattice AboveBelow 2 _≈_ _⊔_ _⊓_
+        isFiniteHeightLattice = record
+            { isLattice = isLattice
+            ; fixedHeight = (((⊥ , ⊤) , longestChain) , isLongest)
+            }
 
-    isFiniteHeightLattice : IsFiniteHeightLattice AboveBelow 2 _≈_ _⊔_ _⊓_
-    isFiniteHeightLattice = record
-        { isLattice = isLattice
-        ; fixedHeight = fixedHeight
-        }
-
-    finiteHeightLattice : FiniteHeightLattice AboveBelow
-    finiteHeightLattice = record
-        { height = 2
-        ; _≈_ = _≈_
-        ; _⊔_ = _⊔_
-        ; _⊓_ = _⊓_
-        ; isFiniteHeightLattice = isFiniteHeightLattice
-        }
+        finiteHeightLattice : FiniteHeightLattice AboveBelow
+        finiteHeightLattice = record
+            { height = 2
+            ; _≈_ = _≈_
+            ; _⊔_ = _⊔_
+            ; _⊓_ = _⊓_
+            ; isFiniteHeightLattice = isFiniteHeightLattice
+            }

Lattice/Bundles/FiniteValueMap.agda

@@ -20,11 +20,11 @@ module FromFiniteHeightLattice (fhB : FiniteHeightLattice B)
         )
 
     import Lattice.FiniteMap
-    module FM = Lattice.FiniteMap ≡-dec-A isLattice₂
+    module FM = Lattice.FiniteMap A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A isLattice₂
     open FM.WithKeys ks public
 
     import Lattice.FiniteValueMap
-    module FVM = Lattice.FiniteValueMap ≡-dec-A isLattice₂
+    module FVM = Lattice.FiniteValueMap A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A isLattice₂
     open FVM.IterProdIsomorphism.WithUniqueKeysAndFixedHeight uks ≈₂-dec height₂ fixedHeight₂ public
 
     ≈-dec = ≈₂-dec⇒≈-dec ≈₂-dec

Lattice/FiniteMap.agda

@@ -4,15 +4,15 @@ open import Relation.Binary.PropositionalEquality as Eq
 open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
 open import Data.List using (List; _∷_; [])
 
-module Lattice.FiniteMap {a b : Level} {A : Set a} {B : Set b}
-    {_≈₂_ : B → B → Set b}
-    {_⊔₂_ : B → B → B} {_⊓₂_ : B → B → B}
+module Lattice.FiniteMap {a b : Level} (A : Set a) (B : Set b)
+    (_≈₂_ : B → B → Set b)
+    (_⊔₂_ : B → B → B) (_⊓₂_ : B → B → B)
     (≡-dec-A : IsDecidable (_≡_ {a} {A}))
     (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
 
 open IsLattice lB using () renaming (_≼_ to _≼₂_)
-open import Lattice.Map ≡-dec-A lB as Map
-    using (Map; ⊔-equal-keys; ⊓-equal-keys; ∈k-dec)
+open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB as Map
+    using (Map; ⊔-equal-keys; ⊓-equal-keys; ∈k-dec; m₁≼m₂⇒m₁[k]≼m₂[k])
     renaming
         ( _≈_ to _≈ᵐ_
         ; _⊔_ to _⊔ᵐ_
@@ -30,7 +30,6 @@ open import Lattice.Map ≡-dec-A lB as Map
         ; absorb-⊓-⊔ to absorb-⊓ᵐ-⊔ᵐ
         ; ≈-dec to ≈ᵐ-dec
         ; _[_] to _[_]ᵐ
-        ; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ
         ; locate to locateᵐ
         ; keys to keysᵐ
         ; _updating_via_ to _updatingᵐ_via_
@@ -70,15 +69,9 @@ module WithKeys (ks : List A) where
                 km₁≡ks
         )
 
-    _∈_ : A × B → FiniteMap → Set (a ⊔ℓ b)
-    _∈_ k,v (m₁ , _) = k,v ∈ˡ (proj₁ m₁)
-
     _∈k_ : A → FiniteMap → Set a
     _∈k_ k (m₁ , _) = k ∈ˡ (keysᵐ m₁)
 
-    locate : ∀ {k : A} {fm : FiniteMap} → k ∈k fm → Σ B (λ v → (k , v) ∈ fm)
-    locate {k} {fm = (m , _)} k∈kfm = locateᵐ {k} {m} k∈kfm
-
     _updating_via_ : FiniteMap → List A → (A → B) → FiniteMap
     _updating_via_ (m₁ , ksm₁≡ks) ks f =
         ( m₁ updatingᵐ ks via f
@@ -129,7 +122,7 @@ module WithKeys (ks : List A) where
         ; absorb-⊓-⊔ = λ (m₁ , _) (m₂ , _) → absorb-⊓ᵐ-⊔ᵐ m₁ m₂
         }
 
-    open IsLattice isLattice using (_≼_; ⊔-Monotonicˡ; ⊔-Monotonicʳ) public
+    open IsLattice isLattice using (_≼_) public
 
     lattice : Lattice FiniteMap
     lattice = record
@@ -139,10 +132,6 @@ module WithKeys (ks : List A) where
         ; isLattice = isLattice
         }
 
-    m₁≼m₂⇒m₁[k]≼m₂[k] : ∀ (fm₁ fm₂ : FiniteMap) {k : A} {v₁ v₂ : B} →
-                        fm₁ ≼ fm₂ → (k , v₁) ∈ fm₁ → (k , v₂) ∈ fm₂ → v₁ ≼₂ v₂
-    m₁≼m₂⇒m₁[k]≼m₂[k] (m₁ , _) (m₂ , _) m₁≼m₂ k,v₁∈m₁ k,v₂∈m₂ = m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ m₁ m₂ m₁≼m₂ k,v₁∈m₁ k,v₂∈m₂
-
     module GeneralizedUpdate
              {l} {L : Set l}
              {_≈ˡ_ : L → L → Set l} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L}
@@ -182,7 +171,7 @@ module WithKeys (ks : List A) where
                 (v₁ , k,v₁∈m₁) = locateᵐ {m = m₁} k∈km₁
                 (v₂ , k,v₂∈m₂) = locateᵐ {m = m₂} k∈km₂
             in
-                (m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ m₁ m₂ m₁≼m₂ k,v₁∈m₁ k,v₂∈m₂) ∷ m₁≼m₂⇒m₁[ks]≼m₂[ks] fm₁ fm₂ ks'' m₁≼m₂
+                (m₁≼m₂⇒m₁[k]≼m₂[k] m₁ m₂ m₁≼m₂ k,v₁∈m₁ k,v₂∈m₂) ∷ m₁≼m₂⇒m₁[ks]≼m₂[ks] fm₁ fm₂ ks'' m₁≼m₂
     ...   | no k∉km₁ | no k∉km₂ = m₁≼m₂⇒m₁[ks]≼m₂[ks] fm₁ fm₂ ks'' m₁≼m₂
     ...   | yes k∈km₁ | no k∉km₂ = ⊥-elim (∈k-exclusive fm₁ fm₂ (k∈km₁ , k∉km₂))
     ...   | no k∉km₁ | yes k∈km₂ = ⊥-elim (∈k-exclusive fm₂ fm₁ (k∈km₂ , k∉km₁))

Lattice/FiniteValueMap.agda

@@ -10,9 +10,9 @@ open import Relation.Binary.Definitions using (Decidable)
 open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
 open import Function.Definitions using (Inverseˡ; Inverseʳ)
 
-module Lattice.FiniteValueMap {A : Set} {B : Set}
-    {_≈₂_ : B → B → Set}
-    {_⊔₂_ : B → B → B} {_⊓₂_ : B → B → B}
+module Lattice.FiniteValueMap (A : Set) (B : Set)
+    (_≈₂_ : B → B → Set)
+    (_⊔₂_ : B → B → B) (_⊓₂_ : B → B → B)
     (≡-dec-A : Decidable (_≡_ {_} {A}))
     (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
 
@@ -29,10 +29,11 @@ open import Data.List.Relation.Unary.Any using (Any; here; there)
 open import Relation.Nullary using (¬_)
 open import Isomorphism using (IsInverseˡ; IsInverseʳ)
 
-open import Lattice.Map ≡-dec-A lB
+open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB
     using
         ( subset-impl
         ; locate; forget
+        ; _∈_
         ; Map-functional
         ; Expr-Provenance
         ; Expr-Provenance-≡
@@ -40,7 +41,7 @@ open import Lattice.Map ≡-dec-A lB
         ; in₁; in₂; bothᵘ; single
         ; ⊔-combines
         )
-open import Lattice.FiniteMap ≡-dec-A lB public
+open import Lattice.FiniteMap A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB public
 
 module IterProdIsomorphism where
     open import Data.Unit using (⊤; tt)
@@ -102,7 +103,7 @@ module IterProdIsomorphism where
         _⊔ⁱᵖ_ {ks} = IP._⊔_ (length ks)
 
         _∈ᵐ_ : ∀ {ks : List A} → A × B → FiniteMap ks → Set
-        _∈ᵐ_ {ks} = _∈_ ks
+        _∈ᵐ_ {ks} k,v fm = k,v ∈ proj₁ fm
 
     -- The left inverse is: from (to x) = x
     from-to-inverseˡ : ∀ {ks : List A} (uks : Unique ks) →
@@ -155,7 +156,7 @@ module IterProdIsomorphism where
 
     private
         first-key-in-map : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) →
-                           Σ B (λ v → (k , v) ∈ᵐ fm)
+                           Σ B (λ v → (k , v) ∈ proj₁ fm)
         first-key-in-map (((k , v) ∷ _ , _) , refl) = (v , here refl)
 
         from-first-value : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) →

Lattice/Map.agda

@@ -3,9 +3,9 @@ open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym;
 open import Relation.Binary.Definitions using (Decidable)
 open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
 
-module Lattice.Map {a b : Level} {A : Set a} {B : Set b}
-    {_≈₂_ : B → B → Set b}
-    {_⊔₂_ : B → B → B} {_⊓₂_ : B → B → B}
+module Lattice.Map {a b : Level} (A : Set a) (B : Set b)
+    (_≈₂_ : B → B → Set b)
+    (_⊔₂_ : B → B → B) (_⊓₂_ : B → B → B)
     (≡-dec-A : Decidable (_≡_ {a} {A}))
     (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
 
@@ -553,18 +553,11 @@ open ImplInsert _⊔₂_ using
     ; union-preserves-∈₂
     ; union-preserves-∉
     ; union-preserves-∈k₁
-    ; union-preserves-∈k₂
     )
 
 ⊔-combines : ∀ {k : A} {v₁ v₂ : B} {m₁ m₂ : Map} → (k , v₁) ∈ m₁ → (k , v₂) ∈ m₂ → (k , v₁ ⊔₂ v₂) ∈ (m₁ ⊔ m₂)
 ⊔-combines {k} {v₁} {v₂} {kvs₁ , u₁} {kvs₂ , u₂} k,v₁∈m₁ k,v₂∈m₂ = union-combines u₁ u₂ k,v₁∈m₁ k,v₂∈m₂
 
-⊔-preserves-∈k₁ : ∀ {k : A} → {m₁ m₂ : Map} → k ∈k m₁ → k ∈k (m₁ ⊔ m₂)
-⊔-preserves-∈k₁ {k} {(l₁ , _)} {(l₂ , _)} k∈km₁ = union-preserves-∈k₁ {l₁ = l₁} {l₂ = l₂} k∈km₁
-
-⊔-preserves-∈k₂ : ∀ {k : A} → {m₁ m₂ : Map} → k ∈k m₂ → k ∈k (m₁ ⊔ m₂)
-⊔-preserves-∈k₂ {k} {(l₁ , _)} {(l₂ , _)} k∈km₁ = union-preserves-∈k₂ {l₁ = l₁} {l₂ = l₂} k∈km₁
-
 open ImplInsert _⊓₂_ using
     ( restrict-needs-both
     ; updates

Lattice/MapSet.agda

@@ -3,31 +3,21 @@ open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym;
 open import Relation.Binary.Definitions using (Decidable)
 open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
 
-module Lattice.MapSet {a : Level} {A : Set a} (≡-dec-A : Decidable (_≡_ {a} {A})) where
+module Lattice.MapSet {a : Level} (A : Set a) (≡-dec-A : Decidable (_≡_ {a} {A})) where
 
 open import Data.List using (List; map)
-open import Data.Product using (_,_; proj₁)
+open import Data.Product using (proj₁)
 open import Function using (_∘_)
 
 open import Lattice.Unit using (⊤; tt) renaming (_≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_; isLattice to ⊤-isLattice)
 import Lattice.Map
 
-private module UnitMap = Lattice.Map ≡-dec-A ⊤-isLattice
-open UnitMap
-    using (Map; Expr; ⟦_⟧)
-    renaming
-        ( Expr-Provenance to Expr-Provenanceᵐ
-        )
-open UnitMap
-    using
-        ( _⊆_; _≈_; ≈-equiv; _⊔_; _⊓_; _∪_ ; _∩_ ; `_; empty; forget
-        ; isUnionSemilattice; isIntersectSemilattice; isLattice; lattice
-        ; Provenance
-        ; ⊔-preserves-∈k₁
-        ; ⊔-preserves-∈k₂
-        )
-    renaming (_∈k_ to _∈_) public
-open Provenance public
+private module UnitMap = Lattice.Map A ⊤ _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A ⊤-isLattice
+open UnitMap using (Map)
+open UnitMap using
+    ( _⊆_; _≈_; ≈-equiv; _⊔_; _⊓_; empty
+    ; isUnionSemilattice; isIntersectSemilattice; isLattice; lattice
+    ) public
 
 MapSet : Set a
 MapSet = Map
@@ -37,9 +27,3 @@ to-List = map proj₁ ∘ proj₁
 
 insert : A → MapSet → MapSet
 insert k = UnitMap.insert k tt
-
-singleton : A → MapSet
-singleton k = UnitMap.insert k tt empty
-
-Expr-Provenance : ∀ (k : A) (e : Expr) → k ∈ ⟦ e ⟧ → Provenance k tt e
-Expr-Provenance k e k∈e = let (tt , (prov , _)) = Expr-Provenanceᵐ k e k∈e in prov

Main.agda

@@ -0,0 +1,57 @@
+module Main where
+
+open import IO
+open import Level using (0ℓ)
+open import Data.Nat.Show using (show)
+open import Data.List using (List; _∷_; []; foldr)
+open import Data.String using (String; _++_) renaming (_≟_ to _≟ˢ_)
+open import Data.Unit using (⊤; tt) renaming (_≟_ to _≟ᵘ_)
+open import Data.Product using (_,_; _×_; proj₁; proj₂)
+open import Data.List.Relation.Unary.All using (_∷_; [])
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; subst; refl; trans)
+open import Relation.Nullary using (¬_)
+
+open import Utils using (Unique; push; empty)
+
+xyzw : List String
+xyzw = "x" ∷ "y" ∷ "z" ∷ "w" ∷ []
+
+xyzw-Unique : Unique xyzw
+xyzw-Unique = push ((λ ()) ∷ (λ ()) ∷ (λ ()) ∷ []) (push ((λ ()) ∷ (λ ()) ∷ []) (push ((λ ()) ∷ []) (push [] empty)))
+
+open import Lattice using (IsFiniteHeightLattice; FiniteHeightLattice; Monotonic)
+
+open import Lattice.AboveBelow ⊤ _≡_ (record { ≈-refl = refl; ≈-sym = sym; ≈-trans = trans }) _≟ᵘ_  as AB using () renaming (≈-dec to ≈ᵘ-dec)
+open AB.Plain using () renaming (finiteHeightLattice to finiteHeightLatticeᵘ)
+
+showAboveBelow : AB.AboveBelow → String
+showAboveBelow AB.⊤ = "⊤"
+showAboveBelow AB.⊥ = "⊥"
+showAboveBelow (AB.[_] tt) = "()"
+
+fhlᵘ = finiteHeightLatticeᵘ (Data.Unit.tt)
+
+import Lattice.Bundles.FiniteValueMap
+open Lattice.Bundles.FiniteValueMap.FromFiniteHeightLattice String AB.AboveBelow _≟ˢ_ fhlᵘ xyzw-Unique ≈ᵘ-dec using (FiniteMap; ≈-dec) renaming (finiteHeightLattice to fhlⁱᵖ)
+
+showMap : FiniteMap → String
+showMap ((kvs , _) , _) = "{" ++ foldr (λ (x , y) rest → x ++ " ↦ " ++ showAboveBelow y ++ ", " ++ rest) "" kvs ++ "}"
+
+open FiniteHeightLattice fhlⁱᵖ using (_≈_; _⊔_; _⊓_; ⊔-idemp; _≼_; ≈-⊔-cong; ≈-refl; ≈-trans; ≈-sym; ⊔-assoc; ⊔-comm; ⊔-Monotonicˡ)
+open import Relation.Binary.Reasoning.Base.Single _≈_ (λ {m} → ≈-refl {m}) (λ {m₁} {m₂} {m₃} → ≈-trans {m₁} {m₂} {m₃}) -- why am I having to eta-expand here?
+
+smallestMap = proj₁ (proj₁ (proj₁ (FiniteHeightLattice.fixedHeight fhlⁱᵖ)))
+largestMap = proj₂ (proj₁ (proj₁ (FiniteHeightLattice.fixedHeight fhlⁱᵖ)))
+
+dumb : FiniteMap
+dumb = ((("x" , AB.[_] tt) ∷ ("y" , AB.⊥) ∷ ("z" , AB.⊥) ∷ ("w" , AB.⊥) ∷ [] , xyzw-Unique) , refl)
+
+dumbFunction : FiniteMap → FiniteMap
+dumbFunction = _⊔_ dumb
+
+dumbFunction-Monotonic : Monotonic _≼_ _≼_ dumbFunction
+dumbFunction-Monotonic {m₁} {m₂} m₁≼m₂ = ⊔-Monotonicˡ dumb {m₁} {m₂} m₁≼m₂
+
+open import Fixedpoint {0ℓ} {FiniteMap} {8} {_≈_} {_⊔_} {_⊓_} ≈-dec (FiniteHeightLattice.isFiniteHeightLattice fhlⁱᵖ) dumbFunction (λ {m₁} {m₂} m₁≼m₂ → dumbFunction-Monotonic {m₁} {m₂} m₁≼m₂)
+
+main = run {0ℓ} (putStrLn (showMap aᶠ))

Utils.agda

@@ -54,11 +54,6 @@ All-x∈xs : ∀ {a} {A : Set a} (xs : List A) → All (λ x → x ∈ xs) xs
 All-x∈xs [] = []
 All-x∈xs (x ∷ xs') = here refl ∷ map there (All-x∈xs xs')
 
-x∈xs⇒fx∈fxs : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) {x : A} {xs : List A} →
-              x ∈ xs → (f x) ∈ mapˡ f xs
-x∈xs⇒fx∈fxs f (here refl) = here refl
-x∈xs⇒fx∈fxs f (there x∈xs') = there (x∈xs⇒fx∈fxs f x∈xs')
-
 iterate : ∀ {a} {A : Set a} (n : ℕ) → (f : A → A) → A → A
 iterate 0 _ a = a
 iterate (suc n) f a = f (iterate n f a)