Add some debugging code to sign analysis to print the results

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

Analysis/Sign.agda

@@ -1,17 +1,19 @@
 module Analysis.Sign where
 
 open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
-open import Data.Product using (proj₁)
+open import Data.Nat using (suc)
-open import Data.List using (foldr)
+open import Data.Product using (_×_; proj₁; _,_)
-open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans)
+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 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.Bundles.FiniteValueMap
+import Lattice.FiniteValueMap
-
-private module FixedHeightFiniteMap = Lattice.Bundles.FiniteValueMap.FromFiniteHeightLattice
 
 data Sign : Set where
     + : Sign
@@ -30,53 +32,133 @@ _≟ᵍ_ 0ˢ + = no (λ ())
 _≟ᵍ_ 0ˢ - = no (λ ())
 _≟ᵍ_ 0ˢ 0ˢ = yes refl
 
-module _ (prog : Program) where
+-- 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
     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.
-    open FixedHeightFiniteMap String SignLattice _≟ˢ_ finiteHeightLatticeᵍ vars-Unique ≈ᵍ-dec
+    module VariableSignsFiniteMap = Lattice.FiniteValueMap.WithKeys _≟ˢ_ isLatticeᵍ vars
+    open VariableSignsFiniteMap
         using ()
         renaming
-            ( finiteHeightLattice to finiteHeightLatticeᵛ
+            ( FiniteMap to VariableSigns
-            ; FiniteMap to VariableSigns
+            ; isLattice to isLatticeᵛ
             ; _≈_ to _≈ᵛ_
             ; _⊔_ to _⊔ᵛ_
-            ; ≈-dec to ≈ᵛ-dec
+            ; _≼_ 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]ᵛ
             )
-    open FiniteHeightLattice finiteHeightLatticeᵛ
+    open IsLattice isLatticeᵛ
         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ᵛ
+            )
 
-    ⊥ᵛ = proj₁ (proj₁ (proj₁ (FiniteHeightLattice.fixedHeight finiteHeightLatticeᵛ)))
+    ≈ᵛ-dec = ≈ᵍ-dec⇒≈ᵛ-dec ≈ᵍ-dec
+    joinSemilatticeᵛ = IsFiniteHeightLattice.joinSemilattice isFiniteHeightLatticeᵛ
+    fixedHeightᵛ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵛ
+    ⊥ᵛ = proj₁ (proj₁ (proj₁ fixedHeightᵛ))
 
     -- Finally, the map we care about is (state -> (variables -> sign)). Bring that in.
-    module StateVariablesFiniteMap = FixedHeightFiniteMap State VariableSigns _≟_ finiteHeightLatticeᵛ states-Unique ≈ᵛ-dec
+    module StateVariablesFiniteMap = Lattice.FiniteValueMap.WithKeys _≟_ isLatticeᵛ states
     open StateVariablesFiniteMap
         using (_[_]; m₁≼m₂⇒m₁[ks]≼m₂[ks])
         renaming
