module SMT.Semantics where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Bool.Base
  using (Bool; true; false; not; Bool→Type; if_then_else_; _≟_)
open import Cubical.Data.Bool.Properties
  using
    ( Bool→Type×
    ; Bool→Type×'
    ; Bool→Type⊎
    ; Bool→Type⊎'
    ; Dec→DecBool
    ; DecBool→Dec
    )
open import Cubical.Data.Empty.Base as Empty
  using (⊥)
open import Cubical.Data.Int.Properties
  using (discreteℤ)
open import Cubical.Data.Int.Order
  using (_≤_; _<_; ≤Dec; <Dec)
open import Cubical.Data.List.Base
  using (List; []; _∷_)
open import Cubical.Data.Sigma.Base
  using (_×_; _,_)
open import Cubical.Data.Sum.Base
  using (_⊎_; inl; inr)
open import Cubical.Data.Unit.Base
  using (Unit; tt)
open import Cubical.Relation.Nullary.Base
  using (¬_; yes; no)

open import SMT.Core

Holds : ∀ {Γ} → Env Γ → Expr Γ sBool → Type₀
Holds ρ p = Bool→Type (eval ρ p)

Refutes : ∀ {Γ} → Env Γ → Expr Γ sBool → Type₀
Refutes ρ p = Bool→Type (not (eval ρ p))

holds→true : ∀ {Γ} {ρ : Env Γ} {p : Expr Γ sBool} → Holds ρ p → eval ρ p ≡ true
holds→true {ρ = ρ} {p = p} h with eval ρ p
... | true = refl
... | false = Empty.rec h

true→holds : ∀ {Γ} {ρ : Env Γ} {p : Expr Γ sBool} → eval ρ p ≡ true → Holds ρ p
true→holds p = subst Bool→Type (sym p) tt

refutes→false : ∀ {Γ} {ρ : Env Γ} {p : Expr Γ sBool} → Refutes ρ p → eval ρ p ≡ false
refutes→false {ρ = ρ} {p = p} h with eval ρ p
... | true = Empty.rec h
... | false = refl

false→refutes : ∀ {Γ} {ρ : Env Γ} {p : Expr Γ sBool} → eval ρ p ≡ false → Refutes ρ p
false→refutes {ρ = ρ} {p = p} q with eval ρ p
... | true = false≠true (sym q)
... | false = tt

data AllHolds {Γ : Ctx} : List (Expr Γ sBool) → Env Γ → Type₀ where
  allHolds[]   : ∀ {ρ} → AllHolds [] ρ
  _holds∷_ : ∀ {ρ p ps} → Holds ρ p → AllHolds ps ρ → AllHolds (p ∷ ps) ρ

allHolds→allTrue : ∀ {Γ} {ρ : Env Γ} {ps} → AllHolds ps ρ → AllTrue ps ρ
allHolds→allTrue allHolds[] = all[]
allHolds→allTrue {ρ = ρ} {ps = p ∷ ps} (hp holds∷ hps) =
  holds→true {ρ = ρ} {p = p} hp all∷ allHolds→allTrue {ρ = ρ} {ps = ps} hps

allTrue→allHolds : ∀ {Γ} {ρ : Env Γ} {ps} → AllTrue ps ρ → AllHolds ps ρ
allTrue→allHolds all[] = allHolds[]
allTrue→allHolds {ρ = ρ} {ps = p ∷ ps} (hp all∷ hps) =
  true→holds {ρ = ρ} {p = p} hp holds∷ allTrue→allHolds {ρ = ρ} {ps = ps} hps

SemanticStatement : ∀ {Γ} → Problem Γ → Type₀
SemanticStatement {Γ = Γ} p =
  (ρ : Env Γ) → AllHolds (assumptions p) ρ → Holds ρ (claim p)

statement→semantic : ∀ {Γ} {p : Problem Γ} → Statement p → SemanticStatement p
statement→semantic {p = p} st ρ ps =
  true→holds {ρ = ρ} {p = claim p} (st ρ (allHolds→allTrue ps))

