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

module OWL2.Portable.GlobalRestrictions where

open import OWL2.Prelude
import OWL2.Portable.AnnotationErasure as Erasure
import OWL2.Portable.Declarations as Decl
import OWL2.Portable.ObjectPropertyKeys as Keys
import OWL2.Portable.PropertyKinds as PK
import OWL2.Portable.Punning as Punning
import OWL2.Portable.Regularity as Reg
import OWL2.Portable.RegularityProof as RegProof
import OWL2.Portable.RegularityRank as Rank
import OWL2.Portable.Semantics as Sem
import OWL2.Portable.Syntax as P
import OWL2.Syntax.Regularity as SynReg

declarationCoverageGaps :
  P.OntologyDocument → List Decl.UndeclaredEntityUse
declarationCoverageGaps =
  Decl.ontologyDocumentUndeclaredEntityUses

declarationRoleCollisions :
  P.OntologyDocument → List PK.DeclarationCollision
declarationRoleCollisions =
  PK.owl2DLOntologyDocumentDeclarationCollisions

propertyRoleUsageConflicts :
  P.OntologyDocument → List PK.PropertyUsageConflict
propertyRoleUsageConflicts =
  PK.ontologyDocumentPropertyRoleUsageConflicts

semanticUnsupportedAxioms :
  P.OntologyDocument → List (P.Annotated P.Axiom)
semanticUnsupportedAxioms document =
  Sem.unsupported (Sem.partialTranslateOntologyDocument document)

regularitySimplePropertyViolations :
  P.OntologyDocument → List Reg.SimplePropertyViolation
regularitySimplePropertyViolations document =
  Reg.regularityReportSimplePropertyViolations (Reg.reportRegularity document)

regularityRankIssues :
  List Rank.PropertyRank →
  P.OntologyDocument →
  List Rank.PropertyChainRankIssue
regularityRankIssues ranks document =
  Rank.regularityRankReportPropertyChainIssues
    (Rank.reportRegularityRank ranks document)

NoDeclarationCoverageGaps : P.OntologyDocument → Type₀
NoDeclarationCoverageGaps document =
  Decl.NoUndeclaredEntityUses (declarationCoverageGaps document)

NoDeclarationRoleCollisions : P.OntologyDocument → Type₀
NoDeclarationRoleCollisions document =
  Punning.NoDisallowedOWL2DLDeclarationPunning document

NoPropertyRoleUsageConflicts : P.OntologyDocument → Type₀
NoPropertyRoleUsageConflicts document =
  PK.NoPropertyUsageConflicts (propertyRoleUsageConflicts document)

NoSemanticUnsupportedAxioms : P.OntologyDocument → Type₀
NoSemanticUnsupportedAxioms document =
  semanticUnsupportedAxioms document ≡ []

NoRegularitySimplePropertyViolations : P.OntologyDocument → Type₀
NoRegularitySimplePropertyViolations =
  Reg.PortableRegularityRestrictions

NoRegularityRankIssues :
  List Rank.PropertyRank → P.OntologyDocument → Type₀
NoRegularityRankIssues =
  Rank.PortableRegularityRankRestrictions

AnnotationErasureMatchesSemantics : P.OntologyDocument → Type₀
AnnotationErasureMatchesSemantics document =
  Erasure.eraseOntologyDocument document ≡
  Sem.semanticOntology (Sem.partialTranslateOntologyDocument document)

AnnotationErasureIgnoresAnnotations : P.OntologyDocument → Type₀
AnnotationErasureIgnoresAnnotations document =
  Erasure.eraseOntologyDocument document ≡
  Erasure.eraseOntologyDocument
    (Erasure.stripOntologyDocumentAnnotations document)

NoAnnotationErasureUnsupportedAxioms :
  P.OntologyDocument → Type₀
NoAnnotationErasureUnsupportedAxioms document =
  Erasure.unsupportedAxiomsOfOntologyDocument document ≡ []

annotationErasureMatchesSemanticsProof :
  (document : P.OntologyDocument) →
  AnnotationErasureMatchesSemantics document
annotationErasureMatchesSemanticsProof =
  Erasure.eraseOntologyDocumentMatchesSemantics

annotationErasureIgnoresAnnotationsProof :
  (document : P.OntologyDocument) →
  AnnotationErasureIgnoresAnnotations document
