Analysis/Forward.agda

@@ -7,19 +7,17 @@ module Analysis.Forward
     (isFiniteHeightLatticeˡ : IsFiniteHeightLattice L h _≈ˡ_ _⊔ˡ_ _⊓ˡ_)
     (≈ˡ-dec : IsDecidable _≈ˡ_) where
 
-open import Data.Empty using (⊥-elim)
 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; foldl; cartesianProduct; cartesianProductWith)
+open import Data.List using (List; _∷_; []; foldr; cartesianProduct; cartesianProductWith)
 open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_)
-open import Data.List.Relation.Unary.Any as Any using ()
 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 (_∘_; flip)
+open import Function using (_∘_)
 
-open import Utils using (Pairwise; _⇒_)
+open import Utils using (Pairwise)
 import Lattice.FiniteValueMap
 
 open IsFiniteHeightLattice isFiniteHeightLatticeˡ
@@ -28,7 +26,6 @@ open IsFiniteHeightLattice isFiniteHeightLatticeˡ
         ( isLattice to isLatticeˡ
         ; fixedHeight to fixedHeightˡ
         ; _≼_ to _≼ˡ_
-        ; ≈-sym to ≈ˡ-sym
         )
 
 module WithProg (prog : Program) where
@@ -96,17 +93,6 @@ module WithProg (prog : Program) where
     ≈ᵐ-dec = ≈ᵛ-dec⇒≈ᵐ-dec ≈ᵛ-dec
     fixedHeightᵐ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵐ
 
-    -- We now have our (state -> (variables -> value)) map.
-    -- Define a couple of helpers to retrieve values from it. Specifically,
-    -- since the State type is as specific as possible, it's always possible to
-    -- retrieve the variable values at each state.
-
-    states-in-Map : ∀ (s : State) (sv : StateVariables) → s ∈kᵐ sv
-    states-in-Map s sv@(m , ksv≡states) rewrite ksv≡states = states-complete s
-
-    variablesAt : State → StateVariables → VariableValues
-    variablesAt s sv = proj₁ (locateᵐ {s} {sv} (states-in-Map s sv))
-
     -- build up the 'join' function, which follows from Exercise 4.26's
     --
     --    L₁ → (A → L₂)
@@ -130,15 +116,8 @@ module WithProg (prog : Program) where
         renaming
             ( f' to joinAll
             ; f'-Monotonic to joinAll-Mono
-            ; f'-k∈ks-≡ to joinAll-k∈ks-≡
             )
 
-    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
-
     -- With 'join' in hand, we need to perform abstract evaluation.
     module WithEvaluator (eval : Expr → VariableValues → L)
                          (eval-Mono : ∀ (e : Expr) → Monotonic _≼ᵛ_ _≼ˡ_ (eval e)) where
@@ -152,11 +131,12 @@ module WithProg (prog : Program) where
                 renaming
                     ( f' to updateVariablesFromExpression
                     ; f'-Monotonic to updateVariablesFromExpression-Mono
-                    ; f'-k∈ks-≡ to updateVariablesFromExpression-k∈ks-≡
-                    ; f'-k∉ks-backward to updateVariablesFromExpression-k∉ks-backward
                     )
                 public
 
+        states-in-Map : ∀ (s : State) (sv : StateVariables) → s ∈kᵐ sv
+        states-in-Map s sv@(m , ksv≡states) rewrite ksv≡states = states-complete s
+
         -- The per-state update function makes use of the single-key setter,
         -- updateVariablesFromExpression, for the case where the statement
         -- is an assignment.
@@ -175,7 +155,11 @@ module WithProg (prog : Program) where
 
         updateVariablesForState : State → StateVariables → VariableValues
         updateVariablesForState s sv =
-            foldl (flip updateVariablesFromStmt) (variablesAt s sv) (code s)
+            let
+                bss = code s
+                (vs , s,vs∈sv) = locateᵐ {s} {sv} (states-in-Map s sv)
+            in
+                foldr updateVariablesFromStmt vs bss
 
         updateVariablesForState-Monoʳ : ∀ (s : State) → Monotonic _≼ᵐ_ _≼ᵛ_ (updateVariablesForState s)
         updateVariablesForState-Monoʳ s {sv₁} {sv₂} sv₁≼sv₂ =
@@ -185,15 +169,14 @@ module WithProg (prog : Program) where
                 (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
-                foldl-Mono' (IsLattice.joinSemilattice isLatticeᵛ) bss
+                foldr-Mono' (IsLattice.joinSemilattice isLatticeᵛ) bss
-                            (flip updateVariablesFromStmt) updateVariablesFromStmt-Monoʳ
+                            updateVariablesFromStmt updateVariablesFromStmt-Monoʳ
                             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
-                ; f'-k∈ks-≡ to updateAll-k∈ks-≡
                 )
 
         -- Finally, the whole analysis consists of getting the 'join'
