{-# OPTIONS --without-K #-}
module Class.Decidable.Core where
 
open import Class.Prelude
open import Class.Core
 
open import Relation.Nullary.Decidable using (True; False; toWitness; toWitnessFalse)
 
record _⁇ (P : Type ℓ) : Type ℓ where
  constructor ⁇_
  field dec : Dec P
 
  auto : ⦃ True dec ⦄ → P
  auto ⦃ pr ⦄ = toWitness pr
 
  contradict : ∀ {X : Type} {pr : False dec} → P → X
  contradict {pr = pr} = ⊥-elim ∘ toWitnessFalse pr
 
open _⁇ ⦃...⦄ public
 
¿_¿ : ∀ (X : Type ℓ) → ⦃ X ⁇ ⦄ → Dec X
¿ _ ¿ = dec
 
¿_¿ᵇ : (P : Type ℓ) → ⦃ P ⁇ ⦄ → Bool
¿ P ¿ᵇ = ⌊ ¿ P ¿ ⌋
 
infix  ifᵈ_then_else_
ifᵈ_then_else_ : ∀ {X : Type ℓ} (P : Type ℓ′)
  → ⦃ P ⁇ ⦄ → ({_ : P} → X) → ({_ : ¬ P} → X) → X
ifᵈ P then t else f with ¿ P ¿
... | yes p = t {p}
... | no ¬p = f {¬p}
 
_⁇¹ = _⁇ ¹
_⁇² = _⁇ ²
_⁇³ = _⁇ ³
 
module _ {A : Type ℓ} where
 
  module _ {P : Pred A ℓ′} where
 
    dec¹ : ⦃ P ⁇¹ ⦄ → Decidable¹ P
    dec¹ _ = dec
 
    ⁇¹_ : Decidable¹ P → P ⁇¹
    ⁇¹ p? = ⁇ (p? _)
 
  ¿_¿¹ : (P : Pred A ℓ′) → ⦃ P ⁇¹ ⦄ → Decidable¹ P
  ¿ _ ¿¹ = dec¹
 
module _ {A B : Type ℓ} where
 
  module _ {R : REL A B ℓ′} where
 
    dec² : ⦃ R ⁇² ⦄ → Decidable² R
    dec² _ _ = dec
 
    ⁇²_ : Decidable² R → R ⁇²
    ⁇² p? = ⁇ (p? _ _)
 
  ¿_¿² : (R : REL A B ℓ′) → ⦃ R ⁇² ⦄ → Decidable² R
  ¿ _ ¿² = dec²
 
module _ {A B C : Type ℓ} where
 
  module _ {R : 3REL A B C ℓ′} where
 
    dec³ : ⦃ R ⁇³ ⦄ → Decidable³ R
    dec³ _ _ _ = dec
 
    ⁇³_ : Decidable³ R → R ⁇³
    ⁇³_ p? = ⁇ (p? _ _ _)
 
  ¿_¿³ : (R : 3REL A B C ℓ′) → ⦃ R ⁇³ ⦄ → Decidable³ R
  ¿ _ ¿³ = dec³
 
infix -100 auto∶_
auto∶_ : ∀ (X : Type ℓ) → ⦃ X ⁇ ⦄ → Type
auto∶_ A = True ¿ A ¿
 
dec-✓ : ∀ {P : Type ℓ} ⦃ _ : P ⁇ ⦄ (p : P) → ∃[ p′ ] ¿ P ¿ ≡ yes p′
dec-✓ = dec-yes ¿ _ ¿