module Analysis.Constant where

open import Data.Integer as Int using (ℤ; +_; -[1+_]; _≟_)
open import Data.Integer.Show as IntShow using ()
open import Data.Nat as Nat using (ℕ; suc; zero)
open import Data.Product using (Σ; proj₁; proj₂; _,_)
open import Data.Sum using (inj₁; inj₂)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Unit using (⊤; tt)
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 (¬_; yes; no)

open import Equivalence
open import Language
open import Lattice
open import Showable using (Showable; show)
open import Utils using (_⇒_; _∧_; _∨_)
open import Analysis.Utils using (eval-combine₂)
import Analysis.Forward

instance
    showable : Showable ℤ
    showable = record
        { show = IntShow.show
        }

instance
    ≡-equiv : IsEquivalence ℤ _≡_
    ≡-equiv = record
        { ≈-refl = refl
        ; ≈-sym = sym
        ; ≈-trans = trans
        }

    ≡-Decidable-ℤ : IsDecidable {_} {ℤ} _≡_
    ≡-Decidable-ℤ = record { R-dec = _≟_ }

-- embelish 'ℕ' with a top and bottom element.
open import Lattice.AboveBelow ℤ _ as AB
    using ()
    renaming
        ( AboveBelow to ConstLattice
        ; ≈-dec to ≈ᶜ-dec
        ; ⊥ to ⊥ᶜ
        ; ⊤ to ⊤ᶜ
        ; [_] to [_]ᶜ
        ; _≈_ to _≈ᶜ_
        ; ≈-⊥-⊥ to ≈ᶜ-⊥ᶜ-⊥ᶜ
        ; ≈-⊤-⊤ to ≈ᶜ-⊤ᶜ-⊤ᶜ
        ; ≈-lift to ≈ᶜ-lift
        ; ≈-refl to ≈ᶜ-refl
        )
-- 'ℕ''s structure is not finite, so just use a 'plain' above-below Lattice.
open AB.Plain (+ 0) using ()
    renaming
        ( isLattice to isLatticeᶜ
        ; isFiniteHeightLattice to isFiniteHeightLatticeᵍ
        ; _≼_ to _≼ᶜ_
        ; _⊔_ to _⊔ᶜ_
        ; _⊓_ to _⊓ᶜ_
        ; ≼-trans to ≼ᶜ-trans
        ; ≼-refl to ≼ᶜ-refl
        )

plus : ConstLattice → ConstLattice → ConstLattice
plus ⊥ᶜ _ = ⊥ᶜ
plus _ ⊥ᶜ = ⊥ᶜ
plus ⊤ᶜ _ = ⊤ᶜ
plus _ ⊤ᶜ = ⊤ᶜ
plus [ z₁ ]ᶜ [ z₂ ]ᶜ = [ z₁ Int.+ z₂ ]ᶜ

-- this is incredibly tedious: 125 cases per monotonicity proof, and tactics
-- are hard. postulate for now.
postulate plus-Monoˡ : ∀ (s₂ : ConstLattice) → Monotonic _≼ᶜ_ _≼ᶜ_ (λ s₁ → plus s₁ s₂)
postulate plus-Monoʳ : ∀ (s₁ : ConstLattice) → Monotonic _≼ᶜ_ _≼ᶜ_ (plus s₁)

plus-Mono₂ : Monotonic₂ _≼ᶜ_ _≼ᶜ_ _≼ᶜ_ plus
plus-Mono₂ = (plus-Monoˡ , plus-Monoʳ)

minus : ConstLattice → ConstLattice → ConstLattice
minus ⊥ᶜ _ = ⊥ᶜ
minus _ ⊥ᶜ = ⊥ᶜ
minus ⊤ᶜ _ = ⊤ᶜ
minus _ ⊤ᶜ = ⊤ᶜ
minus [ z₁ ]ᶜ [ z₂ ]ᶜ = [ z₁ Int.- z₂ ]ᶜ

