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

module OWL2.Examples.WebProtege.Primer where

open import OWL2.Prelude
open import OWL2.Check.Result using (Clean)
import OWL2.Syntax as S
open S
open import OWL2.DirectSemantics
import OWL2.DirectSemantics.Expansions as Expansions
import OWL2.Examples.Cardinality as Cardinality
import OWL2.Examples.Family as Family
import OWL2.Examples.HasKey as HasKey
import OWL2.Examples.PropertyChain as PropertyChain
import OWL2.Examples.WebProtege.Annotations as A
import OWL2.Examples.WebProtege.CardinalityRestrictions
  as CardinalityRestrictions
import OWL2.Examples.WebProtege.Constructors as Constructors
import OWL2.Examples.WebProtege.KeyRestrictions as KeyRestrictions
import OWL2.Portable.CardinalityRestrictions as CR
import OWL2.Portable.Check.WebProtege as WebProtegeCheck
import OWL2.Portable.KeyRestrictions as KR
import OWL2.Portable.Semantics as PS
import OWL2.Portable.Syntax as P
import OWL2.Portable.WebProtegeReport as Report

record PrimerConstructorCoverage : Type₀ where
  constructor mkPrimerConstructorCoverage
  field
    negativeObjectPropertyAssertionSupported :
      SatisfiesAxiom Family.familyInterpretation
        (negativeObjectPropertyAssertion
          Family.HasWife
          Family.Bill
          Family.Mary)

    propertyChainSupported :
      SatisfiesAxiom PropertyChain.chainInterpretation
        (subObjectPropertyOf
          PropertyChain.ParentParentChain
          PropertyChain.HasGrandparent)

    propertyChainEntailsGrandparent :
      evalObjectProperty
        PropertyChain.chainInterpretation
        PropertyChain.HasGrandparent
        PropertyChain.aliceObject
        PropertyChain.carolObject

    hasKeySupported :
      SatisfiesAxiom HasKey.keyInterpretation
        (hasKey HasKey.PersonC HasKey.PersonSSNKey)

    keyIdentifiesAlias :
      ObjectEq
        HasKey.keyInterpretation
        (individualDenotation HasKey.keyInterpretation HasKey.Alice)
        (individualDenotation HasKey.keyInterpretation HasKey.AliceAlias)

    inverseObjectPropertiesSupported :
      SatisfiesAxiom Constructors.constructorInterpretation
        (Expansions.inverseObjectPropertiesExpansion
          Constructors.HasPart
          Constructors.PartOf)

    inverseObjectPropertiesEntailPartOf :
      evalObjectProperty
        Constructors.constructorInterpretation
        Constructors.PartOf
        Constructors.imageDatasetObject
        Constructors.textDatasetObject

    disjointUnionSupported :
      AllList
        (Expansions.disjointUnionExpansion
          Constructors.Dataset
          Constructors.TextDatasetC
          Constructors.ImageDatasetC
          [])
        (SatisfiesAxiom Constructors.constructorInterpretation)

    objectExactCardinalitySupported :
      SatisfiesAxiom Cardinality.cardinalityInterpretation
        (classAssertion
          Cardinality.ExactlyOneSpouse
          Cardinality.Alice)

    dataExactCardinalitySupported :
      SatisfiesAxiom Cardinality.cardinalityInterpretation
        (classAssertion
          Cardinality.ExactlyOneAge
          Cardinality.Alice)

    portableKeyRestrictionsAccepted :
      KR.NoKeyRestrictionViolations KeyRestrictions.acceptedKeyDocument

    portableCardinalityRestrictionsAccepted :
      CR.NoUnsafeCardinalityRestrictions
        CardinalityRestrictions.cardinalityDocument

