{-# OPTIONS --safe --cubical #-}

module OWL2.Check.Bundle where

open import Agda.Primitive using (_⊔_)
open import OWL2.Prelude

data EvidenceKind : Type₀ where
  declarationEvidence :
    EvidenceKind
  punningEvidence :
    EvidenceKind
  propertyRoleEvidence :
    EvidenceKind
  datatypeEvidence :
    EvidenceKind
  importClosureEvidence :
    EvidenceKind
  semanticSupportEvidence :
    EvidenceKind
  annotationErasureEvidence :
    EvidenceKind
  profileEvidence :
    EvidenceKind
  regularityEvidence :
    EvidenceKind

record StoredEvidence {ℓ : Level} {A : Type ℓ} (stored : A) : Type ℓ where
  constructor storedEvidence
  field
    storedValue :
      A
    storedValuePreserved :
      storedValue ≡ stored

open StoredEvidence public

storedEvidenceOf :
  ∀ {ℓ} {A : Type ℓ} →
  (value : A) →
  StoredEvidence value
storedEvidenceOf value =
  storedEvidence value refl

record EvidenceBundle
  {ℓᵈ ℓᵉ : Level}
  (Doc : Type ℓᵈ)
  (Evidence : Doc → EvidenceKind → Type ℓᵉ)
  : Type (ℓᵈ ⊔ ℓᵉ) where
  constructor evidenceBundle
  field
    document :
      Doc
    declarations :
      Optional (Evidence document declarationEvidence)
    punning :
      Optional (Evidence document punningEvidence)
    propertyRoles :
      Optional (Evidence document propertyRoleEvidence)
    datatypeMap :
      Optional (Evidence document datatypeEvidence)
    importClosure :
      Optional (Evidence document importClosureEvidence)
    semanticSupport :
      Optional (Evidence document semanticSupportEvidence)
    annotationErased :
      Optional (Evidence document annotationErasureEvidence)
    profile :
      Optional (Evidence document profileEvidence)
    regularity :
      Optional (Evidence document regularityEvidence)

open EvidenceBundle public