module SMT.Examples.Showcase where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Bool.Base using (true; false)
open import Cubical.Data.Int.Base using (ℤ; negsuc; pos)
open import Cubical.Data.List.Base using (List; []; _∷_)
open import Cubical.Data.Unit.Base using (tt)
open import Cubical.Relation.Nullary.Base using (¬_)

open import SMT.Core
open import SMT.Derived
open import SMT.Syntax

one : ℤ
one = pos 

minusOne : ℤ
minusOne = negsuc 

Gclamp : Ctx
Gclamp = decl "lo" sInt ∷ decl "hi" sInt ∷ decl "x" sInt ∷ []

loC : Expr Gclamp sInt
loC = var vz

hiC : Expr Gclamp sInt
hiC = var (vs vz)

xC : Expr Gclamp sInt
xC = var (vs (vs vz))

clampedC : Expr Gclamp sInt
clampedC = iClamp loC hiC xC

valid-clamp-between : Problem Gclamp
valid-clamp-between =
  (loC ≤ᵢ hiC ∷ []) ⊢ [ loC ≤ᵢ clampedC ≤ᵢ hiC ]

invalid-clamp-between-unordered : Problem Gclamp
invalid-clamp-between-unordered =
  [] ⊢ [ loC ≤ᵢ clampedC ≤ᵢ hiC ]

invalid-clamp-between-unordered-counterexample :
  Counterexample invalid-clamp-between-unordered
invalid-clamp-between-unordered-counterexample =
  counterexample
    (one , (z0 , (z0 , tt)))
    all[]
    refl

not-invalid-clamp-between-unordered :
  ¬ Statement invalid-clamp-between-unordered
not-invalid-clamp-between-unordered =
  refute invalid-clamp-between-unordered-counterexample

Gintervals : Ctx
Gintervals =
  decl "a" sInt ∷ decl "b" sInt ∷ decl "c" sInt ∷ decl "d" sInt ∷ []

aI : Expr Gintervals sInt
aI = var vz

bI : Expr Gintervals sInt
bI = var (vs vz)

cI : Expr Gintervals sInt
cI = var (vs (vs vz))

dI : Expr Gintervals sInt
dI = var (vs (vs (vs vz)))

interval-meet-lower : Expr Gintervals sInt
interval-meet-lower = iMax aI cI

interval-meet-upper : Expr Gintervals sInt
interval-meet-upper = iMin bI dI

intervals-overlap : Expr Gintervals sBool
intervals-overlap = ¬ᵇ (bI <ᵢ cI ∨ᵇ dI <ᵢ aI)

valid-overlapping-interval-meet : Problem Gintervals
valid-overlapping-interval-meet =
  ( aI ≤ᵢ bI
    ∷ cI ≤ᵢ dI
    ∷ intervals-overlap
    ∷ []
  )
  ⊢ interval-meet-lower ≤ᵢ interval-meet-upper

invalid-disjoint-interval-meet : Problem Gintervals
invalid-disjoint-interval-meet =
  ( aI ≤ᵢ bI
    ∷ cI ≤ᵢ dI
    ∷ []
  )
  ⊢ interval-meet-lower ≤ᵢ interval-meet-upper

invalid-disjoint-interval-meet-counterexample :
  Counterexample invalid-disjoint-interval-meet
invalid-disjoint-interval-meet-counterexample =
  counterexample
    (z0 , (z0 , (z1 , (z1 , tt))))
    (refl all∷ (refl all∷ all[]))
    refl

not-invalid-disjoint-interval-meet :
  ¬ Statement invalid-disjoint-interval-meet
not-invalid-disjoint-interval-meet =
  refute invalid-disjoint-interval-meet-counterexample

Gdelta : Ctx
Gdelta = decl "x" sInt ∷ decl "y" sInt ∷ decl "delta" sInt ∷ []

xD : Expr Gdelta sInt
xD = var vz

yD : Expr Gdelta sInt
yD = var (vs vz)

deltaD : Expr Gdelta sInt
deltaD = var (vs (vs vz))

absolute-difference : Expr Gdelta sInt
absolute-difference = iAbs (xD -ᵢ yD)

valid-absolute-difference-window : Problem Gdelta
valid-absolute-difference-window =
  ( int0 ≤ᵢ deltaD
    ∷ absolute-difference ≤ᵢ deltaD
    ∷ []
  )
  ⊢ [ yD -ᵢ deltaD ≤ᵢ xD ≤ᵢ yD +ᵢ deltaD ]

Gload : Ctx
Gload =
  decl "p" sBool ∷
  decl "q" sBool ∷
  decl "x" sInt ∷
  decl "y" sInt ∷
  decl "z" sInt ∷
  decl "cap" sInt ∷
  []

pL : Expr Gload sBool
pL = var vz

qL : Expr Gload sBool
qL = var (vs vz)

xL : Expr Gload sInt
xL = var (vs (vs vz))

yL : Expr Gload sInt
yL = var (vs (vs (vs vz)))