primerConstructorCoverage : PrimerConstructorCoverage
primerConstructorCoverage =
  mkPrimerConstructorCoverage
    Family.billDoesNotHaveWifeMary
    PropertyChain.parentParentImpliesGrandparent
    PropertyChain.aliceHasGrandparentCarolByChain
    HasKey.personSSNKeySatisfied
    HasKey.aliceAliasSameByKey
    Constructors.inverseObjectPropertiesSatisfied
    Constructors.imagePartOfTextByInverseExpansion
    Constructors.disjointUnionExpansionSatisfied
    Cardinality.aliceHasExactlyOneSpouse
    Cardinality.aliceHasExactlyOneAge
    KeyRestrictions.acceptedKeyNoRestrictions
    CardinalityRestrictions.cardinalityDocumentAllSafe

primerPortableCardinalityRestrictionCount :
  CR.reportCardinalityRestrictionCount
    CardinalityRestrictions.cardinalityReport
    ≡ 
primerPortableCardinalityRestrictionCount =
  CardinalityRestrictions.cardinalityDocumentRestrictionCount

primerPortableKeyStructuralViolationCount :
  KR.keyRestrictionStructuralViolationCount
    KeyRestrictions.acceptedKeyReport
    ≡ 
primerPortableKeyStructuralViolationCount =
  KeyRestrictions.acceptedKeyStructuralViolationCount

primerPortableKeyDeclarationCoverageGapCount :
  KR.keyRestrictionDeclarationCoverageGapCount
    KeyRestrictions.acceptedKeyReport
    ≡ 
primerPortableKeyDeclarationCoverageGapCount =
  KeyRestrictions.acceptedKeyDeclarationCoverageGapCount

primerPortableKeyPropertyRoleConflictCount :
  KR.keyRestrictionPropertyRoleUsageConflictCount
    KeyRestrictions.acceptedKeyReport
    ≡ 
primerPortableKeyPropertyRoleConflictCount =
  KeyRestrictions.acceptedKeyPropertyRoleConflictCount

curatedByIRI : P.IRI
curatedByIRI =
  P.iri "https://example.org/webprotege#curatedBy"

curatedBy : P.ObjectPropertyName
curatedBy =
  P.named curatedByIRI

CuratedBy : P.ObjectPropertyExpression
CuratedBy =
  P.objectProperty curatedBy

reviewScoreLiteral : P.Literal
reviewScoreLiteral =
  P.typedLiteral "5" CardinalityRestrictions.xsdString

curatorCuratedByChain : P.ObjectPropertyChain
curatorCuratedByChain =
  P.objectPropertyChain
    (P.twoOrMore A.HasCurator CuratedBy [])

sourceObjectExactCardinality : P.ClassExpression
sourceObjectExactCardinality =
  P.objectExactCardinality
    
    A.HasCurator
    (present A.ContributorC)

sourceDataExactCardinality : P.ClassExpression
sourceDataExactCardinality =
  P.dataExactCardinality
    
    CardinalityRestrictions.ReviewScore
    (present CardinalityRestrictions.StringRange)

sourceDisjointUnionAxiom sourceInverseObjectPropertiesAxiom
  sourcePropertyChainAxiom sourceNegativeObjectPropertyAxiom
  sourceNegativeDataPropertyAxiom sourceHasKeyAxiom
  sourceObjectExactCardinalityAxiom sourceDataExactCardinalityAxiom :
  P.Axiom
sourceDisjointUnionAxiom =
  P.disjointUnion
    A.dataset
    (P.twoOrMore A.CuratedDatasetC A.ContributorC [])
sourceInverseObjectPropertiesAxiom =
  P.inverseObjectProperties A.HasCurator CuratedBy
sourcePropertyChainAxiom =
  P.subObjectPropertyOf
    (P.subObjectPropertyChain curatorCuratedByChain)
    A.HasCurator
sourceNegativeObjectPropertyAxiom =
  P.negativeObjectPropertyAssertion
    A.HasCurator
    A.draftDataset
    A.alice