annotationErasureIgnoresAnnotationsProof =
  Erasure.semanticErasureIgnoresAnnotations

record OWL2DLImplementedGlobalRestrictions
  (document : P.OntologyDocument) : Type₀ where
  constructor owl2DLImplementedGlobalRestrictions
  field
    noDeclarationCoverageGaps :
      NoDeclarationCoverageGaps document
    noDeclarationRoleCollisions :
      NoDeclarationRoleCollisions document
    noPropertyRoleUsageConflicts :
      NoPropertyRoleUsageConflicts document
    noSemanticUnsupportedAxioms :
      NoSemanticUnsupportedAxioms document

open OWL2DLImplementedGlobalRestrictions public

record PortableRegularityPlaceholder
  (document : P.OntologyDocument) : Type₀ where
  constructor portableRegularityPlaceholder
  field
    regularityCheckerPending :
      Unit*

open PortableRegularityPlaceholder public

record PortableRegularityDiagnosticRestrictions
  (document : P.OntologyDocument) : Type₀ where
  constructor portableRegularityDiagnosticRestrictions
  field
    noRegularitySimplePropertyViolations :
      NoRegularitySimplePropertyViolations document

open PortableRegularityDiagnosticRestrictions public

record PortableRegularityRankDiagnosticRestrictions
  (ranks : List Rank.PropertyRank)
  (document : P.OntologyDocument) : Type₀ where
  constructor portableRegularityRankDiagnosticRestrictions
  field
    noRegularityRankIssues :
      NoRegularityRankIssues ranks document

open PortableRegularityRankDiagnosticRestrictions public

record PortableRegularityDiagnosticCoverage
  (ranks : List Rank.PropertyRank)
  (document : P.OntologyDocument) : Type₀ where
  constructor portableRegularityDiagnosticCoverage
  field
    regularitySimplePropertyDiagnosticRestrictions :
      PortableRegularityDiagnosticRestrictions document
    regularityRankDiagnosticRestrictions :
      PortableRegularityRankDiagnosticRestrictions ranks document
    proofBridgePending :
      PortableRegularityPlaceholder document

open PortableRegularityDiagnosticCoverage public

GeneratedHierarchyPathReachabilityWitness :
  P.OntologyDocument → Type₀
GeneratedHierarchyPathReachabilityWitness document =
  ∀ {start target} →
  SynReg.PropertyHierarchyPath
    (RegProof.generatedRegularityContext document)
    start
    target →
  Σ ℕ
    (λ fuel →
      Reg.propertyKeyReachableWithin
        fuel
        (Reg.regularityReportPropertyHierarchyFacts
          (Reg.reportRegularity document))
        (Keys.syntaxObjectPropertyBaseKey start)
        (Keys.syntaxObjectPropertyBaseKey target)
      ≡
      true)

record PortableRegularityProofBridgeCoverage
  (document : P.OntologyDocument) : Type₀ where
  constructor portableRegularityProofBridgeCoverage
  field
    proofBridgeSimplePropertyDiagnostics :
      PortableRegularityDiagnosticRestrictions document
    generatedHierarchyFactKeyCoherence :
      RegProof.PropertyHierarchyFactKeyCoherentResolver
        (Reg.regularityReportPropertyHierarchyFacts
          (Reg.reportRegularity document))
    generatedHierarchyPathReachability :
      GeneratedHierarchyPathReachabilityWitness document
    fullContextualRegularityPending :
      PortableRegularityPlaceholder document

open PortableRegularityProofBridgeCoverage public

record PortableProfilePlaceholder
  (document : P.OntologyDocument) : Type₀ where
  constructor portableProfilePlaceholder
  field
    profileCheckerPending :
      Unit*

open PortableProfilePlaceholder public

record OWL2DLGlobalRestrictionCoverage
  (document : P.OntologyDocument) : Type₀ where
  constructor owl2DLGlobalRestrictionCoverage
  field
    implementedGlobalRestrictions :
      OWL2DLImplementedGlobalRestrictions document
    regularityPlaceholder :
      PortableRegularityPlaceholder document
    profilePlaceholder :
      PortableProfilePlaceholder document

open OWL2DLGlobalRestrictionCoverage public

