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

module OWL2.Examples.WebProtege.GlobalRestrictions where

open import OWL2.Prelude
import OWL2.Examples.WebProtege.Annotations as Annotations
import OWL2.Examples.WebProtege.DL as DL
import OWL2.Examples.Portable.Regularity as PortableRegularity
import OWL2.Examples.Portable.RegularityRank as PortableRegularityRank
import OWL2.Portable.GlobalRestrictions as GR

annotatedDocumentOWL2DLImplemented :
  GR.OWL2DLImplementedGlobalRestrictions Annotations.annotatedDocument
annotatedDocumentOWL2DLImplemented =
  GR.owl2DLImplementedGlobalRestrictions tt* tt* tt* refl

annotatedDocumentWebProtegeImplemented :
  GR.WebProtegeImplementedGlobalRestrictions Annotations.annotatedDocument
annotatedDocumentWebProtegeImplemented =
  GR.webProtegeImplementedGlobalRestrictions
    annotatedDocumentOWL2DLImplemented
    refl
    (GR.annotationErasureMatchesSemanticsProof
      Annotations.annotatedDocument)
    (GR.annotationErasureIgnoresAnnotationsProof
      Annotations.annotatedDocument)

annotatedDocumentCoverage :
  GR.WebProtegeGlobalRestrictionCoverage Annotations.annotatedDocument
annotatedDocumentCoverage =
  GR.webProtegeGlobalRestrictionCoverage
    annotatedDocumentWebProtegeImplemented
    (GR.defaultRegularityPlaceholder Annotations.annotatedDocument)
    (GR.defaultProfilePlaceholder Annotations.annotatedDocument)

annotatedDocumentRegularityDiagnostics :
  GR.PortableRegularityDiagnosticCoverage [] Annotations.annotatedDocument
annotatedDocumentRegularityDiagnostics =
  GR.completePortableRegularityDiagnosticCoverage
    []
    Annotations.annotatedDocument
    tt*
    tt*

annotatedDocumentRegularityProofBridgeCoverage :
  GR.PortableRegularityProofBridgeCoverage Annotations.annotatedDocument
annotatedDocumentRegularityProofBridgeCoverage =
  GR.completePortableRegularityProofBridgeCoverage
    Annotations.annotatedDocument
    tt*

missingDeclarationRejected :
  ¬ GR.NoDeclarationCoverageGaps DL.missingDeclarationDocument
missingDeclarationRejected impossible =
  impossible

propertyUsageCollisionRejected :
  ¬ GR.NoPropertyRoleUsageConflicts DL.propertyUsageCollisionDocument
propertyUsageCollisionRejected impossible =
  impossible

chainRegularityRejected :
  ¬ GR.NoRegularitySimplePropertyViolations
      PortableRegularity.chainDocument
chainRegularityRejected impossible =
  impossible

chainHierarchyRegularityRejected :
  ¬ GR.NoRegularitySimplePropertyViolations
      PortableRegularity.chainHierarchyDocument
chainHierarchyRegularityRejected impossible =
  impossible

missingRankRejected :
  ¬ GR.NoRegularityRankIssues
      PortableRegularityRank.missingSuperRankRanks
      PortableRegularityRank.strictChainDocument
missingRankRejected impossible =
  impossible