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

module OWL2.Portable.Check.Regularity where

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

record RegularityEvidence (document : P.OntologyDocument) : Type₀ where
  constructor regularityEvidence
  field
    sourceDocument :
      P.OntologyDocument
    sourcePreserved :
      sourceDocument ≡ document
    regularityReport :
      Regularity.RegularityReport
    simplePropertyViolations :
      List Regularity.SimplePropertyViolation

open RegularityEvidence public

record RegularityCheckMeaning
  (document : P.OntologyDocument)
  (evidence : RegularityEvidence document)
  : Type₀ where
  constructor regularityCheckMeaning
  field
    regularitySourcePreserved :
      sourceDocument evidence ≡ document
    regularityReportRecorded :
      regularityReport evidence ≡
      Regularity.reportRegularity document
    simplePropertyViolationsRecorded :
      simplePropertyViolations evidence ≡
      Regularity.regularityReportSimplePropertyViolations
        (regularityReport evidence)

open RegularityCheckMeaning public

RegularityCheckResult : Type₀
RegularityCheckResult =
  CheckResult
    P.OntologyDocument
    RegularityEvidence
    RegularityCheckMeaning

regularityDiagnosticNamespace : String
regularityDiagnosticNamespace =
  "owl2.portable.regularity"

nonCanonicalSimplePropertyUseCode compositeSimplePropertyUseCode
  compositeHierarchySimplePropertyUseCode :
  DiagnosticCode
nonCanonicalSimplePropertyUseCode =
  mkDiagnosticCode
    regularityDiagnosticNamespace
    "nonCanonicalSimplePropertyUse"
compositeSimplePropertyUseCode =
  mkDiagnosticCode
    regularityDiagnosticNamespace
    "compositeSimplePropertyUse"
compositeHierarchySimplePropertyUseCode =
  mkDiagnosticCode
    regularityDiagnosticNamespace
    "compositeHierarchySimplePropertyUse"

simplePropertyViolationKindDiagnosticCode :
  Regularity.SimplePropertyViolationKind →
  DiagnosticCode
simplePropertyViolationKindDiagnosticCode
  Regularity.nonCanonicalSimplePropertyUse =
  nonCanonicalSimplePropertyUseCode
simplePropertyViolationKindDiagnosticCode
  (Regularity.compositeSimplePropertyUse fact) =
  compositeSimplePropertyUseCode
simplePropertyViolationKindDiagnosticCode
  (Regularity.compositeHierarchySimplePropertyUse fact) =
  compositeHierarchySimplePropertyUseCode

simplePropertyViolationKindMessage :
  Regularity.SimplePropertyViolationKind →
  String
simplePropertyViolationKindMessage
  Regularity.nonCanonicalSimplePropertyUse =
  "simple-property position uses a non-canonical object-property expression"
simplePropertyViolationKindMessage
  (Regularity.compositeSimplePropertyUse fact) =
  "simple-property position uses a composite object property"
simplePropertyViolationKindMessage
  (Regularity.compositeHierarchySimplePropertyUse fact) =
  "simple-property position uses a property with a composite predecessor"

simplePropertyViolationDiagnostic :
  Regularity.SimplePropertyViolation →
  Diagnostic
simplePropertyViolationDiagnostic violation =
  diagnostic
    (simplePropertyViolationKindDiagnosticCode
      (Regularity.simplePropertyViolationKind violation))
    severityError
    rootSourcePath
    (simplePropertyViolationKindMessage
      (Regularity.simplePropertyViolationKind violation))

simplePropertyViolationDiagnostics :
  List Regularity.SimplePropertyViolation →
  Diagnostics
simplePropertyViolationDiagnostics [] =
  []
simplePropertyViolationDiagnostics (violation ∷ violations) =
  simplePropertyViolationDiagnostic violation
  ∷ simplePropertyViolationDiagnostics violations

regularityDiagnostics : P.OntologyDocument → Diagnostics
regularityDiagnostics document =
  simplePropertyViolationDiagnostics
    (Regularity.regularityReportSimplePropertyViolations
      (Regularity.reportRegularity document))

regularityEvidenceFor :
  (document : P.OntologyDocument) →
  RegularityEvidence document
regularityEvidenceFor document =
  regularityEvidence
    document
    refl
    (Regularity.reportRegularity document)
    (Regularity.regularityReportSimplePropertyViolations
      (Regularity.reportRegularity document))

regularityMeaningFor :
  (document : P.OntologyDocument) →
  (evidence : RegularityEvidence document) →
  sourceDocument evidence ≡ document →
  regularityReport evidence ≡
    Regularity.reportRegularity document →
  simplePropertyViolations evidence ≡
    Regularity.regularityReportSimplePropertyViolations
      (regularityReport evidence) →
  RegularityCheckMeaning document evidence
regularityMeaningFor document evidence preserved report violations =
  regularityCheckMeaning preserved report violations

checkRegularity : P.OntologyDocument → RegularityCheckResult
checkRegularity document =
  Core.successfulResultWithDiagnostics
    (regularityDiagnostics document)
    document
    evidence
    (regularityMeaningFor document evidence refl refl refl)
  where
  evidence : RegularityEvidence document
  evidence =
    regularityEvidenceFor document