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

module OWL2.Examples.Portable.Declarations where

open import OWL2.Prelude
import OWL2.Check.Result as CheckResult
import OWL2.Portable.Check.Declarations as CheckDeclarations
open import OWL2.Portable.Declarations
import OWL2.Portable.PropertyKinds as PK
import OWL2.Portable.Syntax as P

name : String → P.Name
name text =
  P.named (P.iri text)

className : String → P.ClassName
className =
  name

objectPropertyName : String → P.ObjectPropertyName
objectPropertyName =
  name

dataPropertyName : String → P.DataPropertyName
dataPropertyName =
  name

datatypeName : String → P.DatatypeName
datatypeName =
  name

annotationPropertyName : String → P.AnnotationPropertyName
annotationPropertyName =
  P.iri

axiom : P.Axiom → P.Annotated P.Axiom
axiom body =
  P.annotated [] body

document : List (P.Annotated P.Axiom) → P.OntologyDocument
document axioms =
  P.ontologyDocument [] (P.ontology P.anonymousOntology [] [] axioms)

person employee : P.ClassName
person =
  className "https://example.org/portable#Person"
employee =
  className "https://example.org/portable#Employee"

hasManager : P.ObjectPropertyName
hasManager =
  objectPropertyName "https://example.org/portable#hasManager"

employeeId : P.DataPropertyName
employeeId =
  dataPropertyName "https://example.org/portable#employeeId"

stringDatatype : P.DatatypeName
stringDatatype =
  datatypeName "http://www.w3.org/2001/XMLSchema#string"

alice bob : P.NamedIndividualName
alice =
  P.iri "https://example.org/portable#Alice"
bob =
  P.iri "https://example.org/portable#Bob"

label : P.AnnotationPropertyName
label =
  annotationPropertyName "http://www.w3.org/2000/01/rdf-schema#label"

declaredAxioms : List (P.Annotated P.Axiom)
declaredAxioms =
  axiom (P.declaration (P.classEntity person))
  ∷ axiom (P.declaration (P.classEntity employee))
  ∷ axiom (P.declaration (P.objectPropertyEntity hasManager))
  ∷ axiom (P.declaration (P.dataPropertyEntity employeeId))
  ∷ axiom (P.declaration (P.datatypeEntity stringDatatype))
  ∷ axiom (P.declaration (P.namedIndividualEntity alice))
  ∷ axiom (P.declaration (P.namedIndividualEntity bob))
  ∷ axiom (P.declaration (P.annotationPropertyEntity label))
  ∷ axiom
      (P.subClassOf
        (P.namedClass employee)
        (P.objectSomeValuesFrom
          (P.objectProperty hasManager)
          (P.namedClass person)))
  ∷ axiom
      (P.dataPropertyAssertion
        (P.dataProperty employeeId)
        (P.namedIndividual alice)
        (P.typedLiteral "E-1" stringDatatype))
  ∷ axiom
      (P.objectPropertyAssertion
        (P.objectProperty hasManager)
        (P.namedIndividual alice)
        (P.namedIndividual bob))
  ∷ axiom
      (P.annotationAssertion
        label
        (P.annotationSubjectIRI alice)
        (P.annotationValueLiteral (P.stringLiteral "Alice")))
  ∷ []

declaredDocument : P.OntologyDocument
declaredDocument =
  document declaredAxioms

declaredDocumentCovered : AllEntityUsesDeclared declaredDocument
declaredDocumentCovered =
  tt*

declaredDocumentCheckResult :
  CheckDeclarations.DeclarationCheckResult
declaredDocumentCheckResult =
  CheckDeclarations.checkDeclarations declaredDocument

declaredDocumentCheckDiagnostics :
  CheckResult.diagnostics declaredDocumentCheckResult ≡ []
declaredDocumentCheckDiagnostics =
  refl

declaredDocumentCheckClean :
  CheckResult.clean? declaredDocumentCheckResult ≡ true
declaredDocumentCheckClean =
  refl

declarationOnlyDocument : P.OntologyDocument
declarationOnlyDocument =
  document (axiom (P.declaration (P.classEntity person)) ∷ [])

declarationOnlyDocumentCovered : AllEntityUsesDeclared declarationOnlyDocument
declarationOnlyDocumentCovered =
  tt*

undeclaredClassDocument : P.OntologyDocument
undeclaredClassDocument =
  document
    ( axiom
        (P.subClassOf
          (P.namedClass employee)
          (P.namedClass person))
    ∷ [] )

undeclaredClassRejected :
  ¬ AllEntityUsesDeclared undeclaredClassDocument
undeclaredClassRejected impossible =
  impossible

undeclaredClassCheckResult :
  CheckDeclarations.DeclarationCheckResult
undeclaredClassCheckResult =
  CheckDeclarations.checkDeclarations undeclaredClassDocument

undeclaredClassCheckDiagnostics :
  CheckResult.diagnostics undeclaredClassCheckResult ≡
  CheckDeclarations.undeclaredEntityUseDiagnostic
    (undeclaredEntityUse
      "https://example.org/portable#Employee"
      PK.classRole
      (axiomSource
        (axiom
          (P.subClassOf
            (P.namedClass employee)
            (P.namedClass person)))))
  ∷
  CheckDeclarations.undeclaredEntityUseDiagnostic
    (undeclaredEntityUse
      "https://example.org/portable#Person"
      PK.classRole
      (axiomSource
        (axiom
          (P.subClassOf
            (P.namedClass employee)
            (P.namedClass person)))))
  ∷ []
undeclaredClassCheckDiagnostics =
  refl

undeclaredClassCheckUnclean :
  CheckResult.clean? undeclaredClassCheckResult ≡ false
undeclaredClassCheckUnclean =
  refl

undeclaredClassCheckEvidenceUnavailable :
  CheckResult.evidence? undeclaredClassCheckResult ≡ absent
undeclaredClassCheckEvidenceUnavailable =
  refl

annotatedDeclarationDocument : P.OntologyDocument
annotatedDeclarationDocument =
  document
    ( P.annotated
        (P.annotation
          []
          label
          (P.annotationValueLiteral (P.stringLiteral "Person"))
        ∷ [])
        (P.declaration (P.classEntity person))
    ∷ [] )

annotatedDeclarationRejected :
  ¬ AllEntityUsesDeclared annotatedDeclarationDocument
annotatedDeclarationRejected impossible =
  impossible