postulate minus-Monoˡ : ∀ (s₂ : ConstLattice) → Monotonic _≼ᶜ_ _≼ᶜ_ (λ s₁ → minus s₁ s₂)
postulate minus-Monoʳ : ∀ (s₁ : ConstLattice) → Monotonic _≼ᶜ_ _≼ᶜ_ (minus s₁)

minus-Mono₂ : Monotonic₂ _≼ᶜ_ _≼ᶜ_ _≼ᶜ_ minus
minus-Mono₂ = (minus-Monoˡ , minus-Monoʳ)

⟦_⟧ᶜ : ConstLattice → Value → Set
⟦_⟧ᶜ ⊥ᶜ _ = ⊥
⟦_⟧ᶜ ⊤ᶜ _ = ⊤
⟦_⟧ᶜ [ z ]ᶜ v = v ≡ ↑ᶻ z

⟦⟧ᶜ-respects-≈ᶜ : ∀ {s₁ s₂ : ConstLattice} → s₁ ≈ᶜ s₂ → ⟦ s₁ ⟧ᶜ ⇒ ⟦ s₂ ⟧ᶜ
⟦⟧ᶜ-respects-≈ᶜ ≈ᶜ-⊥ᶜ-⊥ᶜ v bot = bot
⟦⟧ᶜ-respects-≈ᶜ ≈ᶜ-⊤ᶜ-⊤ᶜ v top = top
⟦⟧ᶜ-respects-≈ᶜ (≈ᶜ-lift { z } { z } refl) v proof = proof

⟦⟧ᶜ-⊔ᶜ-∨ : ∀ {s₁ s₂ : ConstLattice} → (⟦ s₁ ⟧ᶜ ∨ ⟦ s₂ ⟧ᶜ) ⇒ ⟦ s₁ ⊔ᶜ s₂ ⟧ᶜ
⟦⟧ᶜ-⊔ᶜ-∨ {⊥ᶜ} x (inj₂ px₂) = px₂
⟦⟧ᶜ-⊔ᶜ-∨ {⊤ᶜ} x _ = tt
⟦⟧ᶜ-⊔ᶜ-∨ {[ s₁ ]ᶜ} {[ s₂ ]ᶜ} x px
    with s₁ ≟ s₂
...   | no _ = tt
...   | yes refl
        with px
...       | inj₁ px₁ = px₁
...       | inj₂ px₂ = px₂
⟦⟧ᶜ-⊔ᶜ-∨ {[ s₁ ]ᶜ} {⊥ᶜ} x (inj₁ px₁) = px₁
⟦⟧ᶜ-⊔ᶜ-∨ {[ s₁ ]ᶜ} {⊤ᶜ} x _ = tt

s₁≢s₂⇒¬s₁∧s₂ : ∀ {z₁ z₂ : ℤ} → ¬ z₁ ≡ z₂ → ∀ {v} → ¬ ((⟦ [ z₁ ]ᶜ ⟧ᶜ ∧ ⟦ [ z₂ ]ᶜ ⟧ᶜ) v)
s₁≢s₂⇒¬s₁∧s₂ { z₁ } { z₂ } z₁≢z₂ {v} (v≡z₁ , v≡z₂)
    with refl ← trans (sym v≡z₁) v≡z₂ = z₁≢z₂ refl

⟦⟧ᶜ-⊓ᶜ-∧ : ∀ {s₁ s₂ : ConstLattice} → (⟦ s₁ ⟧ᶜ ∧ ⟦ s₂ ⟧ᶜ) ⇒ ⟦ s₁ ⊓ᶜ s₂ ⟧ᶜ
⟦⟧ᶜ-⊓ᶜ-∧ {⊥ᶜ} x (bot , _) = bot
⟦⟧ᶜ-⊓ᶜ-∧ {⊤ᶜ} x (_ , px₂) = px₂
⟦⟧ᶜ-⊓ᶜ-∧ {[ s₁ ]ᶜ} {[ s₂ ]ᶜ} x (px₁ , px₂)
    with s₁ ≟ s₂