semantic→statement : ∀ {Γ} {p : Problem Γ} → SemanticStatement p → Statement p
semantic→statement {p = p} st ρ ps =
  holds→true {ρ = ρ} {p = claim p} (st ρ (allTrue→allHolds ps))

record SemanticCounterexample {Γ : Ctx} (p : Problem Γ) : Type₀ where
  constructor semanticCounterexample
  field
    env             : Env Γ
    assumptionsHold : AllHolds (assumptions p) env
    claimRefuted    : Refutes env (claim p)

open SemanticCounterexample public

semanticCounterexample→Counterexample :
  ∀ {Γ} {p : Problem Γ} → SemanticCounterexample p → Counterexample p
semanticCounterexample→Counterexample {p = p} c =
  counterexample
    (env c)
    (allHolds→allTrue (assumptionsHold c))
    (refutes→false {ρ = env c} {p = claim p} (claimRefuted c))

refuteSemantic : ∀ {Γ} {p : Problem Γ} → SemanticCounterexample p → ¬ Statement p
refuteSemantic c = refute (semanticCounterexample→Counterexample c)

holds-refutes-contradiction :
  ∀ {Γ} {ρ : Env Γ} {p : Expr Γ sBool} → Holds ρ p → Refutes ρ p → ⊥
holds-refutes-contradiction {ρ = ρ} {p = p} hp rp with eval ρ p
... | true = Empty.rec rp
... | false = Empty.rec hp

NoCounterexample : ∀ {Γ} → Problem Γ → Type₀
NoCounterexample p = ¬ SemanticCounterexample p

semantic→noCounterexample :
  ∀ {Γ} {p : Problem Γ} → SemanticStatement p → NoCounterexample p
semantic→noCounterexample {p = p} st c =
  holds-refutes-contradiction {ρ = env c} {p = claim p}
    (st (env c) (assumptionsHold c))
    (claimRefuted c)

noCounterexample→semantic :
  ∀ {Γ} {p : Problem Γ} → NoCounterexample p → SemanticStatement p
noCounterexample→semantic {p = p} none ρ ps =
  go (eval ρ (claim p)) refl
  where
    go : (b : Bool) → eval ρ (claim p) ≡ b → Holds ρ (claim p)
    go true eq = true→holds {ρ = ρ} {p = claim p} eq
    go false eq =
      Empty.rec
        (none (semanticCounterexample ρ ps (false→refutes {ρ = ρ} {p = claim p} eq)))

SatisfiableAssertions : ∀ {Γ} → List (Expr Γ sBool) → Type₀
SatisfiableAssertions {Γ = Γ} ps = Σ[ ρ ∈ Env Γ ] AllHolds ps ρ

SatisfiableProblem : ∀ {Γ} → Problem Γ → Type₀
SatisfiableProblem p = SatisfiableAssertions (assumptions p)

iEq-sound :
  ∀ {Γ} {ρ : Env Γ} {x y : Expr Γ sInt} →
  Holds ρ (iEq x y) → eval ρ x ≡ eval ρ y
iEq-sound {ρ = ρ} {x = x} {y = y} =
  DecBool→Dec (discreteℤ (eval ρ x) (eval ρ y))

iEq-complete :
  ∀ {Γ} {ρ : Env Γ} {x y : Expr Γ sInt} →
  eval ρ x ≡ eval ρ y → Holds ρ (iEq x y)
iEq-complete {ρ = ρ} {x = x} {y = y} =
  Dec→DecBool (discreteℤ (eval ρ x) (eval ρ y))

iNe-sound :
  ∀ {Γ} {ρ : Env Γ} {x y : Expr Γ sInt} →
  Holds ρ (iNe x y) → ¬ eval ρ x ≡ eval ρ y
iNe-sound {ρ = ρ} {x = x} {y = y} h with discreteℤ (eval ρ x) (eval ρ y)
... | yes p = Empty.rec h
... | no ¬p = ¬p

iNe-complete :
  ∀ {Γ} {ρ : Env Γ} {x y : Expr Γ sInt} →
  ¬ eval ρ x ≡ eval ρ y → Holds ρ (iNe x y)