zL : Expr Gload sInt
zL = var (vs (vs (vs (vs vz))))

capL : Expr Gload sInt
capL = var (vs (vs (vs (vs (vs vz)))))

selected-load : Expr Gload sInt
selected-load =
  (ifᵉ pL then xL else int0) +ᵢ (ifᵉ qL then yL else int0) +ᵢ zL

both-selected : Expr Gload sBool
both-selected = pL ∧ᵇ qL

only-x-selected : Expr Gload sBool
only-x-selected = pL ∧ᵇ ¬ᵇ qL

only-y-selected : Expr Gload sBool
only-y-selected = ¬ᵇ pL ∧ᵇ qL

none-selected : Expr Gload sBool
none-selected = ¬ᵇ pL ∧ᵇ ¬ᵇ qL

both-load : Expr Gload sInt
both-load = xL +ᵢ yL +ᵢ zL

only-x-load : Expr Gload sInt
only-x-load = xL +ᵢ zL

only-y-load : Expr Gload sInt
only-y-load = yL +ᵢ zL

complete-load-assumptions : List (Expr Gload sBool)
complete-load-assumptions =
  int0 ≤ᵢ zL
  ∷ pL ⇒ᵇ int0 ≤ᵢ xL
  ∷ qL ⇒ᵇ int0 ≤ᵢ yL
  ∷ both-selected ⇒ᵇ both-load ≤ᵢ capL
  ∷ only-x-selected ⇒ᵇ only-x-load ≤ᵢ capL
  ∷ only-y-selected ⇒ᵇ only-y-load ≤ᵢ capL
  ∷ none-selected ⇒ᵇ zL ≤ᵢ capL
  ∷ []

valid-mode-selected-load-bounded : Problem Gload
valid-mode-selected-load-bounded =
  complete-load-assumptions ⊢ [ int0 ≤ᵢ selected-load ≤ᵢ capL ]

missing-both-load-assumptions : List (Expr Gload sBool)
missing-both-load-assumptions =
  int0 ≤ᵢ zL
  ∷ pL ⇒ᵇ int0 ≤ᵢ xL
  ∷ qL ⇒ᵇ int0 ≤ᵢ yL
  ∷ only-x-selected ⇒ᵇ only-x-load ≤ᵢ capL
  ∷ only-y-selected ⇒ᵇ only-y-load ≤ᵢ capL
  ∷ none-selected ⇒ᵇ zL ≤ᵢ capL
  ∷ []

invalid-mode-selected-load-missing-both-case : Problem Gload
invalid-mode-selected-load-missing-both-case =
  missing-both-load-assumptions ⊢ [ int0 ≤ᵢ selected-load ≤ᵢ capL ]

invalid-mode-selected-load-missing-both-case-counterexample :
  Counterexample invalid-mode-selected-load-missing-both-case
invalid-mode-selected-load-missing-both-case-counterexample =
  counterexample
    (true , (true , (z1 , (z1 , (z0 , (z1 , tt))))))
    ( refl all∷
      (refl all∷
      (refl all∷
      (refl all∷
      (refl all∷
      (refl all∷ all[])))))
    )
    refl

not-invalid-mode-selected-load-missing-both-case :
  ¬ Statement invalid-mode-selected-load-missing-both-case
not-invalid-mode-selected-load-missing-both-case =
  refute invalid-mode-selected-load-missing-both-case-counterexample

missing-y-nonnegative-assumptions : List (Expr Gload sBool)
missing-y-nonnegative-assumptions =
  int0 ≤ᵢ zL
  ∷ pL ⇒ᵇ int0 ≤ᵢ xL
  ∷ both-selected ⇒ᵇ both-load ≤ᵢ capL
  ∷ only-x-selected ⇒ᵇ only-x-load ≤ᵢ capL
  ∷ only-y-selected ⇒ᵇ only-y-load ≤ᵢ capL
  ∷ none-selected ⇒ᵇ zL ≤ᵢ capL
  ∷ []

invalid-mode-selected-load-missing-y-nonnegative : Problem Gload
invalid-mode-selected-load-missing-y-nonnegative =
  missing-y-nonnegative-assumptions ⊢ [ int0 ≤ᵢ selected-load ≤ᵢ capL ]

invalid-mode-selected-load-missing-y-nonnegative-counterexample :
  Counterexample invalid-mode-selected-load-missing-y-nonnegative
invalid-mode-selected-load-missing-y-nonnegative-counterexample =
  counterexample
    (false , (true , (z0 , (minusOne , (z0 , (z0 , tt))))))
    ( refl all∷
      (refl all∷
      (refl all∷
      (refl all∷
      (refl all∷
      (refl all∷ all[])))))
    )
    refl

not-invalid-mode-selected-load-missing-y-nonnegative :
  ¬ Statement invalid-mode-selected-load-missing-y-nonnegative
not-invalid-mode-selected-load-missing-y-nonnegative =
  refute invalid-mode-selected-load-missing-y-nonnegative-counterexample