-            ( finiteHeightLattice to finiteHeightLatticeᵐ
+            ( FiniteMap to StateVariables
-            ; 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 FiniteHeightLattice finiteHeightLatticeᵐ
+    open Lattice.FiniteValueMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight _≟_ isLatticeᵛ states-Unique ≈ᵛ-dec _ fixedHeightᵛ
         using ()
-        renaming (_≼_ to _≼ᵐ_)
+        renaming
+            ( isFiniteHeightLattice to isFiniteHeightLatticeᵐ
+            )
+
+    ≈ᵐ-dec = ≈ᵛ-dec⇒≈ᵐ-dec ≈ᵛ-dec
+    fixedHeightᵐ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵐ
 
     -- build up the 'join' function, which follows from Exercise 4.26's
     --
@@ -103,3 +185,157 @@ module _ (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,17 +3,19 @@ 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; _≡_)
+open import Relation.Binary.PropositionalEquality using (cong; _≡_; refl)
 open import Relation.Nullary using (¬_)
 open import Function using (_∘_)
 
 open import Lattice
-open import Utils using (Unique; Unique-map; empty; push)
+open import Utils using (Unique; Unique-map; empty; push; x∈xs⇒fx∈fxs)
 
 data Expr : Set where
     _+_ : Expr → Expr → Expr
@@ -24,24 +26,116 @@ data Expr : Set where
 data Stmt : Set where
     _←_ : String → Expr → Stmt
 
-open import Lattice.MapSet String _≟ˢ_
+open import Lattice.MapSet _≟ˢ_
     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) = insertˢ s emptyˢ
+    Expr-vars (` s) = singletonˢ s
     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) = insertˢ x (Expr-vars e)
+    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')
 
     -- Creating a new number from a natural number can never create one
     -- equal to one you get from weakening the bounds on another number.
@@ -62,6 +156,10 @@ 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
@@ -71,8 +169,7 @@ record Program : Set where
 
     private
         vars-Set : StringSet
-        vars-Set = foldr (λ n → StringSet)
+        vars-Set = Stmts-vars stmts
-                         (λ {k} stmt acc → (Stmt-vars stmt) ⊔ˢ acc) emptyˢ stmts
 
     vars : List String
     vars = to-Listˢ vars-Set
@@ -83,19 +180,25 @@ 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 edged  will have to change too
+    -- Computations for incoming and outgoing edges will have to change too
     -- when we support branching etc.
 
     incoming : State → List State

Lattice/AboveBelow.agda

@@ -68,7 +68,10 @@ 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.
-module Plain where
+--
+-- 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
     _⊔_ : AboveBelow → AboveBelow → AboveBelow
     ⊥ ⊔ x = x
     ⊤ ⊔ x = ⊤
@@ -296,7 +299,7 @@ module Plain where
         ; isLattice = isLattice
         }
 
-    open IsLattice isLattice using (_≼_; _≺_)
+    open IsLattice isLattice using (_≼_; _≺_; ⊔-Monotonicˡ; ⊔-Monotonicʳ) public
 
     ⊥≺[x] : ∀ (x : A) → ⊥ ≺ [ x ]
     ⊥≺[x] x = (≈-refl , λ ())
@@ -322,36 +325,38 @@ module Plain where
 
     open Chain _≈_ ≈-equiv (IsLattice._≺_ isLattice) (IsLattice.≺-cong isLattice)
 
-    module _ (x : A) where
+    longestChain : Chain ⊥ ⊤ 2
-        longestChain : Chain ⊥ ⊤ 2
+    longestChain = step (⊥≺[x] x) ≈-refl (step ([x]≺⊤ x) ≈-⊤-⊤ (done ≈-⊤-⊤))
-        longestChain = step (⊥≺[x] x) ≈-refl (step ([x]≺⊤ x) ≈-⊤-⊤ (done ≈-⊤-⊤))
 
-        ¬-Chain-⊤ : ∀ {ab : AboveBelow} {n : ℕ} → ¬ Chain ⊤ ab (suc n)
+    ¬-Chain-⊤ : ∀ {ab : AboveBelow} {n : ℕ} → ¬ Chain ⊤ ab (suc n)
-        ¬-Chain-⊤ {x} (step (⊤⊔x≈x , ⊤̷≈x) _ _) rewrite ⊤⊔x≡⊤ x = ⊥-elim (⊤̷≈x ⊤⊔x≈x)
+    ¬-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 : ∀ {ab₁ ab₂ : AboveBelow} {n : ℕ} → Chain ab₁ ab₂ n → n ≤ 2
-        isLongest (done _) = z≤n
+    isLongest (done _) = z≤n
-        isLongest (step _ _ (done _)) = s≤s z≤n
+    isLongest (step _ _ (done _)) = s≤s z≤n
-        isLongest (step _ _ (step _ _ (done _))) = s≤s (s≤s z≤n)
+    isLongest (step _ _ (step _ _ (done _))) = s≤s (s≤s z≤n)
-        isLongest {⊤} c@(step _ _ _) = ⊥-elim (¬-Chain-⊤ c)
+    isLongest {⊤} c@(step _ _ _) = ⊥-elim (¬-Chain-⊤ c)
-        isLongest {[ x ]} (step {_} {y} [x]≺y y≈y' c@(step _ _ _))
+    isLongest {[ x ]} (step {_} {y} [x]≺y y≈y' c@(step _ _ _))
-            rewrite [x]≺y⇒y≡⊤ x y [x]≺y with ≈-⊤-⊤ ← y≈y' = ⊥-elim (¬-Chain-⊤ c)
+        rewrite [x]≺y⇒y≡⊤ x y [x]≺y with ≈-⊤-⊤ ← y≈y' = ⊥-elim (¬-Chain-⊤ c)
-        isLongest {⊥} (step {_} {⊥} (_ , ⊥̷≈⊥) _ _) = ⊥-elim (⊥̷≈⊥ ≈-⊥-⊥)
+    isLongest {⊥} (step {_} {⊥} (_ , ⊥̷≈⊥) _ _) = ⊥-elim (⊥̷≈⊥ ≈-⊥-⊥)
-        isLongest {⊥} (step {_} {⊤} _ ≈-⊤-⊤ c@(step _ _ _)) = ⊥-elim (¬-Chain-⊤ c)
+    isLongest {⊥} (step {_} {⊤} _ ≈-⊤-⊤ c@(step _ _ _)) = ⊥-elim (¬-Chain-⊤ c)
-        isLongest {⊥} (step {_} {[ x ]} _ (≈-lift _) (step [x]≺y y≈z c@(step _ _ _)))
+    isLongest {⊥} (step {_} {[ x ]} _ (≈-lift _) (step [x]≺y y≈z c@(step _ _ _)))
-            rewrite [x]≺y⇒y≡⊤ _ _ [x]≺y with ≈-⊤-⊤ ← y≈z = ⊥-elim (¬-Chain-⊤ c)
+        rewrite [x]≺y⇒y≡⊤ _ _ [x]≺y with ≈-⊤-⊤ ← y≈z = ⊥-elim (¬-Chain-⊤ c)
 
-        isFiniteHeightLattice : IsFiniteHeightLattice AboveBelow 2 _≈_ _⊔_ _⊓_
+    fixedHeight : IsLattice.FixedHeight isLattice 2
-        isFiniteHeightLattice = record
+    fixedHeight = (((⊥ , ⊤) , longestChain) , isLongest)
-            { isLattice = isLattice
-            ; fixedHeight = (((⊥ , ⊤) , longestChain) , isLongest)
-            }
 
-        finiteHeightLattice : FiniteHeightLattice AboveBelow
+    isFiniteHeightLattice : IsFiniteHeightLattice AboveBelow 2 _≈_ _⊔_ _⊓_
-        finiteHeightLattice = record
+    isFiniteHeightLattice = record
-            { height = 2
+        { isLattice = isLattice
-            ; _≈_ = _≈_
+        ; fixedHeight = fixedHeight
-            ; _⊔_ = _⊔_
+        }
-            ; _⊓_ = _⊓_
+
-            ; 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 A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A isLattice₂
+    module FM = Lattice.FiniteMap ≡-dec-A isLattice₂
     open FM.WithKeys ks public
 
     import Lattice.FiniteValueMap
-    module FVM = Lattice.FiniteValueMap A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A isLattice₂
+    module FVM = Lattice.FiniteValueMap ≡-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)
+module Lattice.FiniteMap {a b : Level} {A : Set a} {B : Set b}
-    (_≈₂_ : B → B → Set b)
+    {_≈₂_ : B → B → Set b}
-    (_⊔₂_ : B → B → B) (_⊓₂_ : B → B → 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 A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB as Map
+open import Lattice.Map ≡-dec-A lB as Map
-    using (Map; ⊔-equal-keys; ⊓-equal-keys; ∈k-dec; m₁≼m₂⇒m₁[k]≼m₂[k])
+    using (Map; ⊔-equal-keys; ⊓-equal-keys; ∈k-dec)
     renaming
         ( _≈_ to _≈ᵐ_
         ; _⊔_ to _⊔ᵐ_
@@ -30,6 +30,7 @@ open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-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_
@@ -69,9 +70,15 @@ 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
@@ -122,7 +129,7 @@ module WithKeys (ks : List A) where
         ; absorb-⊓-⊔ = λ (m₁ , _) (m₂ , _) → absorb-⊓ᵐ-⊔ᵐ m₁ m₂
         }
 
-    open IsLattice isLattice using (_≼_) public
+    open IsLattice isLattice using (_≼_; ⊔-Monotonicˡ; ⊔-Monotonicʳ) public
 
     lattice : Lattice FiniteMap
     lattice = record
@@ -132,6 +139,10 @@ 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}
@@ -171,7 +182,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)
+module Lattice.FiniteValueMap {A : Set} {B : Set}
-    (_≈₂_ : B → B → Set)
+    {_≈₂_ : B → B → Set}
-    (_⊔₂_ : B → B → B) (_⊓₂_ : B → B → B)
+    {_⊔₂_ : B → B → B} {_⊓₂_ : B → B → B}
     (≡-dec-A : Decidable (_≡_ {_} {A}))
     (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
 
@@ -29,11 +29,10 @@ 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 A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB
+open import Lattice.Map ≡-dec-A lB
     using
         ( subset-impl
         ; locate; forget
-        ; _∈_
         ; Map-functional
         ; Expr-Provenance
         ; Expr-Provenance-≡
@@ -41,7 +40,7 @@ open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB
         ; in₁; in₂; bothᵘ; single
         ; ⊔-combines
         )
-open import Lattice.FiniteMap A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB public
+open import Lattice.FiniteMap ≡-dec-A lB public
 
 module IterProdIsomorphism where
     open import Data.Unit using (⊤; tt)
@@ -103,7 +102,7 @@ module IterProdIsomorphism where
         _⊔ⁱᵖ_ {ks} = IP._⊔_ (length ks)
 
         _∈ᵐ_ : ∀ {ks : List A} → A × B → FiniteMap ks → Set
-        _∈ᵐ_ {ks} k,v fm = k,v ∈ proj₁ fm
+        _∈ᵐ_ {ks} = _∈_ ks
 
     -- The left inverse is: from (to x) = x
     from-to-inverseˡ : ∀ {ks : List A} (uks : Unique ks) →
@@ -156,7 +155,7 @@ module IterProdIsomorphism where
 
     private
         first-key-in-map : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) →
-                           Σ B (λ v → (k , v) ∈ proj₁ fm)
+                           Σ B (λ v → (k , v) ∈ᵐ 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)
+module Lattice.Map {a b : Level} {A : Set a} {B : Set b}
-    (_≈₂_ : B → B → Set b)
+    {_≈₂_ : B → B → Set b}
-    (_⊔₂_ : B → B → B) (_⊓₂_ : B → B → B)
+    {_⊔₂_ : B → B → B} {_⊓₂_ : B → B → B}
     (≡-dec-A : Decidable (_≡_ {a} {A}))
     (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
 
@@ -553,11 +553,18 @@ 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,21 +3,31 @@ 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 A ⊤ _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A ⊤-isLattice
+private module UnitMap = Lattice.Map ≡-dec-A ⊤-isLattice
-open UnitMap using (Map)
+open UnitMap
-open UnitMap using
+    using (Map; Expr; ⟦_⟧)
-    ( _⊆_; _≈_; ≈-equiv; _⊔_; _⊓_; empty
+    renaming
-    ; isUnionSemilattice; isIntersectSemilattice; isLattice; lattice
+        ( Expr-Provenance to Expr-Provenanceᵐ
-    ) public
+        )
+open UnitMap
+    using
+        ( _⊆_; _≈_; ≈-equiv; _⊔_; _⊓_; _∪_ ; _∩_ ; `_; empty; forget
+        ; isUnionSemilattice; isIntersectSemilattice; isLattice; lattice
+        ; Provenance
+        ; ⊔-preserves-∈k₁
+        ; ⊔-preserves-∈k₂
+        )
+    renaming (_∈k_ to _∈_) public
+open Provenance public
 
 MapSet : Set a
 MapSet = Map
@@ -27,3 +37,9 @@ 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

@@ -1,57 +0,0 @@
-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,6 +54,11 @@ 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)