module SMT.Syntax where

open import Cubical.Data.Bool.Base using (Bool; true; false)
open import Cubical.Data.Int.Base using (ℤ)
open import Cubical.Data.List.Base using (List; [])

open import SMT.Core
open import SMT.Derived

infixr  _⊢_
infixr  _⇒ᵇ_
infixr  _∨ᵇ_ _⊕ᵇ_
infixr  _∧ᵇ_
infix   _⇔ᵇ_
infix   _≡ᵢ_ _≠ᵢ_ _≤ᵢ_ _<ᵢ_ _≥ᵢ_ _>ᵢ_
infix   [_≤ᵢ_≤ᵢ_]
infixl  _+ᵢ_ _-ᵢ_
infixl  _·ᵢ_
infix   ¬ᵇ_ -ᵢ_
infix   ifᵉ_then_else_

𝔹 : ∀ {Γ} → Bool → Expr Γ sBool
𝔹 = bool

ℤᵉ : ∀ {Γ} → ℤ → Expr Γ sInt
ℤᵉ = int

⊤ᵇ : ∀ {Γ} → Expr Γ sBool
⊤ᵇ = bool true

⊥ᵇ : ∀ {Γ} → Expr Γ sBool
⊥ᵇ = bool false

_⊢_ : ∀ {Γ} → List (Expr Γ sBool) → Expr Γ sBool → Problem Γ
ps ⊢ p = problem ps p

_+ᵢ_ : ∀ {Γ} → Expr Γ sInt → Expr Γ sInt → Expr Γ sInt
_+ᵢ_ = iAdd

_-ᵢ_ : ∀ {Γ} → Expr Γ sInt → Expr Γ sInt → Expr Γ sInt
_-ᵢ_ = iSub

-ᵢ_ : ∀ {Γ} → Expr Γ sInt → Expr Γ sInt
-ᵢ_ = iNeg

_·ᵢ_ : ∀ {Γ} → ℤ → Expr Γ sInt → Expr Γ sInt
_·ᵢ_ = iScale

_≡ᵢ_ : ∀ {Γ} → Expr Γ sInt → Expr Γ sInt → Expr Γ sBool
_≡ᵢ_ = iEq

_≠ᵢ_ : ∀ {Γ} → Expr Γ sInt → Expr Γ sInt → Expr Γ sBool
_≠ᵢ_ = iNe

_≤ᵢ_ : ∀ {Γ} → Expr Γ sInt → Expr Γ sInt → Expr Γ sBool
_≤ᵢ_ = iLe

_<ᵢ_ : ∀ {Γ} → Expr Γ sInt → Expr Γ sInt → Expr Γ sBool
_<ᵢ_ = iLt

_≥ᵢ_ : ∀ {Γ} → Expr Γ sInt → Expr Γ sInt → Expr Γ sBool
_≥ᵢ_ = iGe

_>ᵢ_ : ∀ {Γ} → Expr Γ sInt → Expr Γ sInt → Expr Γ sBool
_>ᵢ_ = iGt

[_≤ᵢ_≤ᵢ_] : ∀ {Γ} → Expr Γ sInt → Expr Γ sInt → Expr Γ sInt → Expr Γ sBool
[ lo ≤ᵢ x ≤ᵢ hi ] = between lo x hi

¬ᵇ_ : ∀ {Γ} → Expr Γ sBool → Expr Γ sBool
¬ᵇ_ = bNot

_∧ᵇ_ : ∀ {Γ} → Expr Γ sBool → Expr Γ sBool → Expr Γ sBool
_∧ᵇ_ = bAnd

_∨ᵇ_ : ∀ {Γ} → Expr Γ sBool → Expr Γ sBool → Expr Γ sBool
_∨ᵇ_ = bOr

_⊕ᵇ_ : ∀ {Γ} → Expr Γ sBool → Expr Γ sBool → Expr Γ sBool
_⊕ᵇ_ = bXor

_⇒ᵇ_ : ∀ {Γ} → Expr Γ sBool → Expr Γ sBool → Expr Γ sBool
_⇒ᵇ_ = bImp

_⇔ᵇ_ : ∀ {Γ} → Expr Γ sBool → Expr Γ sBool → Expr Γ sBool
_⇔ᵇ_ = bEq

ifᵉ_then_else_ : ∀ {Γ s} → Expr Γ sBool → Expr Γ s → Expr Γ s → Expr Γ s
ifᵉ c then t else f = ite c t f