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

module OWL2.Examples.GlobalRestrictions where

open import OWL2.Prelude
open import OWL2.Syntax
open import OWL2.Syntax.Declarations
open import OWL2.Syntax.WellFormed
open import OWL2.Syntax.Regularity
open import OWL2.Syntax.GlobalRestrictions
import OWL2.Examples.PropertyChain as Chain
import OWL2.Examples.Regularity as Reg

declaredChainAxioms : List (Axiom Chain.ChainSignature)
declaredChainAxioms =
  declaration (classEntity Chain.Person)
  ∷ declaration (objectPropertyEntity Chain.hasParent)
  ∷ declaration (objectPropertyEntity Chain.hasGrandparent)
  ∷ declaration (individualEntity Chain.Alice)
  ∷ declaration (individualEntity Chain.Bob)
  ∷ declaration (individualEntity Chain.Carol)
  ∷ subObjectPropertyOf Chain.ParentParentChain Chain.HasGrandparent
  ∷ objectPropertyAssertion Chain.HasParent Chain.Alice Chain.Bob
  ∷ objectPropertyAssertion Chain.HasParent Chain.Bob Chain.Carol
  ∷ objectPropertyAssertion Chain.HasGrandparent Chain.Alice Chain.Carol
  ∷ []

declaredChainOntology : Ontology Chain.ChainSignature
declaredChainOntology =
  ontology (Chain.chainDocument ∷ []) [] declaredChainAxioms

declaredChainEnvironment :
  DeclarationEnvironment Chain.ChainSignature
declaredChainEnvironment =
  ontologyDeclarationEnvironment declaredChainOntology

personDeclared :
  EntityDeclared declaredChainEnvironment (classEntity Chain.Person)
personDeclared =
  declaredAtHead

parentDeclared :
  EntityDeclared
    declaredChainEnvironment
    (objectPropertyEntity Chain.hasParent)
parentDeclared =
  declaredLater declaredAtHead

grandparentDeclared :
  EntityDeclared
    declaredChainEnvironment
    (objectPropertyEntity Chain.hasGrandparent)
grandparentDeclared =
  declaredLater (declaredLater declaredAtHead)

aliceDeclared :
  EntityDeclared declaredChainEnvironment (individualEntity Chain.Alice)
aliceDeclared =
  declaredLater (declaredLater (declaredLater declaredAtHead))

bobDeclared :
  EntityDeclared declaredChainEnvironment (individualEntity Chain.Bob)
bobDeclared =
  declaredLater
    (declaredLater
      (declaredLater
        (declaredLater declaredAtHead)))

carolDeclared :
  EntityDeclared declaredChainEnvironment (individualEntity Chain.Carol)
carolDeclared =
  declaredLater
    (declaredLater
      (declaredLater
        (declaredLater
          (declaredLater declaredAtHead))))

declaredChainOntologyWellFormed :
  OntologyWellFormed declaredChainEnvironment declaredChainOntology
declaredChainOntologyWellFormed =
  tt* ,
  tt* ,
  tt* ,
  tt* ,
  tt* ,
  tt* ,
  ((parentDeclared , (parentDeclared , tt*)) , grandparentDeclared) ,
  (parentDeclared , (aliceDeclared , bobDeclared)) ,
  (parentDeclared , (bobDeclared , carolDeclared)) ,
  (grandparentDeclared , (aliceDeclared , carolDeclared)) ,
  tt*

declaredChainAxiomsUseOnlySimpleProperties :
  AxiomsUseOnlySimpleObjectProperties
    Reg.chainRegularityContext
    declaredChainAxioms
declaredChainAxiomsUseOnlySimpleProperties =
  tt* ,
  tt* ,
  tt* ,
  tt* ,
  tt* ,
  tt* ,
  tt* ,
  tt* ,
  tt* ,
  tt* ,
  tt*

declaredChainAxiomsRegular :
  AxiomsPropertyChainsRegular Reg.ChainOrder declaredChainAxioms
declaredChainAxiomsRegular =
  tt* ,
  tt* ,
  tt* ,
  tt* ,
  tt* ,
  tt* ,
  Reg.strictChainRegular ,
  tt* ,
  tt* ,
  tt* ,
  tt*

declaredChainStrictOrder :
  StrictChainOrder Chain.ChainSignature declaredChainAxioms
declaredChainStrictOrder ._<_ =
  Reg.ChainOrder
declaredChainStrictOrder .irrefl =
  Reg.chainOrderIrrefl
declaredChainStrictOrder .trans =
  Reg.chainOrderTrans
declaredChainStrictOrder .inversePreserves =
  Reg.chainOrderInversePreserves
declaredChainStrictOrder .chainsRegular =
  declaredChainAxiomsRegular

declaredChainHierarchyCompatibleOrder :
  HierarchyCompatibleChainOrder
    Chain.ChainSignature
    Reg.chainRegularityContext
    declaredChainAxioms
declaredChainHierarchyCompatibleOrder .strictChainOrder =
  declaredChainStrictOrder
declaredChainHierarchyCompatibleOrder .noBackHierarchy =
  Reg.chainOrderNoBackHierarchy

declaredChainContextualRegular :
  ContextualOntologyRegular
    Reg.chainRegularityContext
    declaredChainOntology
declaredChainContextualRegular .simpleObjectPropertyUses =
  declaredChainAxiomsUseOnlySimpleProperties
declaredChainContextualRegular .hierarchyCompatibleChainOrder =
  declaredChainHierarchyCompatibleOrder

declaredChainGlobalRestrictions :
  OntologyGlobalRestrictions
    declaredChainEnvironment
    Reg.chainRegularityContext
    declaredChainOntology
declaredChainGlobalRestrictions .wellFormed =
  declaredChainOntologyWellFormed
declaredChainGlobalRestrictions .contextualRegularity =
  declaredChainContextualRegular

declaredChainSelfContainedGlobalRestrictions :
  OntologySelfContainedGlobalRestrictions
    Reg.chainRegularityContext
    declaredChainOntology
declaredChainSelfContainedGlobalRestrictions =
  ontologyGlobalRestrictionsSelfContained declaredChainGlobalRestrictions

nonSimpleCardinalityOntology : Ontology Chain.ChainSignature
nonSimpleCardinalityOntology =
  ontology
    []
    []
    (subClassOf Chain.PersonC Reg.AtLeastOneGrandparent ∷ [])

nonSimpleCardinalityGlobalRestrictionsRejected :
  ¬ OntologyGlobalRestrictions
      fullDeclarationEnvironment
      Reg.chainRegularityContext
      nonSimpleCardinalityOntology
nonSimpleCardinalityGlobalRestrictionsRejected restrictions =
  Reg.atLeastOneGrandparentRejected
    (snd
      (fst
        (ContextualOntologyRegular.simpleObjectPropertyUses
          (ontologyGlobalRestrictionsRegular restrictions))))