{-# OPTIONS --without-K #-}
module Class.Decidable.Instances where
 
open import Class.Prelude
open import Class.Decidable.Core
open import Class.DecEq.Core
 
private variable
  n : ℕ
  x : A
  P Q : Pred A ℓ
  R : Rel A ℓ
 
instance
 
  -- ** deriving from DecEq
  DecEq⇒Dec : ⦃ DecEq A ⦄ → _≡_ {A = A} ⁇²
  DecEq⇒Dec = ⁇² _≟_
 
  -- ** basic type formers
 
  Dec-⊥ : ⊥ ⁇
  Dec-⊥ .dec = no λ()
 
  Dec-⊤ : ⊤ ⁇
  Dec-⊤ .dec = yes tt
 
  open import Relation.Nullary.Decidable as D
 
  Dec-→ : ⦃ A ⁇ ⦄ → ⦃ B ⁇ ⦄ → (A → B) ⁇
  Dec-→ .dec = dec D.→-dec dec
 
  -- ** products
 
  Dec-× : ⦃ A ⁇ ⦄ → ⦃ B ⁇ ⦄ → (A × B) ⁇
  Dec-× .dec = dec D.×-dec dec
 
  -- ** sums
 
  Dec-⊎ : ⦃ A ⁇ ⦄ → ⦃ B ⁇ ⦄ → (A ⊎ B) ⁇
  Dec-⊎ .dec = dec D.⊎-dec dec
 
  import Data.Sum.Relation.Unary.All as ⊎; open ⊎ using (inj₁; inj₂)
  open import Relation.Nullary.Decidable using () renaming (map′ to mapDec)
 
  Dec-⊎All : ⦃ P ⁇¹ ⦄ → ⦃ Q ⁇¹ ⦄ → ⊎.All P Q ⁇¹
  Dec-⊎All {P = P} {Q = Q} {x = inj₁ x} .dec = mapDec inj₁ inj₁˘ ¿ P x ¿
    where inj₁˘ : ⊎.All P Q (inj₁ x) → P x
          inj₁˘ (inj₁ x) = x
  Dec-⊎All {P = P} {Q = Q} {x = inj₂ y} .dec = mapDec inj₂ inj₂˘ ¿ Q y ¿
    where inj₂˘ : ⊎.All P Q (inj₂ x) → Q x
          inj₂˘ (inj₂ x) = x
 
  import Data.Bool as 𝔹
 
  Dec-T : T ⁇¹
  Dec-T = ⁇¹ 𝔹.T?
 
  import Data.List.Relation.Unary.All as L
  import Data.List.Relation.Unary.Any as L
 
  Dec-All : ⦃ P ⁇¹ ⦄ → L.All P ⁇¹
  Dec-All = ⁇¹ L.all? dec¹
 
  Dec-Any : ⦃ P ⁇¹ ⦄ → L.Any P ⁇¹
  Dec-Any = ⁇¹ L.any? dec¹
 
  import Data.List.Relation.Unary.AllPairs as AP
 
  Dec-AllPairs : ⦃ R ⁇² ⦄ → AP.AllPairs R ⁇¹
  Dec-AllPairs = ⁇¹ AP.allPairs? dec²
 
  open import Data.Vec as V
  open import Data.Vec.Relation.Unary.All as V
  open import Data.Vec.Relation.Unary.Any as V
 
  Dec-VAll : ⦃ P ⁇¹ ⦄ → V.All P {n} ⁇¹
  Dec-VAll = ⁇¹ V.all? dec¹
 
  Dec-VAny : ⦃ P ⁇¹ ⦄ → V.Any P {n} ⁇¹
  Dec-VAny = ⁇¹ V.any? dec¹
 
  import Data.Maybe as M
  import Data.Maybe.Relation.Unary.All as M renaming (dec to all?)
  import Data.Maybe.Relation.Unary.Any as M renaming (dec to any?)
 
  Dec-MAll : ⦃ P ⁇¹ ⦄ → M.All P ⁇¹
  Dec-MAll = ⁇¹ M.all? dec¹
 
  Dec-MAny : ⦃ P ⁇¹ ⦄ → M.Any P ⁇¹
  Dec-MAny = ⁇¹ M.any? dec¹
 
  -- ** inequalities
 
  import Data.Nat.Properties as ℕ
 
  ℕ-Dec-≤ = ⁇² ℕ._≤?_
  ℕ-Dec-< = ⁇² ℕ._<?_
 
  import Data.Integer.Properties as ℤ
 
  ℤ-Dec-≤ = ⁇² ℤ._≤?_
  ℤ-Dec-< = ⁇² ℤ._<?_
 
  import Data.Rational.Properties as Rat
 
  ℚ-Dec-≤ = ⁇² Rat._≤?_
  ℚ-Dec-< = ⁇² Rat._<?_