@@ -211,62 +194,5 @@ module WithProg (prog : Program) where
         -- The fixed point of the 'analyze' function is our final goal.
         open import Fixedpoint ≈ᵐ-dec isFiniteHeightLatticeᵐ analyze (λ {m₁} {m₂} m₁≼m₂ → analyze-Mono {m₁} {m₂} m₁≼m₂)
             using ()
-            renaming (aᶠ to result; aᶠ≈faᶠ to result≈analyze-result)
+            renaming (aᶠ to result)
             public
-
-        variablesAt-updateAll : ∀ (s : State) (sv : StateVariables) →
-                                variablesAt s (updateAll sv) ≡ updateVariablesForState s sv
-        variablesAt-updateAll s sv
-            with (vs , s,vs∈usv) ← locateᵐ {s} {updateAll sv} (states-in-Map s (updateAll sv)) =
-            updateAll-k∈ks-≡ {l = sv} (states-complete s) s,vs∈usv
-
-        module WithInterpretation (latticeInterpretationˡ : LatticeInterpretation isLatticeˡ) where
-            open LatticeInterpretation latticeInterpretationˡ
-                using ()
-                renaming (⟦_⟧ to ⟦_⟧ˡ; ⟦⟧-respects-≈ to ⟦⟧ˡ-respects-≈ˡ)
-
-            ⟦_⟧ᵛ : VariableValues → Env → Set
-            ⟦_⟧ᵛ vs ρ = ∀ {k l} → (k , l) ∈ᵛ vs → ∀ {v} → (k , v) Language.∈ ρ → ⟦ l ⟧ˡ v
-
-
-            ⟦⟧ᵛ-respects-≈ᵛ : ∀ {vs₁ vs₂ : VariableValues} → vs₁ ≈ᵛ vs₂ → ⟦ vs₁ ⟧ᵛ ⇒ ⟦ vs₂ ⟧ᵛ
-            ⟦⟧ᵛ-respects-≈ᵛ {m₁ , _} {m₂ , _}
-                            (m₁⊆m₂ , m₂⊆m₁) ρ ⟦vs₁⟧ρ {k} {l} k,l∈m₂ {v} k,v∈ρ =
-                let
-                    (l' , (l≈l' , k,l'∈m₁)) = m₂⊆m₁ _ _ k,l∈m₂
-                    ⟦l'⟧v = ⟦vs₁⟧ρ k,l'∈m₁ k,v∈ρ
-                in
-                    ⟦⟧ˡ-respects-≈ˡ (≈ˡ-sym l≈l') v ⟦l'⟧v
-
-            InterpretationValid : Set
-            InterpretationValid = ∀ {vs ρ e v} → ρ , e ⇒ᵉ v → ⟦ vs ⟧ᵛ ρ → ⟦ eval e vs ⟧ˡ v
-
-            module WithValidity (interpretationValidˡ : InterpretationValid) where
-
-                updateVariablesFromStmt-matches : ∀ {bs vs ρ₁ ρ₂} → ρ₁ , bs ⇒ᵇ ρ₂ → ⟦ vs ⟧ᵛ ρ₁ → ⟦ updateVariablesFromStmt bs vs ⟧ᵛ ρ₂
-                updateVariablesFromStmt-matches {_} {vs} {ρ₁} {ρ₁} (⇒ᵇ-noop ρ₁) ⟦vs⟧ρ₁ = ⟦vs⟧ρ₁
-                updateVariablesFromStmt-matches {_} {vs} {ρ₁} {_} (⇒ᵇ-← ρ₁ k e v ρ,e⇒v) ⟦vs⟧ρ₁ {k'} {l} k',l∈vs' {v'} k',v'∈ρ₂
-                    with k ≟ˢ k' | k',v'∈ρ₂
-                ...   | yes refl | here _ v _
-                        rewrite updateVariablesFromExpression-k∈ks-≡ k e {l = vs} (Any.here refl) k',l∈vs' =
-                        interpretationValidˡ ρ,e⇒v ⟦vs⟧ρ₁
-                ...   | 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'∈ρ₁ =
-                        let
-                            k'∉[k] = (λ { (Any.here refl) → k≢k' refl })
-                            k',l∈vs = updateVariablesFromExpression-k∉ks-backward k e {l = vs} k'∉[k] k',l∈vs'
-                        in
-                            ⟦vs⟧ρ₁ k',l∈vs k',v'∈ρ₁
-
-                updateVariablesFromStmt-fold-matches : ∀ {bss vs ρ₁ ρ₂} → ρ₁ , bss ⇒ᵇˢ ρ₂ → ⟦ vs ⟧ᵛ ρ₁ → ⟦ foldl (flip updateVariablesFromStmt) vs bss ⟧ᵛ ρ₂
-                updateVariablesFromStmt-fold-matches [] ⟦vs⟧ρ = ⟦vs⟧ρ
-                updateVariablesFromStmt-fold-matches {bs ∷ bss'} {vs} {ρ₁} {ρ₂} (ρ₁,bs⇒ρ ∷ ρ,bss'⇒ρ₂) ⟦vs⟧ρ₁ =
-                    updateVariablesFromStmt-fold-matches {bss'} {updateVariablesFromStmt bs vs} ρ,bss'⇒ρ₂ (updateVariablesFromStmt-matches ρ₁,bs⇒ρ ⟦vs⟧ρ₁)
-
-                updateVariablesForState-matches : ∀ {s sv ρ₁ ρ₂} → ρ₁ , (code s) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s sv ⟧ᵛ ρ₁ → ⟦ updateVariablesForState s sv ⟧ᵛ ρ₂
-                updateVariablesForState-matches = updateVariablesFromStmt-fold-matches
-
-                updateAll-matches : ∀ {s sv ρ₁ ρ₂} → ρ₁ , (code s) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s sv ⟧ᵛ ρ₁ → ⟦ variablesAt s (updateAll sv) ⟧ᵛ ρ₂
-                updateAll-matches {s} {sv} ρ₁,bss⇒ρ₂ ⟦vs⟧ρ₁ rewrite variablesAt-updateAll s sv =
-                    updateVariablesForState-matches {s} {sv} ρ₁,bss⇒ρ₂ ⟦vs⟧ρ₁

Lattice.agda

@@ -137,7 +137,7 @@ module _ {a b} {A : Set a} {B : Set b}
     const-Mono : ∀ (x : B) → Monotonic _≼₁_ _≼₂_ (λ _ → x)
     const-Mono x _ = ⊔₂-idemp x
 
-    open import Data.List as List using (List; foldr; foldl; _∷_)
+    open import Data.List as List using (List; foldr; _∷_)
     open import Utils using (Pairwise; _∷_)
 
     foldr-Mono : ∀ (l₁ l₂ : List A) (f : A → B → B) (b₁ b₂ : B) →
@@ -150,22 +150,13 @@ module _ {a b} {A : Set a} {B : Set b}
         ≼₂-trans (f-Mono₁ (foldr f b₁ xs) x≼y)
                  (f-Mono₂ y (foldr-Mono xs ys f b₁ b₂ xs≼ys b₁≼b₂ f-Mono₁ f-Mono₂))
 
-    foldl-Mono : ∀ (l₁ l₂ : List A) (f : B → A → B) (b₁ b₂ : B) →
-                 Pairwise _≼₁_ l₁ l₂ → b₁ ≼₂ b₂ →
-                 (∀ a → Monotonic _≼₂_ _≼₂_ (λ b → f b a)) →
-                 (∀ b → Monotonic _≼₁_ _≼₂_ (f b)) →
-                 foldl f b₁ l₁ ≼₂ foldl f b₂ l₂
-    foldl-Mono List.[] List.[] f b₁ b₂ _ b₁≼b₂ _ _ = b₁≼b₂
-    foldl-Mono (x ∷ xs) (y ∷ ys) f b₁ b₂ (x≼y ∷ xs≼ys) b₁≼b₂ f-Mono₁ f-Mono₂ =
-        foldl-Mono xs ys f (f b₁ x) (f b₂ y) xs≼ys (≼₂-trans (f-Mono₁ x b₁≼b₂) (f-Mono₂ b₂ x≼y)) f-Mono₁ f-Mono₂
-
 module _ {a b} {A : Set a} {B : Set b}
          {_≈₂_ : B → B → Set b} {_⊔₂_ : B → B → B}
          (lB : IsSemilattice B _≈₂_ _⊔₂_) where
 
     open IsSemilattice lB using () renaming (_≼_ to _≼₂_; ⊔-idemp to ⊔₂-idemp; ≼-trans to ≼₂-trans)
 
-    open import Data.List as List using (List; foldr; foldl; _∷_)
+    open import Data.List as List using (List; foldr; _∷_)
     open import Utils using (Pairwise; _∷_)
 
     foldr-Mono' : ∀ (l : List A) (f : A → B → B) →
@@ -174,12 +165,6 @@ module _ {a b} {A : Set a} {B : Set b}
     foldr-Mono' List.[] f _ b₁≼b₂ = b₁≼b₂
     foldr-Mono' (x ∷ xs) f f-Mono₂ b₁≼b₂ = f-Mono₂ x (foldr-Mono' xs f f-Mono₂ b₁≼b₂)
 