sourceNegativeDataPropertyAxiom =
  P.negativeDataPropertyAssertion
    CardinalityRestrictions.ReviewScore
    A.draftDataset
    reviewScoreLiteral
sourceHasKeyAxiom =
  P.hasKey
    A.CuratedDatasetC
    (P.propertyKey
      (A.HasCurator ∷ [])
      (CardinalityRestrictions.ReviewScore ∷ []))
sourceObjectExactCardinalityAxiom =
  P.classAssertion sourceObjectExactCardinality A.datasetOne
sourceDataExactCardinalityAxiom =
  P.classAssertion sourceDataExactCardinality A.datasetOne

primerSourceDeclarationAxioms :
  List (P.Annotated P.Axiom)
primerSourceDeclarationAxioms =
  A.declarationAxioms
  ++ CardinalityRestrictions.localDeclarationAxioms
  ++ (A.axiom (P.declaration (P.objectPropertyEntity curatedBy)) ∷ [])

primerSourceConstructorAxioms :
  List (P.Annotated P.Axiom)
primerSourceConstructorAxioms =
  A.axiom sourceDisjointUnionAxiom
  ∷ A.axiom sourceInverseObjectPropertiesAxiom
  ∷ A.axiom sourcePropertyChainAxiom
  ∷ A.axiom sourceNegativeObjectPropertyAxiom
  ∷ A.axiom sourceNegativeDataPropertyAxiom
  ∷ A.axiom sourceHasKeyAxiom
  ∷ A.axiom sourceObjectExactCardinalityAxiom
  ∷ A.axiom sourceDataExactCardinalityAxiom
  ∷ []

primerSourceDocument : P.OntologyDocument
primerSourceDocument =
  P.ontologyDocument
    (A.webProtegePrefix ∷ [])
    (P.ontology
      (P.ontologyIRI A.webProtegeOntologyIRI absent)
      []
      []
      (primerSourceDeclarationAxioms ++ primerSourceConstructorAxioms))

primerSourceCheckResult : WebProtegeCheck.WebProtegeDocumentCheckResult
primerSourceCheckResult =
  WebProtegeCheck.checkWebProtegeDocument primerSourceDocument

primerSourceCheckClean : Clean primerSourceCheckResult
primerSourceCheckClean =
  tt

primerSourceReport : Report.DocumentReport
primerSourceReport =
  WebProtegeCheck.webProtegeReportFromClean
    primerSourceCheckResult
    primerSourceCheckClean

primerSourceCompleteWebProtegeDocument :
  Report.CompleteWebProtegeDocument primerSourceDocument
primerSourceCompleteWebProtegeDocument =
  WebProtegeCheck.completeWebProtegeDocumentFromClean
    primerSourceCheckResult
    primerSourceCheckClean

primerSourceCompleteSemanticTranslation :
  PS.CompleteSemanticTranslation primerSourceDocument
primerSourceCompleteSemanticTranslation =
  refl

primerSourceCardinalityReport :
  CR.CardinalityRestrictionsReport
primerSourceCardinalityReport =
  CR.reportCardinalityRestrictions primerSourceDocument

primerSourceCardinalityRestrictionCount :
  CR.reportCardinalityRestrictionCount
    primerSourceCardinalityReport
    ≡ 
primerSourceCardinalityRestrictionCount =
  refl

primerSourceUnsafeCardinalityIssueCount :
  CR.reportUnsafeCardinalityRestrictionIssueCount
    primerSourceCardinalityReport
    ≡ 
primerSourceUnsafeCardinalityIssueCount =
  refl

primerSourceCardinalitiesSafe :
  CR.NoUnsafeCardinalityRestrictions primerSourceDocument
primerSourceCardinalitiesSafe =
  tt*

primerSourceKeyReport :
  KR.KeyRestrictionsReport
primerSourceKeyReport =
  KR.reportKeyRestrictions primerSourceDocument