record WebProtegeImplementedGlobalRestrictions
  (document : P.OntologyDocument) : Type₀ where
  constructor webProtegeImplementedGlobalRestrictions
  field
    webProtegeOWL2DLRestrictions :
      OWL2DLImplementedGlobalRestrictions document
    webProtegeAnnotationErasureUnsupported :
      NoAnnotationErasureUnsupportedAxioms document
    webProtegeAnnotationErasureMatchesSemantics :
      AnnotationErasureMatchesSemantics document
    webProtegeAnnotationErasureIgnoresAnnotations :
      AnnotationErasureIgnoresAnnotations document

open WebProtegeImplementedGlobalRestrictions public

record WebProtegeGlobalRestrictionCoverage
  (document : P.OntologyDocument) : Type₀ where
  constructor webProtegeGlobalRestrictionCoverage
  field
    implementedWebProtegeRestrictions :
      WebProtegeImplementedGlobalRestrictions document
    regularityPlaceholder :
      PortableRegularityPlaceholder document
    profilePlaceholder :
      PortableProfilePlaceholder document

open WebProtegeGlobalRestrictionCoverage public

completeOWL2DLImplementedGlobalRestrictions :
  (document : P.OntologyDocument) →
  Decl.AllEntityUsesDeclared document →
  PK.OWL2DLDeclarationRolesConsistent document →
  PK.PropertyRoleUsageConsistent document →
  Sem.CompleteSemanticTranslation document →
  OWL2DLImplementedGlobalRestrictions document
completeOWL2DLImplementedGlobalRestrictions
  document
  declarations
  declarationRoles
  propertyRoles
  semantics =
  owl2DLImplementedGlobalRestrictions
    declarations
    declarationRoles
    propertyRoles
    semantics

defaultRegularityPlaceholder :
  (document : P.OntologyDocument) →
  PortableRegularityPlaceholder document
defaultRegularityPlaceholder document =
  portableRegularityPlaceholder tt*

completePortableRegularityDiagnosticRestrictions :
  (document : P.OntologyDocument) →
  Reg.PortableRegularityRestrictions document →
  PortableRegularityDiagnosticRestrictions document
completePortableRegularityDiagnosticRestrictions document restrictions =
  portableRegularityDiagnosticRestrictions restrictions

completePortableRegularityRankDiagnosticRestrictions :
  (ranks : List Rank.PropertyRank) →
  (document : P.OntologyDocument) →
  Rank.PortableRegularityRankRestrictions ranks document →
  PortableRegularityRankDiagnosticRestrictions ranks document
completePortableRegularityRankDiagnosticRestrictions ranks document restrictions =
  portableRegularityRankDiagnosticRestrictions restrictions

completePortableRegularityDiagnosticCoverage :
  (ranks : List Rank.PropertyRank) →
  (document : P.OntologyDocument) →
  Reg.PortableRegularityRestrictions document →
  Rank.PortableRegularityRankRestrictions ranks document →
  PortableRegularityDiagnosticCoverage ranks document
completePortableRegularityDiagnosticCoverage
  ranks
  document
  simpleRestrictions
  rankRestrictions =
  portableRegularityDiagnosticCoverage
    (completePortableRegularityDiagnosticRestrictions
      document
      simpleRestrictions)
    (completePortableRegularityRankDiagnosticRestrictions
      ranks
      document
      rankRestrictions)
    (defaultRegularityPlaceholder document)

completePortableRegularityProofBridgeCoverage :
  (document : P.OntologyDocument) →
  Reg.PortableRegularityRestrictions document →
  PortableRegularityProofBridgeCoverage document
completePortableRegularityProofBridgeCoverage document simpleRestrictions =
  portableRegularityProofBridgeCoverage
    (completePortableRegularityDiagnosticRestrictions
      document
      simpleRestrictions)
    (RegProof.ontologyDocumentPropertyHierarchyFactsKeyCoherent document)
    (λ path →
      RegProof.propertyKeyReachableWithinWitnessFromHierarchyPath
        (RegProof.ontologyDocumentPropertyHierarchyFactsKeyCoherent document)
        path)
    (defaultRegularityPlaceholder document)

defaultProfilePlaceholder :
  (document : P.OntologyDocument) →
  PortableProfilePlaceholder document
defaultProfilePlaceholder document =
  portableProfilePlaceholder tt*