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

module OWL2.Examples.WebProtege.Annotations where

open import OWL2.Prelude
open import OWL2.Portable.Declarations using (AllEntityUsesDeclared)
import OWL2.Portable.Semantics as PS
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

individualName : String → P.NamedIndividualName
individualName =
  P.iri

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

webProtegeOntologyIRI : P.IRI
webProtegeOntologyIRI =
  P.iri "https://example.org/webprotege"

webResourceIRI datasetIRI curatedDatasetIRI contributorIRI : P.IRI
webResourceIRI =
  P.iri "https://example.org/webprotege#WebResource"
datasetIRI =
  P.iri "https://example.org/webprotege#Dataset"
curatedDatasetIRI =
  P.iri "https://example.org/webprotege#CuratedDataset"
contributorIRI =
  P.iri "https://example.org/webprotege#Contributor"

hasCuratorIRI datasetOneIRI draftDatasetIRI aliceIRI : P.IRI
hasCuratorIRI =
  P.iri "https://example.org/webprotege#hasCurator"
datasetOneIRI =
  P.iri "https://example.org/webprotege#dataset-one"
draftDatasetIRI =
  P.iri "https://example.org/webprotege#draft-dataset"
aliceIRI =
  P.iri "https://example.org/webprotege#alice"

webResource dataset curatedDataset contributor : P.ClassName
webResource =
  P.named webResourceIRI
dataset =
  P.named datasetIRI
curatedDataset =
  P.named curatedDatasetIRI
contributor =
  P.named contributorIRI

hasCurator : P.ObjectPropertyName
hasCurator =
  P.named hasCuratorIRI

datasetOne draftDataset alice : P.Individual
datasetOne =
  P.namedIndividual datasetOneIRI
draftDataset =
  P.namedIndividual draftDatasetIRI
alice =
  P.namedIndividual aliceIRI

label definition synonym xref comment editorNote curationStatus :
  P.AnnotationPropertyName
label =
  annotationPropertyName "http://www.w3.org/2000/01/rdf-schema#label"
definition =
  annotationPropertyName "http://purl.obolibrary.org/obo/IAO_0000115"
synonym =
  annotationPropertyName
    "http://www.geneontology.org/formats/oboInOwl#hasExactSynonym"
xref =
  annotationPropertyName
    "http://www.geneontology.org/formats/oboInOwl#hasDbXref"
comment =
  annotationPropertyName "http://www.w3.org/2000/01/rdf-schema#comment"
editorNote =
  annotationPropertyName "http://purl.obolibrary.org/obo/IAO_0000116"
curationStatus =
  annotationPropertyName "https://example.org/webprotege#curationStatus"

WebResourceC DatasetC CuratedDatasetC ContributorC : P.ClassExpression
WebResourceC =
  P.namedClass webResource
DatasetC =
  P.namedClass dataset
CuratedDatasetC =
  P.namedClass curatedDataset
ContributorC =
  P.namedClass contributor

HasCurator : P.ObjectPropertyExpression
HasCurator =
  P.objectProperty hasCurator

CuratedByContributorC : P.ClassExpression
CuratedByContributorC =
  P.objectSomeValuesFrom HasCurator ContributorC

stringAnnotation :
  P.AnnotationPropertyName → String → P.Annotation
stringAnnotation property text =
  P.annotation
    []
    property
    (P.annotationValueLiteral (P.stringLiteral text))

labelAnnotation definitionAnnotation synonymAnnotation xrefAnnotation
  commentAnnotation editorNoteAnnotation :
  String → P.Annotation
labelAnnotation =
  stringAnnotation label
definitionAnnotation =
  stringAnnotation definition
synonymAnnotation =
  stringAnnotation synonym
xrefAnnotation =
  stringAnnotation xref
commentAnnotation =
  stringAnnotation comment
editorNoteAnnotation =
  stringAnnotation editorNote

reviewedAnnotation : P.Annotation
reviewedAnnotation =
  stringAnnotation curationStatus "reviewed"

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

annotatedAxiom : List P.Annotation → P.Axiom → P.Annotated P.Axiom
annotatedAxiom annotations body =
  P.annotated annotations body

declarationAxioms : List (P.Annotated P.Axiom)
declarationAxioms =
  axiom (P.declaration (P.classEntity webResource))
  ∷ axiom (P.declaration (P.classEntity dataset))
  ∷ axiom (P.declaration (P.classEntity curatedDataset))
  ∷ axiom (P.declaration (P.classEntity contributor))
  ∷ axiom (P.declaration (P.objectPropertyEntity hasCurator))
  ∷ axiom (P.declaration (P.namedIndividualEntity datasetOneIRI))
  ∷ axiom (P.declaration (P.namedIndividualEntity draftDatasetIRI))
  ∷ axiom (P.declaration (P.namedIndividualEntity aliceIRI))
  ∷ axiom (P.declaration (P.annotationPropertyEntity label))
  ∷ axiom (P.declaration (P.annotationPropertyEntity definition))
  ∷ axiom (P.declaration (P.annotationPropertyEntity synonym))
  ∷ axiom (P.declaration (P.annotationPropertyEntity xref))
  ∷ axiom (P.declaration (P.annotationPropertyEntity comment))
  ∷ axiom (P.declaration (P.annotationPropertyEntity editorNote))
  ∷ axiom (P.declaration (P.annotationPropertyEntity curationStatus))
  ∷ []

