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

module OWL2.Portable.Check.PropertyRoles where

open import OWL2.Prelude
open import OWL2.Check.Result
open import OWL2.Diagnostics
import OWL2.Portable.Check.Core as Core
import OWL2.Portable.PropertyKinds as PropertyKinds
import OWL2.Portable.Syntax as P

record PropertyRoleEvidence (document : P.OntologyDocument) : Type₀ where
  constructor propertyRoleEvidence
  field
    sourceDocument :
      P.OntologyDocument
    sourcePreserved :
      sourceDocument ≡ document
    propertyUsageFacts :
      List PropertyKinds.PropertyUsageFact
    propertyRoleUsageConflicts :
      List PropertyKinds.PropertyUsageConflict

open PropertyRoleEvidence public

record PropertyRoleCheckMeaning
  (document : P.OntologyDocument)
  (evidence : PropertyRoleEvidence document)
  : Type₀ where
  constructor propertyRoleCheckMeaning
  field
    propertyRoleSourcePreserved :
      sourceDocument evidence ≡ document
    propertyUsageFactsRecorded :
      propertyUsageFacts evidence ≡
      PropertyKinds.ontologyDocumentPropertyUsageFacts document
    propertyRoleUsageConflictsRecorded :
      propertyRoleUsageConflicts evidence ≡
      PropertyKinds.ontologyDocumentPropertyRoleUsageConflicts document

open PropertyRoleCheckMeaning public

PropertyRoleCheckResult : Type₀
PropertyRoleCheckResult =
  CheckResult
    P.OntologyDocument
    PropertyRoleEvidence
    PropertyRoleCheckMeaning

propertyRoleDiagnosticNamespace : String
propertyRoleDiagnosticNamespace =
  "owl2.portable.propertyRoles"

propertyRoleUsageConflictCode : DiagnosticCode
propertyRoleUsageConflictCode =
  mkDiagnosticCode
    propertyRoleDiagnosticNamespace
    "propertyRoleUsageConflict"

propertyRoleUsageConflictDiagnostic :
  PropertyKinds.PropertyUsageConflict →
  Diagnostic
propertyRoleUsageConflictDiagnostic conflict =
  diagnostic
    propertyRoleUsageConflictCode
    severityError
    rootSourcePath
    "property IRI is used in incompatible property roles"

propertyRoleUsageConflictDiagnostics :
  List PropertyKinds.PropertyUsageConflict →
  Diagnostics
propertyRoleUsageConflictDiagnostics [] =
  []
propertyRoleUsageConflictDiagnostics (conflict ∷ conflicts) =
  propertyRoleUsageConflictDiagnostic conflict
  ∷ propertyRoleUsageConflictDiagnostics conflicts

propertyRoleDiagnostics : P.OntologyDocument → Diagnostics
propertyRoleDiagnostics document =
  propertyRoleUsageConflictDiagnostics
    (PropertyKinds.ontologyDocumentPropertyRoleUsageConflicts document)

propertyRoleEvidenceFor :
  (document : P.OntologyDocument) →
  PropertyRoleEvidence document
propertyRoleEvidenceFor document =
  propertyRoleEvidence
    document
    refl
    (PropertyKinds.ontologyDocumentPropertyUsageFacts document)
    (PropertyKinds.ontologyDocumentPropertyRoleUsageConflicts document)

propertyRoleMeaningFor :
  (document : P.OntologyDocument) →
  (evidence : PropertyRoleEvidence document) →
  sourceDocument evidence ≡ document →
  propertyUsageFacts evidence ≡
    PropertyKinds.ontologyDocumentPropertyUsageFacts document →
  propertyRoleUsageConflicts evidence ≡
    PropertyKinds.ontologyDocumentPropertyRoleUsageConflicts document →
  PropertyRoleCheckMeaning document evidence
propertyRoleMeaningFor document evidence preserved facts conflicts =
  propertyRoleCheckMeaning preserved facts conflicts

checkPropertyRoles : P.OntologyDocument → PropertyRoleCheckResult
checkPropertyRoles document =
  Core.successfulResultWithDiagnostics
    (propertyRoleDiagnostics document)
    document
    evidence
    (propertyRoleMeaningFor document evidence refl refl refl)
  where
  evidence : PropertyRoleEvidence document
  evidence =
    propertyRoleEvidenceFor document