iNe-complete {ρ = ρ} {x = x} {y = y} ¬p with discreteℤ (eval ρ x) (eval ρ y)
... | yes p = Empty.rec (¬p p)
... | no _ = tt

iLe-sound :
  ∀ {Γ} {ρ : Env Γ} {x y : Expr Γ sInt} →
  Holds ρ (iLe x y) → eval ρ x ≤ eval ρ y
iLe-sound {ρ = ρ} {x = x} {y = y} =
  DecBool→Dec (≤Dec (eval ρ x) (eval ρ y))

iLe-complete :
  ∀ {Γ} {ρ : Env Γ} {x y : Expr Γ sInt} →
  eval ρ x ≤ eval ρ y → Holds ρ (iLe x y)
iLe-complete {ρ = ρ} {x = x} {y = y} =
  Dec→DecBool (≤Dec (eval ρ x) (eval ρ y))

iLt-sound :
  ∀ {Γ} {ρ : Env Γ} {x y : Expr Γ sInt} →
  Holds ρ (iLt x y) → eval ρ x < eval ρ y
iLt-sound {ρ = ρ} {x = x} {y = y} =
  DecBool→Dec (<Dec (eval ρ x) (eval ρ y))

iLt-complete :
  ∀ {Γ} {ρ : Env Γ} {x y : Expr Γ sInt} →
  eval ρ x < eval ρ y → Holds ρ (iLt x y)
iLt-complete {ρ = ρ} {x = x} {y = y} =
  Dec→DecBool (<Dec (eval ρ x) (eval ρ y))

iGe-sound :
  ∀ {Γ} {ρ : Env Γ} {x y : Expr Γ sInt} →
  Holds ρ (iGe x y) → eval ρ y ≤ eval ρ x
iGe-sound {ρ = ρ} {x = x} {y = y} =
  DecBool→Dec (≤Dec (eval ρ y) (eval ρ x))

iGe-complete :
  ∀ {Γ} {ρ : Env Γ} {x y : Expr Γ sInt} →
  eval ρ y ≤ eval ρ x → Holds ρ (iGe x y)
iGe-complete {ρ = ρ} {x = x} {y = y} =
  Dec→DecBool (≤Dec (eval ρ y) (eval ρ x))

iGt-sound :
  ∀ {Γ} {ρ : Env Γ} {x y : Expr Γ sInt} →
  Holds ρ (iGt x y) → eval ρ y < eval ρ x
iGt-sound {ρ = ρ} {x = x} {y = y} =
  DecBool→Dec (<Dec (eval ρ y) (eval ρ x))

iGt-complete :
  ∀ {Γ} {ρ : Env Γ} {x y : Expr Γ sInt} →
  eval ρ y < eval ρ x → Holds ρ (iGt x y)
iGt-complete {ρ = ρ} {x = x} {y = y} =
  Dec→DecBool (<Dec (eval ρ y) (eval ρ x))

bEq-sound :
  ∀ {Γ} {ρ : Env Γ} {p q : Expr Γ sBool} →
  Holds ρ (bEq p q) → eval ρ p ≡ eval ρ q
bEq-sound {ρ = ρ} {p = p} {q = q} =
  DecBool→Dec (eval ρ p ≟ eval ρ q)

bEq-complete :
  ∀ {Γ} {ρ : Env Γ} {p q : Expr Γ sBool} →
  eval ρ p ≡ eval ρ q → Holds ρ (bEq p q)
bEq-complete {ρ = ρ} {p = p} {q = q} =
  Dec→DecBool (eval ρ p ≟ eval ρ q)

not-sound :
  ∀ {Γ} {ρ : Env Γ} {p : Expr Γ sBool} →
  Holds ρ (bNot p) → Refutes ρ p
not-sound h = h

not-complete :
  ∀ {Γ} {ρ : Env Γ} {p : Expr Γ sBool} →
  Refutes ρ p → Holds ρ (bNot p)
not-complete h = h

and-sound :
  ∀ {Γ} {ρ : Env Γ} {p q : Expr Γ sBool} →
  Holds ρ (bAnd p q) → Holds ρ p × Holds ρ q
and-sound {ρ = ρ} {p = p} {q = q} =
  Bool→Type× (eval ρ p) (eval ρ q)

