open import Language hiding (_[_])
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.Empty using (⊥-elim)
open import Data.String using (String)
open import Data.Product using (_,_)
open import Data.List using (_∷_; []; foldr; foldl)
open import Data.List.Relation.Unary.Any as Any using ()
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym; subst)
open import Relation.Nullary using (yes; no)
open import Function using (_∘_; flip)

open IsFiniteHeightLattice isFiniteHeightLatticeˡ
    using () renaming (isLattice to isLatticeˡ)

module WithProg (prog : Program) where
    open import Analysis.Forward.Lattices isFiniteHeightLatticeˡ ≈ˡ-dec prog
    open import Analysis.Forward.Evaluation isFiniteHeightLatticeˡ ≈ˡ-dec prog
    open Program prog

    private module WithStmtEvaluator {{evaluator : StmtEvaluator}} where
        open StmtEvaluator evaluator

        updateVariablesForState : State → StateVariables → VariableValues
        updateVariablesForState s sv =
            foldl (flip (eval s)) (variablesAt s sv) (code s)

        updateVariablesForState-Monoʳ : ∀ (s : State) → Monotonic _≼ᵐ_ _≼ᵛ_ (updateVariablesForState s)
        updateVariablesForState-Monoʳ s {sv₁} {sv₂} sv₁≼sv₂ =
            let
                bss = code s
                (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
                foldl-Mono' (IsLattice.joinSemilattice isLatticeᵛ) bss
                            (flip (eval s)) (eval-Monoʳ s)
                            vs₁≼vs₂

        open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) updateVariablesForState updateVariablesForState-Monoʳ states
            using ()
            renaming
                ( f' to updateAll
                ; f'-Monotonic to updateAll-Mono
                ; f'-k∈ks-≡ to updateAll-k∈ks-≡
                )
            public

        -- 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; aᶠ≈faᶠ to result≈analyze-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 WithValidInterpretation {{latticeInterpretationˡ : LatticeInterpretation isLatticeˡ}}
                                       {{validEvaluator : ValidStmtEvaluator evaluator latticeInterpretationˡ}} where
            open ValidStmtEvaluator validEvaluator

            eval-fold-valid : ∀ {s bss vs ρ₁ ρ₂} → ρ₁ , bss ⇒ᵇˢ ρ₂ → ⟦ vs ⟧ᵛ ρ₁ → ⟦ foldl (flip (eval s)) vs bss ⟧ᵛ ρ₂
            eval-fold-valid {_} [] ⟦vs⟧ρ = ⟦vs⟧ρ
            eval-fold-valid {s} {bs ∷ bss'} {vs} {ρ₁} {ρ₂} (ρ₁,bs⇒ρ ∷ ρ,bss'⇒ρ₂) ⟦vs⟧ρ₁ =
                eval-fold-valid
                    {bss = bss'} {eval s bs vs} ρ,bss'⇒ρ₂
                    (valid ρ₁,bs⇒ρ ⟦vs⟧ρ₁)

            updateVariablesForState-matches : ∀ {s sv ρ₁ ρ₂} → ρ₁ , (code s) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s sv ⟧ᵛ ρ₁ → ⟦ updateVariablesForState s sv ⟧ᵛ ρ₂
            updateVariablesForState-matches = eval-fold-valid

            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⟧ρ₁

            stepTrace : ∀ {s₁ ρ₁ ρ₂} → ⟦ joinForKey s₁ result ⟧ᵛ ρ₁ → ρ₁ , (code s₁) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s₁ result ⟧ᵛ ρ₂
            stepTrace {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ ρ₁,bss⇒ρ₂ =
                    let
                        -- I'd use rewrite, but Agda gets a memory overflow (?!).
                        ⟦joinAll-result⟧ρ₁ =
                            subst (λ vs → ⟦ vs ⟧ᵛ ρ₁)
                                  (sym (variablesAt-joinAll s₁ result))
                                  ⟦joinForKey-s₁⟧ρ₁
                        ⟦analyze-result⟧ρ₂ =
                            updateAll-matches {sv = joinAll result}
                                              ρ₁,bss⇒ρ₂ ⟦joinAll-result⟧ρ₁
                        analyze-result≈result =
                            ≈ᵐ-sym {result} {updateAll (joinAll result)}
                                   result≈analyze-result
                        analyze-s₁≈s₁ =
                            variablesAt-≈ s₁ (updateAll (joinAll result))
                                             result (analyze-result≈result)
                    in
                        ⟦⟧ᵛ-respects-≈ᵛ {variablesAt s₁ (updateAll (joinAll result))} {variablesAt s₁ result} (analyze-s₁≈s₁) ρ₂ ⟦analyze-result⟧ρ₂

            walkTrace : ∀ {s₁ s₂ ρ₁ ρ₂} → ⟦ joinForKey s₁ result ⟧ᵛ ρ₁ → Trace {graph} s₁ s₂ ρ₁ ρ₂ → ⟦ variablesAt s₂ result ⟧ᵛ ρ₂
            walkTrace {s₁} {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ (Trace-single ρ₁,bss⇒ρ₂) =
                stepTrace {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ ρ₁,bss⇒ρ₂
            walkTrace {s₁} {s₂} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ (Trace-edge {ρ₂ = ρ} {idx₂ = s} ρ₁,bss⇒ρ s₁→s₂ tr) =
                let
                    ⟦result-s₁⟧ρ =
                        stepTrace {s₁} {ρ₁} {ρ} ⟦joinForKey-s₁⟧ρ₁ ρ₁,bss⇒ρ
                    s₁∈incomingStates =
                        []-∈ result (edge⇒incoming s₁→s₂)
                                    (variablesAt-∈ s₁ result)
                    ⟦joinForKey-s⟧ρ =
                        ⟦⟧ᵛ-foldr ⟦result-s₁⟧ρ s₁∈incomingStates
                in
                    walkTrace ⟦joinForKey-s⟧ρ tr

            joinForKey-initialState-⊥ᵛ : joinForKey initialState result ≡ ⊥ᵛ
            joinForKey-initialState-⊥ᵛ = cong (λ ins → foldr _⊔ᵛ_ ⊥ᵛ (result [ ins ])) initialState-pred-∅

            ⟦joinAll-initialState⟧ᵛ∅ : ⟦ joinForKey initialState result ⟧ᵛ []
            ⟦joinAll-initialState⟧ᵛ∅ = subst (λ vs → ⟦ vs ⟧ᵛ []) (sym joinForKey-initialState-⊥ᵛ) ⟦⊥ᵛ⟧ᵛ∅

            analyze-correct : ∀ {ρ : Env} → [] , rootStmt ⇒ˢ ρ → ⟦ variablesAt finalState result ⟧ᵛ ρ
            analyze-correct {ρ} ∅,s⇒ρ = walkTrace {initialState} {finalState} {[]} {ρ} ⟦joinAll-initialState⟧ᵛ∅ (trace ∅,s⇒ρ)

    open WithStmtEvaluator using (result; analyze; result≈analyze-result) public
    open WithStmtEvaluator.WithValidInterpretation using (analyze-correct) public