module Chapter7.Derivable where

open import Function

open import Level

open import Data.Bool 
open import Data.Empty
open import Data.Maybe hiding (Eq)
open import Data.Unit hiding (_≟_)
open import Data.Nat hiding (compare ; _≟_ ; pred ; suc)
open import Data.Fin hiding (pred ; suc)
open import Data.Product
open import Data.Sum

open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

open import Chapter4.Desc
open import Chapter4.Desc.Fixpoint



SemiDec : ∀{ℓ} → Set ℓ → Set ℓ
SemiDec A = Maybe A

IsTrue : ∀ {ℓ} {P : Set ℓ} → SemiDec P → Set
IsTrue (just _) = ⊤
IsTrue nothing = ⊥

toSemiWitness : ∀{ℓ} {P : Set ℓ} {Q : SemiDec P} → IsTrue Q → P
toSemiWitness {Q = just p} _  = p
toSemiWitness {Q = nothing} ()


record Derive {ℓ : Level}(P : Desc ℓ → Set) : Set (suc (suc ℓ)) where
  field
    subUniverse : Desc ℓ → Set (suc ℓ)
    belongTo : (D : Desc ℓ) → SemiDec (subUniverse D)
    derive : {D : Desc ℓ} → subUniverse D → P D

deriving : ∀{ℓ}{P} → (prop : Derive P)(D : Desc ℓ) → IsTrue (Derive.belongTo prop D) → P D
deriving prop D q = Derive.derive prop (toSemiWitness {Q = belongTo D} q)
  where open Derive prop