4 changed files with 17 additions and 128 deletions
--- a/Analysis/Forward.agda
+++ b/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
-                            (flip updateVariablesFromStmt) updateVariablesFromStmt-Monoʳ
+                foldr-Mono' (IsLattice.joinSemilattice isLatticeᵛ) bss
+                            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⟧ρ₁
--- a/Lattice.agda
+++ b/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)
--- a/Lattice/FiniteMap.agda
+++ b/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)

--- a/Lattice/FiniteValueMap.agda
+++ b/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-≡