logicalAxioms : List (P.Annotated P.Axiom)
logicalAxioms =
  annotatedAxiom
    ( labelAnnotation "Curated dataset is a dataset" ∷
      reviewedAnnotation ∷ [] )
    (P.subClassOf CuratedDatasetC DatasetC)
  ∷ annotatedAxiom
      ( definitionAnnotation
          "Every curated dataset has a contributor recorded as curator."
      ∷ synonymAnnotation "curated data collection"
      ∷ xrefAnnotation "WP:CURATED_DATASET"
      ∷ editorNoteAnnotation "Mirrors a WebProtege class description." ∷ [] )
      (P.subClassOf CuratedDatasetC CuratedByContributorC)
  ∷ annotatedAxiom
      ( commentAnnotation "Datasets are modelled as web resources." ∷ [] )
      (P.subClassOf DatasetC WebResourceC)
  ∷ axiom (P.classAssertion CuratedDatasetC datasetOne)
  ∷ axiom (P.classAssertion DatasetC draftDataset)
  ∷ axiom (P.classAssertion ContributorC alice)
  ∷ axiom (P.objectPropertyAssertion HasCurator datasetOne alice)
  ∷ []

annotationAssertionAxioms : List (P.Annotated P.Axiom)
annotationAssertionAxioms =
  axiom
    (P.annotationAssertion
      label
      (P.annotationSubjectIRI curatedDatasetIRI)
      (P.annotationValueLiteral (P.stringLiteral "curated dataset")))
  ∷ axiom
      (P.annotationAssertion
        definition
        (P.annotationSubjectIRI curatedDatasetIRI)
        (P.annotationValueLiteral
          (P.stringLiteral "A dataset with explicit curator metadata.")))
  ∷ axiom
      (P.annotationAssertion
        editorNote
        (P.annotationSubjectIRI datasetOneIRI)
        (P.annotationValueLiteral
          (P.stringLiteral "Seeded from a WebProtege-like editing session.")))
  ∷ axiom
      (P.annotationAssertion
        synonym
        (P.annotationSubjectIRI curatedDatasetIRI)
        (P.annotationValueLiteral (P.stringLiteral "reviewed dataset")))
  ∷ axiom
      (P.annotationAssertion
        xref
        (P.annotationSubjectIRI curatedDatasetIRI)
        (P.annotationValueLiteral (P.stringLiteral "WP:0001")))
  ∷ axiom
      (P.annotationAssertion
        comment
        (P.annotationSubjectIRI curatedDatasetIRI)
        (P.annotationValueLiteral
          (P.stringLiteral "Comment text is editorial metadata.")))
  ∷ []

ontologyAnnotations : List P.Annotation
ontologyAnnotations =
  labelAnnotation "WebProtege scaffold"
  ∷ definitionAnnotation
      "A tiny annotation-heavy ontology document for checked examples."
  ∷ synonymAnnotation "WP annotation scaffold"
  ∷ xrefAnnotation "WP:ANNOTATIONS"
  ∷ commentAnnotation "Ontology comments are preserved but semantically erased."
  ∷ reviewedAnnotation
  ∷ []

plainAxioms annotatedAxioms : List (P.Annotated P.Axiom)
plainAxioms =
  declarationAxioms ++ logicalAxioms
annotatedAxioms =
  plainAxioms ++ annotationAssertionAxioms

plainOntology annotatedOntology : P.Ontology
plainOntology =
  P.ontology
    (P.ontologyIRI webProtegeOntologyIRI absent)
    []
    []
    plainAxioms
annotatedOntology =
  P.ontology
    (P.ontologyIRI webProtegeOntologyIRI absent)
    []
    ontologyAnnotations
    annotatedAxioms

webProtegePrefix : P.PrefixDeclaration
webProtegePrefix =
  P.prefix
    (P.prefixName "webprotege")
    (P.iri "https://example.org/webprotege#")

plainDocument annotatedDocument : P.OntologyDocument
plainDocument =
  P.ontologyDocument (webProtegePrefix ∷ []) plainOntology
annotatedDocument =
  P.ontologyDocument (webProtegePrefix ∷ []) annotatedOntology

plainDocumentCovered : AllEntityUsesDeclared plainDocument
plainDocumentCovered =
  tt*

annotatedDocumentCovered : AllEntityUsesDeclared annotatedDocument
annotatedDocumentCovered =
  tt*

annotatedDocumentComplete : PS.CompleteSemanticTranslation annotatedDocument
annotatedDocumentComplete =
  refl

annotatedErasesLikePlain :
  PS.semanticOntology (PS.partialTranslateOntologyDocument annotatedDocument) ≡
  PS.semanticOntology (PS.partialTranslateOntologyDocument plainDocument)
annotatedErasesLikePlain =
  refl

annotationAssertionsErase :
  PS.semanticAxioms
    (PS.translateAnnotatedAxioms annotationAssertionAxioms)
  ≡ []
annotationAssertionsErase =
  refl

webProtegeMetadataAnnotationsEraseLikePlain :
  PS.semanticOntology (PS.partialTranslateOntology annotatedOntology) ≡
  PS.semanticOntology (PS.partialTranslateOntology plainOntology)
webProtegeMetadataAnnotationsEraseLikePlain =
  refl

webProtegeMetadataDocumentErasesLikePlain :
  PS.semanticOntology (PS.partialTranslateOntologyDocument annotatedDocument) ≡
  PS.semanticOntology (PS.partialTranslateOntologyDocument plainDocument)
webProtegeMetadataDocumentErasesLikePlain =
  refl