-    foldl-Mono' : ∀ (l : List A) (f : B → A → B) →
-                  (∀ b → Monotonic _≼₂_ _≼₂_ (λ a → f a b)) →
-                  Monotonic _≼₂_ _≼₂_ (λ b → foldl f b l)
-    foldl-Mono' List.[] f _ b₁≼b₂ = b₁≼b₂
-    foldl-Mono' (x ∷ xs) f f-Mono₁ b₁≼b₂ = foldl-Mono' xs f f-Mono₁ (f-Mono₁ x b₁≼b₂)
-
 record IsLattice {a} (A : Set a)
     (_≈_ : A → A → Set a)
     (_⊔_ : A → A → A)

Lattice/FiniteMap.agda

@@ -35,11 +35,6 @@ open import Lattice.Map ≡-dec-A lB as Map
         ; keys to keysᵐ
         ; _updating_via_ to _updatingᵐ_via_
         ; updating-via-keys-≡ to updatingᵐ-via-keys-≡
-        ; updating-via-k∈ks to updatingᵐ-via-k∈ks
-        ; updating-via-k∈ks-≡ to updatingᵐ-via-k∈ks-≡
-        ; updating-via-∈k-forward to updatingᵐ-via-∈k-forward
-        ; updating-via-k∉ks-forward to updatingᵐ-via-k∉ks-forward
-        ; updating-via-k∉ks-backward to updatingᵐ-via-k∉ks-backward
         ; f'-Monotonic to f'-Monotonicᵐ
         ; _≼_ to _≼ᵐ_
         ; ∈k-dec to ∈k-decᵐ
