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

module OWL2.Kernel.Regularity where

open import OWL2.Prelude public
open import OWL2.Kernel.Signature public
  using (Signature)
open import OWL2.Kernel.Name public
  using (ObjectPropertyName)

record RegularityContext (Sig : Signature) : Type₀ where
  constructor regularityContext
  field
    simpleObjectProperty? :
      ObjectPropertyName Sig → Bool

open RegularityContext public

trivialRegularityContext : {Sig : Signature} → RegularityContext Sig
trivialRegularityContext =
  regularityContext (λ property → true)

SimpleDecision : Bool → Type₀
SimpleDecision true =
  Unit
SimpleDecision false =
  ⊥

record SimpleObjectProperty
  (Sig : Signature) (p : ObjectPropertyName Sig) : Type₀ where
  constructor simpleObjectProperty
  field
    simpleContext :
      RegularityContext Sig
    simpleDecision :
      SimpleDecision (simpleObjectProperty? simpleContext p)

open SimpleObjectProperty public

trivialSimpleObjectProperty :
  {Sig : Signature} →
  (p : ObjectPropertyName Sig) →
  SimpleObjectProperty Sig p
trivialSimpleObjectProperty p =
  simpleObjectProperty trivialRegularityContext tt

simpleObjectPropertyEvidenceFromDecision :
  {Sig : Signature} →
  (simple? : ObjectPropertyName Sig → Bool) →
  (p : ObjectPropertyName Sig) →
  (decision : Bool) →
  decision ≡ simple? p →
  Optional (SimpleObjectProperty Sig p)
simpleObjectPropertyEvidenceFromDecision simple? p true equality =
  present
    (simpleObjectProperty
      (regularityContext simple?)
      (subst SimpleDecision equality tt))
simpleObjectPropertyEvidenceFromDecision simple? p false equality =
  absent

simpleObjectPropertyEvidence? :
  {Sig : Signature} →
  (context : RegularityContext Sig) →
  (p : ObjectPropertyName Sig) →
  Optional (SimpleObjectProperty Sig p)
simpleObjectPropertyEvidence? (regularityContext simple?) p =
  simpleObjectPropertyEvidenceFromDecision
    simple?
    p
    (simple? p)
    refl

record SimpleObjectPropertyName (Sig : Signature) : Type₀ where
  constructor simpleObjectPropertyName
  field
    property : ObjectPropertyName Sig
    simple   : SimpleObjectProperty Sig property

open SimpleObjectPropertyName public