and-complete :
  ∀ {Γ} {ρ : Env Γ} {p q : Expr Γ sBool} →
  Holds ρ p × Holds ρ q → Holds ρ (bAnd p q)
and-complete {ρ = ρ} {p = p} {q = q} =
  Bool→Type×' (eval ρ p) (eval ρ q)

or-sound :
  ∀ {Γ} {ρ : Env Γ} {p q : Expr Γ sBool} →
  Holds ρ (bOr p q) → Holds ρ p ⊎ Holds ρ q
or-sound {ρ = ρ} {p = p} {q = q} =
  Bool→Type⊎ (eval ρ p) (eval ρ q)

or-complete :
  ∀ {Γ} {ρ : Env Γ} {p q : Expr Γ sBool} →
  Holds ρ p ⊎ Holds ρ q → Holds ρ (bOr p q)
or-complete {ρ = ρ} {p = p} {q = q} =
  Bool→Type⊎' (eval ρ p) (eval ρ q)

xor-sound :
  ∀ {Γ} {ρ : Env Γ} {p q : Expr Γ sBool} →
  Holds ρ (bXor p q) → (Holds ρ p × Refutes ρ q) ⊎ (Refutes ρ p × Holds ρ q)
xor-sound {ρ = ρ} {p = p} {q = q} h with eval ρ p | eval ρ q
... | true | true = Empty.rec h
... | true | false = inl (tt , tt)
... | false | true = inr (tt , tt)
... | false | false = Empty.rec h

xor-complete :
  ∀ {Γ} {ρ : Env Γ} {p q : Expr Γ sBool} →
  (Holds ρ p × Refutes ρ q) ⊎ (Refutes ρ p × Holds ρ q) → Holds ρ (bXor p q)
xor-complete {ρ = ρ} {p = p} {q = q} h with eval ρ p | eval ρ q
... | true | true with h
...   | inl (_ , rq) = Empty.rec rq
...   | inr (rp , _) = Empty.rec rp
xor-complete {ρ = ρ} {p = p} {q = q} h | true | false = tt
xor-complete {ρ = ρ} {p = p} {q = q} h | false | true = tt
xor-complete {ρ = ρ} {p = p} {q = q} h | false | false with h
...   | inl (hp , _) = Empty.rec hp
...   | inr (_ , hq) = Empty.rec hq

xor-self-refuted :
  ∀ {Γ} {ρ : Env Γ} {p : Expr Γ sBool} → Refutes ρ (bXor p p)
xor-self-refuted {ρ = ρ} {p = p} with eval ρ p
... | true = tt
... | false = tt

imp-sound :
  ∀ {Γ} {ρ : Env Γ} {p q : Expr Γ sBool} →
  Holds ρ (bImp p q) → Holds ρ p → Holds ρ q
imp-sound {ρ = ρ} {p = p} {q = q} h hp with eval ρ p | eval ρ q
... | true | true = tt
... | true | false = Empty.rec h
... | false | true = tt
... | false | false = Empty.rec hp

imp-complete :
  ∀ {Γ} {ρ : Env Γ} {p q : Expr Γ sBool} →
  (Holds ρ p → Holds ρ q) → Holds ρ (bImp p q)
imp-complete {ρ = ρ} {p = p} {q = q} f with eval ρ p | eval ρ q
... | true | true = tt
... | true | false = Empty.rec (f tt)
... | false | true = tt
... | false | false = tt

ite-true :
  ∀ {Γ s} {ρ : Env Γ} {c : Expr Γ sBool} {t f : Expr Γ s} →
  Holds ρ c → eval ρ (ite c t f) ≡ eval ρ t
ite-true {ρ = ρ} {c = c} h with eval ρ c
... | true = refl
... | false = Empty.rec h

ite-false :
  ∀ {Γ s} {ρ : Env Γ} {c : Expr Γ sBool} {t f : Expr Γ s} →
  Refutes ρ c → eval ρ (ite c t f) ≡ eval ρ f
ite-false {ρ = ρ} {c = c} h with eval ρ c
... | true = Empty.rec h
... | false = refl