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

module OWL2.Examples.WebProtege.DocumentPolicy where

open import OWL2.Prelude
import OWL2.Portable.DocumentPolicy as Policy
import OWL2.Portable.Syntax as P

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

className : String → P.ClassName
className =
  name

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

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

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

documentIRI datasetIRI datasetOneIRI : P.IRI
documentIRI =
  P.iri "https://example.org/webprotege/document-policy"
datasetIRI =
  P.iri "https://example.org/webprotege/document-policy#Dataset"
datasetOneIRI =
  P.iri "https://example.org/webprotege/document-policy#dataset-one"

dataset : P.ClassName
dataset =
  P.named datasetIRI

DatasetC : P.ClassExpression
DatasetC =
  P.namedClass dataset

datasetOne : P.Individual
datasetOne =
  P.namedIndividual datasetOneIRI

namedIndividualDocument : P.OntologyDocument
namedIndividualDocument =
  document
    (P.ontologyIRI documentIRI absent)
    ( axiom (P.declaration (P.classEntity dataset))
    ∷ axiom (P.declaration (P.namedIndividualEntity datasetOneIRI))
    ∷ axiom (P.classAssertion DatasetC datasetOne)
    ∷ [] )

namedIndividualDocumentReport : Policy.DocumentPolicyReport
namedIndividualDocumentReport =
  Policy.reportDocumentPolicy namedIndividualDocument

namedIndividualDocumentAnonymousIndividualUseCount :
  Policy.documentPolicyReportAnonymousIndividualUseCount
    namedIndividualDocumentReport
  ≡ 0
namedIndividualDocumentAnonymousIndividualUseCount =
  refl

namedIndividualDocumentAccepted :
  Policy.NoAnonymousIndividuals namedIndividualDocument
namedIndividualDocumentAccepted =
  tt*

namedIndividualDocumentPolicy :
  Policy.WebProtegeNamedIndividualPolicy namedIndividualDocument
namedIndividualDocumentPolicy =
  Policy.webProtegeNamedIndividualPolicy
    namedIndividualDocumentAccepted

anonymousBlankNode : P.BlankNodeID
anonymousBlankNode =
  P.blankNodeID "anonymous-dataset"

anonymousIndividual : P.Individual
anonymousIndividual =
  P.anonymousIndividual anonymousBlankNode

anonymousIndividualDocument : P.OntologyDocument
anonymousIndividualDocument =
  document
    (P.ontologyIRI documentIRI absent)
    ( axiom (P.classAssertion DatasetC anonymousIndividual)
    ∷ [] )

anonymousIndividualDocumentReport : Policy.DocumentPolicyReport
anonymousIndividualDocumentReport =
  Policy.reportDocumentPolicy anonymousIndividualDocument

anonymousIndividualDocumentAnonymousIndividualUseCount :
  Policy.documentPolicyReportAnonymousIndividualUseCount
    anonymousIndividualDocumentReport
  ≡ 1
anonymousIndividualDocumentAnonymousIndividualUseCount =
  refl

anonymousIndividualDocumentUsesClassAssertionSubject :
  Policy.ontologyDocumentAnonymousIndividualUses anonymousIndividualDocument
  ≡
  Policy.anonymousIndividualUse
    (Policy.axiomBodySource
      (axiom (P.classAssertion DatasetC anonymousIndividual)))
    Policy.classAssertionSubjectUse
    anonymousBlankNode
  ∷ []
anonymousIndividualDocumentUsesClassAssertionSubject =
  refl

anonymousIndividualDocumentRejected :
  ¬ Policy.NoAnonymousIndividuals anonymousIndividualDocument
anonymousIndividualDocumentRejected impossible =
  impossible

versionedDocumentIRI versionIRI : P.IRI
versionedDocumentIRI =
  P.iri "https://example.org/webprotege/document-policy/versioned"
versionIRI =
  P.iri "https://example.org/webprotege/document-policy/versioned/1"

versionedDocument : P.OntologyDocument
versionedDocument =
  document
    (P.ontologyIRI versionedDocumentIRI (present versionIRI))
    []

versionedOntologyIDReport : Policy.OntologyIDReport
versionedOntologyIDReport =
  Policy.reportOntologyID versionedDocument

versionedDocumentHasOntologyID :
  Policy.HasOntologyIRIAndVersion
    versionedDocument
    versionedDocumentIRI
    (present versionIRI)
versionedDocumentHasOntologyID =
  refl , refl

versionedReportStatesOntologyID :
  Policy.ReportStatesOntologyIRIAndVersion
    versionedOntologyIDReport
    (present versionedDocumentIRI)
    (present versionIRI)
versionedReportStatesOntologyID =
  refl , refl