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

module OWL2.Portable.Punning where

open import OWL2.Prelude
import OWL2.Portable.PropertyKinds as PK
import OWL2.Portable.Syntax as P

DeclarationPunningCollision : Type₀
DeclarationPunningCollision =
  PK.DeclarationCollision

owl2DLDeclarationPunningCollisions :
  P.OntologyDocument → List DeclarationPunningCollision
owl2DLDeclarationPunningCollisions =
  PK.owl2DLOntologyDocumentDeclarationCollisions

strictDeclarationPunningCollisions :
  P.OntologyDocument → List DeclarationPunningCollision
strictDeclarationPunningCollisions =
  PK.strictOntologyDocumentDeclarationPunningCollisions

NoDisallowedOWL2DLDeclarationPunning :
  P.OntologyDocument → Type₀
NoDisallowedOWL2DLDeclarationPunning document =
  PK.NoCollisions (owl2DLDeclarationPunningCollisions document)

NoStrictDeclarationPunning :
  P.OntologyDocument → Type₀
NoStrictDeclarationPunning document =
  PK.NoCollisions (strictDeclarationPunningCollisions document)

OWL2DLPunningConsistent : P.OntologyDocument → Type₀
OWL2DLPunningConsistent =
  NoDisallowedOWL2DLDeclarationPunning

StrictPunningConsistent : P.OntologyDocument → Type₀
StrictPunningConsistent =
  NoStrictDeclarationPunning

record OWL2DLPunningPolicy
  (document : P.OntologyDocument) : Type₀ where
  constructor owl2DLPunningPolicy
  field
    noDisallowedOWL2DLDeclarationPunning :
      NoDisallowedOWL2DLDeclarationPunning document

open OWL2DLPunningPolicy public

record StrictPunningPolicy
  (document : P.OntologyDocument) : Type₀ where
  constructor strictPunningPolicy
  field
    noStrictDeclarationPunning :
      NoStrictDeclarationPunning document

open StrictPunningPolicy public

owl2DLPunningPolicyFromPropertyKinds :
  (document : P.OntologyDocument) →
  PK.OWL2DLDeclarationRolesConsistent document →
  OWL2DLPunningPolicy document
owl2DLPunningPolicyFromPropertyKinds document consistent =
  owl2DLPunningPolicy consistent

strictPunningPolicyFromPropertyKinds :
  (document : P.OntologyDocument) →
  PK.StrictDeclarationRolesConsistent document →
  StrictPunningPolicy document
strictPunningPolicyFromPropertyKinds document consistent =
  strictPunningPolicy consistent