open import Language
open import Lattice

module Analysis.Forward
    {L : Set} {h}
    {_≈ˡ_ : L → L → Set} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L}
    (isFiniteHeightLatticeˡ : IsFiniteHeightLattice L h _≈ˡ_ _⊔ˡ_ _⊓ˡ_)
    (≈ˡ-dec : IsDecidable _≈ˡ_) 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 Relation.Nullary using (¬_; Dec; yes; no)
open import Data.Unit using (⊤)
open import Function using (_∘_)

open import Utils using (Pairwise)
import Lattice.FiniteValueMap

open IsFiniteHeightLattice isFiniteHeightLatticeˡ
    using ()
    renaming
        ( isLattice to isLatticeˡ
        ; fixedHeight to fixedHeightˡ
        ; _≼_ to _≼ˡ_
        )

module WithProg (prog : Program) where
    open Program prog

    -- The variable -> abstract value (e.g. sign) map is a finite value-map
    -- with keys strings. Use a bundle to avoid explicitly specifying operators.
    module VariableValuesFiniteMap = Lattice.FiniteValueMap.WithKeys _≟ˢ_ isLatticeˡ vars
    open VariableValuesFiniteMap
        using ()
        renaming
            ( FiniteMap to VariableValues
            ; isLattice to isLatticeᵛ
            ; _≈_ 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]ᵛ
            ; ∈k-dec to ∈k-decᵛ
            ; all-equal-keys to all-equal-keysᵛ
            )
        public
    open IsLattice isLatticeᵛ
        using ()
        renaming
            ( ⊔-Monotonicˡ to ⊔ᵛ-Monotonicˡ
            ; ⊔-Monotonicʳ to ⊔ᵛ-Monotonicʳ
            ; ⊔-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ᵛ))

    -- Finally, the map we care about is (state -> (variables -> value)). Bring that in.
    module StateVariablesFiniteMap = Lattice.FiniteValueMap.WithKeys _≟_ isLatticeᵛ states
    open StateVariablesFiniteMap
        using (_[_]; m₁≼m₂⇒m₁[ks]≼m₂[ks])
        renaming
            ( 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]ᵐ
            )
        public
    open Lattice.FiniteValueMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight _≟_ isLatticeᵛ states-Unique ≈ᵛ-dec _ fixedHeightᵛ
        using ()
        renaming
            ( isFiniteHeightLattice to isFiniteHeightLatticeᵐ
            )

    ≈ᵐ-dec = ≈ᵛ-dec⇒≈ᵐ-dec ≈ᵛ-dec
    fixedHeightᵐ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵐ

    -- build up the 'join' function, which follows from Exercise 4.26's
    --
    --    L₁ → (A → L₂)
    --
    -- Construction, with L₁ = (A → L₂), and f = id

    joinForKey : State → StateVariables → VariableValues
    joinForKey k states = foldr _⊔ᵛ_ ⊥ᵛ (states [ incoming k ])

    -- The per-key join is made up of map key accesses (which are monotonic)
    -- and folds using the join operation (also monotonic)

    joinForKey-Mono : ∀ (k : State) → Monotonic _≼ᵐ_ _≼ᵛ_ (joinForKey k)
    joinForKey-Mono k {fm₁} {fm₂} fm₁≼fm₂ =
        foldr-Mono joinSemilatticeᵛ joinSemilatticeᵛ (fm₁ [ incoming k ]) (fm₂ [ incoming k ]) _⊔ᵛ_ ⊥ᵛ ⊥ᵛ
                   (m₁≼m₂⇒m₁[ks]≼m₂[ks] fm₁ fm₂ (incoming k) fm₁≼fm₂)
                   (⊔ᵛ-idemp ⊥ᵛ) ⊔ᵛ-Monotonicʳ ⊔ᵛ-Monotonicˡ

    -- The name f' comes from the formulation of Exercise 4.26.
    open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) joinForKey joinForKey-Mono states
        renaming
            ( f' to joinAll
            ; f'-Monotonic to joinAll-Mono
            )

    -- With 'join' in hand, we need to perform abstract evaluation.
    module WithEvaluator (eval : Expr → VariableValues → L)
                         (eval-Mono : ∀ (e : Expr) → Monotonic _≼ᵛ_ _≼ˡ_ (eval e)) where

        -- For a particular evaluation function, we need to perform an evaluation
        -- for an assignment, and update the corresponding key. Use Exercise 4.26's
        -- generalized update to set the single key's value.

        private module _ (k : String) (e : Expr) where
            open VariableValuesFiniteMap.GeneralizedUpdate vars isLatticeᵛ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) (λ _ → eval e) (λ _ {vs₁} {vs₂} vs₁≼vs₂ → eval-Mono e {vs₁} {vs₂} vs₁≼vs₂) (k ∷ [])
                renaming
                    ( f' to updateVariablesFromExpression
                    ; f'-Monotonic to updateVariablesFromExpression-Mono
                    )
                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.
        --
        -- This per-state function adjusts the variables in that state,
        -- also monotonically; we derive the for-each-state update from
        -- the Exercise 4.26 again.

        updateVariablesForState : State → StateVariables → VariableValues
        updateVariablesForState s sv
            with code s
        ...   | k ← e =
                let
                    (vs , s,vs∈sv) = locateᵐ {s} {sv} (states-in-Map s sv)
                in
                    updateVariablesFromExpression k e vs

        updateVariablesForState-Monoʳ : ∀ (s : State) → Monotonic _≼ᵐ_ _≼ᵛ_ (updateVariablesForState s)
        updateVariablesForState-Monoʳ s {sv₁} {sv₂} sv₁≼sv₂
            with code s
        ...   | k ← e =
                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 {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
                )

        -- Finally, the whole analysis consists of getting the 'join'
        -- of all incoming states, then applying the per-state evaluation
        -- function. This is just a composition, and is trivially monotonic.

        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₂)

        -- 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)
            public