@@ -88,8 +83,6 @@ module WithKeys (ks : List A) where
     _∈k_ : A → FiniteMap → Set a
     _∈k_ k (m₁ , _) = k ∈ˡ (keysᵐ m₁)
 
-    open Map using (forget) public
-
     ∈k-dec = ∈k-decᵐ
 
     locate : ∀ {k : A} {fm : FiniteMap} → k ∈k fm → Σ B (λ v → (k , v) ∈ fm)
@@ -178,21 +171,6 @@ module WithKeys (ks : List A) where
         f'-Monotonic : Monotonic _≼ˡ_ _≼_ f'
         f'-Monotonic {l₁} {l₂} l₁≼l₂ = f'-Monotonicᵐ lL (proj₁ ∘ f) f-Monotonic g g-Monotonicʳ ks l₁≼l₂
 
-        f'-∈k-forward : ∀ {k l} → k ∈k (f l) → k ∈k (f' l)
-        f'-∈k-forward {k} {l} = updatingᵐ-via-∈k-forward (proj₁ (f l)) ks (updater l)
-
-        f'-k∈ks : ∀ {k l} → k ∈ˡ ks → k ∈k (f' l) → (k , updater l k) ∈ (f' l)
-        f'-k∈ks {k} {l} = updatingᵐ-via-k∈ks (proj₁ (f l)) (updater l)
-
-        f'-k∈ks-≡ : ∀ {k v l} → k ∈ˡ ks → (k , v) ∈ (f' l) → v ≡ updater l k
-        f'-k∈ks-≡ {k} {v} {l} = updatingᵐ-via-k∈ks-≡ (proj₁ (f l)) (updater l)
-
-        f'-k∉ks-forward : ∀ {k v l} → ¬ k ∈ˡ ks → (k , v) ∈ (f l) → (k , v) ∈ (f' l)
-        f'-k∉ks-forward {k} {v} {l} = updatingᵐ-via-k∉ks-forward (proj₁ (f l)) (updater l)
-
-        f'-k∉ks-backward : ∀ {k v l} → ¬ k ∈ˡ ks → (k , v) ∈ (f' l) → (k , v) ∈ (f l)
-        f'-k∉ks-backward {k} {v} {l} = updatingᵐ-via-k∉ks-backward (proj₁ (f l)) (updater 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)
 

Lattice/FiniteValueMap.agda

@@ -32,7 +32,7 @@ open import Isomorphism using (IsInverseˡ; IsInverseʳ)
 open import Lattice.Map ≡-dec-A lB
     using
         ( subset-impl
-        ; locate
+        ; locate; forget
         ; Map-functional
         ; Expr-Provenance
         ; Expr-Provenance-≡