open import Language hiding (_[_])
open import Lattice

module Analysis.Forward.Adapters
    (L : Set) {h}
    {_≈ˡ_ : L → L → Set} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L}
    {{isFiniteHeightLatticeˡ : IsFiniteHeightLattice L h _≈ˡ_ _⊔ˡ_ _⊓ˡ_}}
    {{≈ˡ-dec : IsDecidable _≈ˡ_}}
    (prog : Program) where

open import Analysis.Forward.Lattices L prog
open import Analysis.Forward.Evaluation L prog

open import Data.Empty using (⊥-elim)
open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
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ˡ
        ; _≼_ to _≼ˡ_
        )
open Program prog

-- Now, allow StmtEvaluators to be auto-constructed from ExprEvaluators.
module ExprToStmtAdapter {{ exprEvaluator : ExprEvaluator }} where
    open ExprEvaluator exprEvaluator
        using ()
        renaming
            ( eval to evalᵉ
            ; eval-Monoʳ to evalᵉ-Monoʳ
            )

    -- 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 {{isLatticeᵛ}} (λ x → x) (λ a₁≼a₂ → a₁≼a₂) (λ _ → evalᵉ e) (λ _ {vs₁} {vs₂} vs₁≼vs₂ → evalᵉ-Monoʳ e {vs₁} {vs₂} vs₁≼vs₂) (k ∷ [])
            using ()
            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

    -- 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.

    evalᵇ : State → BasicStmt → VariableValues → VariableValues
    evalᵇ _ (k ← e) vs = updateVariablesFromExpression k e vs
    evalᵇ _ noop vs = vs

    evalᵇ-Monoʳ : ∀ (s : State) (bs : BasicStmt) → Monotonic _≼ᵛ_ _≼ᵛ_ (evalᵇ s bs)
    evalᵇ-Monoʳ _ (k ← e) {vs₁} {vs₂} vs₁≼vs₂ = updateVariablesFromExpression-Mono k e {vs₁} {vs₂} vs₁≼vs₂
    evalᵇ-Monoʳ _ noop vs₁≼vs₂ = vs₁≼vs₂

    instance
        stmtEvaluator : StmtEvaluator
        stmtEvaluator = record { eval = evalᵇ ; eval-Monoʳ = evalᵇ-Monoʳ }

    -- Moreover, correct StmtEvaluators can be constructed from correct
    -- ExprEvaluators.
    module _ {{latticeInterpretationˡ : LatticeInterpretation isLatticeˡ}}
             {{isValid : ValidExprEvaluator exprEvaluator latticeInterpretationˡ}} where
        open ValidExprEvaluator isValid using () renaming (valid to validᵉ)

        evalᵇ-valid : ∀ {s vs ρ₁ ρ₂ bs} → ρ₁ , bs ⇒ᵇ ρ₂ → ⟦ vs ⟧ᵛ ρ₁ → ⟦ evalᵇ s bs vs ⟧ᵛ ρ₂
        evalᵇ-valid {_} {vs} {ρ₁} {ρ₁} {_} (⇒ᵇ-noop ρ₁) ⟦vs⟧ρ₁ = ⟦vs⟧ρ₁
        evalᵇ-valid {_} {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' =
                validᵉ ρ,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'∈ρ₁

        instance
            validStmtEvaluator : ValidStmtEvaluator stmtEvaluator latticeInterpretationˡ
            validStmtEvaluator = record
                { valid = λ {a} {b} {c} {d} →  evalᵇ-valid {a} {b} {c} {d}
                }