primerSourceKeyRestrictionsAccepted :
  KR.NoKeyRestrictionViolations primerSourceDocument
primerSourceKeyRestrictionsAccepted =
  KR.noKeyRestrictionViolations tt* tt* tt*

sourceDisjointUnionTranslationShape :
  PS.translateAxiom sourceDisjointUnionAxiom ≡
  present
    ( S.equivalentClasses
        ( S.namedClass A.dataset
        ∷ S.objectUnionOf
            (S.namedClass A.curatedDataset ∷
             S.namedClass A.contributor ∷ [])
        ∷ [] )
    ∷ S.disjointClasses
        (S.namedClass A.curatedDataset ∷
         S.namedClass A.contributor ∷ [])
    ∷ [] )
sourceDisjointUnionTranslationShape =
  refl

sourceInverseObjectPropertiesTranslationShape :
  PS.translateAxiom sourceInverseObjectPropertiesAxiom ≡
  present
    ( S.equivalentObjectProperties
        ( PS.translateObjectPropertyExpression A.HasCurator
        ∷ S.objectInverseOf
            (PS.translateObjectPropertyExpression CuratedBy)
        ∷ [] )
    ∷ [] )
sourceInverseObjectPropertiesTranslationShape =
  refl

sourcePropertyChainTranslationShape :
  PS.translateAxiom sourcePropertyChainAxiom ≡
  present
    ( S.subObjectPropertyOf
        (S.subObjectPropertyChain
          (PS.translateObjectPropertyExpression A.HasCurator)
          (PS.translateObjectPropertyExpression CuratedBy)
          [])
        (PS.translateObjectPropertyExpression A.HasCurator)
    ∷ [] )
sourcePropertyChainTranslationShape =
  refl

sourceNegativeObjectPropertyTranslationShape :
  PS.translateAxiom sourceNegativeObjectPropertyAxiom ≡
  present
    ( S.negativeObjectPropertyAssertion
        (PS.translateObjectPropertyExpression A.HasCurator)
        A.draftDataset
        A.alice
    ∷ [] )
sourceNegativeObjectPropertyTranslationShape =
  refl

sourceNegativeDataPropertyTranslationShape :
  PS.translateAxiom sourceNegativeDataPropertyAxiom ≡
  present
    ( S.negativeDataPropertyAssertion
        ( PS.translateDataPropertyExpression
          CardinalityRestrictions.ReviewScore )
        A.draftDataset
        reviewScoreLiteral
    ∷ [] )
sourceNegativeDataPropertyTranslationShape =
  refl

sourceHasKeyTranslationShape :
  PS.translateAxiom sourceHasKeyAxiom ≡
  present
    ( S.hasKey
        (S.namedClass A.curatedDataset)
        (S.propertyKey
          (PS.translateObjectPropertyExpression A.HasCurator ∷ [])
          ( PS.translateDataPropertyExpression
            CardinalityRestrictions.ReviewScore ∷ [] ))
    ∷ [] )
sourceHasKeyTranslationShape =
  refl

sourceObjectExactCardinalityTranslationShape :
  PS.translateAxiom sourceObjectExactCardinalityAxiom ≡
  present
    ( S.classAssertion
        (S.objectExactCardinality
          
          (PS.translateObjectPropertyExpression A.HasCurator)
          (present (S.namedClass A.contributor)))
        A.datasetOne
    ∷ [] )
sourceObjectExactCardinalityTranslationShape =
  refl

sourceDataExactCardinalityTranslationShape :
  PS.translateAxiom sourceDataExactCardinalityAxiom ≡
  present
    ( S.classAssertion
        (S.dataExactCardinality
          
          ( PS.translateDataPropertyExpression
            CardinalityRestrictions.ReviewScore )
          (present (S.datatype CardinalityRestrictions.xsdString)))
        A.datasetOne
    ∷ [] )
sourceDataExactCardinalityTranslationShape =
  refl