...   | no s₁≢s₂ = s₁≢s₂⇒¬s₁∧s₂ s₁≢s₂ (px₁ , px₂)
...   | yes refl = px₁
⟦⟧ᶜ-⊓ᶜ-∧ {[ g₁ ]ᶜ} {⊥ᶜ} x (_ , bot) = bot
⟦⟧ᶜ-⊓ᶜ-∧ {[ g₁ ]ᶜ} {⊤ᶜ} x (px₁ , _) = px₁

instance
    latticeInterpretationᶜ : LatticeInterpretation isLatticeᶜ
    latticeInterpretationᶜ = record
        { ⟦_⟧ = ⟦_⟧ᶜ
        ; ⟦⟧-respects-≈ = ⟦⟧ᶜ-respects-≈ᶜ
        ; ⟦⟧-⊔-∨ = ⟦⟧ᶜ-⊔ᶜ-∨
        ; ⟦⟧-⊓-∧ = ⟦⟧ᶜ-⊓ᶜ-∧
        }

module WithProg (prog : Program) where
    open Program prog

    open import Analysis.Forward.Lattices ConstLattice prog
    open import Analysis.Forward.Evaluation ConstLattice prog
    open import Analysis.Forward.Adapters ConstLattice prog

    eval : ∀ (e : Expr) → VariableValues → ConstLattice
    eval (e₁ + e₂) vs = plus (eval e₁ vs) (eval e₂ vs)
    eval (e₁ - e₂) vs = minus (eval e₁ vs) (eval e₂ vs)
    eval (` k) vs
        with ∈k-decᵛ k (proj₁ (proj₁ vs))
    ...   | yes k∈vs = proj₁ (locateᵛ {k} {vs} k∈vs)
    ...   | no _ = ⊤ᶜ
    eval (# n) _ = [ + n ]ᶜ

    eval-Monoʳ : ∀ (e : Expr) → Monotonic _≼ᵛ_ _≼ᶜ_ (eval e)
    eval-Monoʳ (e₁ + e₂) {vs₁} {vs₂} vs₁≼vs₂ =
        eval-combine₂ (λ {x} {y} {z} →  ≼ᶜ-trans {x} {y} {z})
                      plus plus-Mono₂ {o₁ = eval e₁ vs₁}
                      (eval-Monoʳ e₁ vs₁≼vs₂) (eval-Monoʳ e₂ vs₁≼vs₂)
    eval-Monoʳ (e₁ - e₂) {vs₁} {vs₂} vs₁≼vs₂ =
        eval-combine₂ (λ {x} {y} {z} →  ≼ᶜ-trans {x} {y} {z})
                      minus minus-Mono₂ {o₁ = eval e₁ vs₁}
                      (eval-Monoʳ e₁ vs₁≼vs₂) (eval-Monoʳ e₂ vs₁≼vs₂)
    eval-Monoʳ (` k) {vs₁@((kvs₁ , _) , _)} {vs₂@((kvs₂ , _), _)} vs₁≼vs₂
        with ∈k-decᵛ k kvs₁ | ∈k-decᵛ k kvs₂
    ...   | yes k∈kvs₁ | yes k∈kvs₂ =
            let
                (v₁ , k,v₁∈vs₁) = locateᵛ {k} {vs₁} k∈kvs₁
                (v₂ , k,v₂∈vs₂) = locateᵛ {k} {vs₂} k∈kvs₂
            in
                m₁≼m₂⇒m₁[k]ᵛ≼m₂[k]ᵛ vs₁ vs₂ vs₁≼vs₂ k,v₁∈vs₁ k,v₂∈vs₂
    ...   | yes k∈kvs₁ | no k∉kvs₂ = ⊥-elim (k∉kvs₂ (subst (λ l → k ∈ˡ l) (all-equal-keysᵛ vs₁ vs₂) k∈kvs₁))
    ...   | no k∉kvs₁ | yes k∈kvs₂ = ⊥-elim (k∉kvs₁ (subst (λ l → k ∈ˡ l) (all-equal-keysᵛ vs₂ vs₁) k∈kvs₂))
    ...   | no k∉kvs₁ | no k∉kvs₂ = IsLattice.≈-refl isLatticeᶜ
    eval-Monoʳ (# n) _ = ≼ᶜ-refl ([ + n ]ᶜ)

    instance
        ConstEval : ExprEvaluator
        ConstEval = record { eval = eval; eval-Monoʳ = eval-Monoʳ }

    -- For debugging purposes, print out the result.
    output = show (Analysis.Forward.WithProg.result ConstLattice prog)

    -- This should have fewer cases -- the same number as the actual 'plus' above.
    -- But agda only simplifies on first argument, apparently, so we are stuck
    -- listing them all.
    plus-valid : ∀ {g₁ g₂} {z₁ z₂} → ⟦ g₁ ⟧ᶜ (↑ᶻ z₁) → ⟦ g₂ ⟧ᶜ (↑ᶻ z₂) → ⟦ plus g₁ g₂ ⟧ᶜ (↑ᶻ (z₁ Int.+ z₂))
    plus-valid {⊥ᶜ} {_} ⊥ _ = ⊥
    plus-valid {[ z ]ᶜ} {⊥ᶜ} _ ⊥ = ⊥
    plus-valid {⊤ᶜ} {⊥ᶜ} _ ⊥ = ⊥
    plus-valid {⊤ᶜ} {[ z ]ᶜ} _ _ = tt
    plus-valid {⊤ᶜ} {⊤ᶜ} _ _ = tt
    plus-valid {[ z₁ ]ᶜ} {[ z₂ ]ᶜ} refl refl = refl
    plus-valid {[ z ]ᶜ} {⊤ᶜ} _ _ = tt
    --
    -- Same for this one. It should be easier, but Agda won't simplify.
    minus-valid : ∀ {g₁ g₂} {z₁ z₂} → ⟦ g₁ ⟧ᶜ (↑ᶻ z₁) → ⟦ g₂ ⟧ᶜ (↑ᶻ z₂) → ⟦ minus g₁ g₂ ⟧ᶜ (↑ᶻ (z₁ Int.- z₂))
    minus-valid {⊥ᶜ} {_} ⊥ _ = ⊥
    minus-valid {[ z ]ᶜ} {⊥ᶜ} _ ⊥ = ⊥
    minus-valid {⊤ᶜ} {⊥ᶜ} _ ⊥ = ⊥
    minus-valid {⊤ᶜ} {[ z ]ᶜ} _ _ = tt
    minus-valid {⊤ᶜ} {⊤ᶜ} _ _ = tt
    minus-valid {[ z₁ ]ᶜ} {[ z₂ ]ᶜ} refl refl = refl
    minus-valid {[ z ]ᶜ} {⊤ᶜ} _ _ = tt

    eval-valid : IsValidExprEvaluator
    eval-valid (⇒ᵉ-+ ρ e₁ e₂ z₁ z₂ ρ,e₁⇒z₁ ρ,e₂⇒z₂) ⟦vs⟧ρ =
        plus-valid (eval-valid ρ,e₁⇒z₁ ⟦vs⟧ρ) (eval-valid ρ,e₂⇒z₂ ⟦vs⟧ρ)
    eval-valid (⇒ᵉ-- ρ e₁ e₂ z₁ z₂ ρ,e₁⇒z₁ ρ,e₂⇒z₂) ⟦vs⟧ρ =
        minus-valid (eval-valid ρ,e₁⇒z₁ ⟦vs⟧ρ) (eval-valid ρ,e₂⇒z₂ ⟦vs⟧ρ)
    eval-valid {vs} (⇒ᵉ-Var ρ x v x,v∈ρ) ⟦vs⟧ρ
        with ∈k-decᵛ x (proj₁ (proj₁ vs))
    ...   | yes x∈kvs = ⟦vs⟧ρ (proj₂ (locateᵛ {x} {vs} x∈kvs)) x,v∈ρ
    ...   | no x∉kvs = tt
    eval-valid (⇒ᵉ-ℕ ρ n) _ = refl

    instance
        ConstEvalValid : ValidExprEvaluator ConstEval latticeInterpretationᶜ
        ConstEvalValid = record { valid = eval-valid }

    analyze-correct = Analysis.Forward.WithProg.analyze-correct ConstLattice prog tt