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

module OWL2.Portable.DocumentPolicy where

open import Cubical.Data.Nat.Base using (zero; suc)
open import OWL2.Prelude
import OWL2.Portable.Syntax as P

private
  concatMap : ∀ {A B : Type₀} → (A → List B) → List A → List B
  concatMap f [] =
    []
  concatMap f (x ∷ xs) =
    f x ++ concatMap f xs

listCount : ∀ {ℓ} {A : Type ℓ} → List A → ℕ
listCount [] =
  zero
listCount (x ∷ xs) =
  suc (listCount xs)

data AnonymousIndividualUseKind : Type₀ where
  classExpressionIndividualUse :
    AnonymousIndividualUseKind
  sameIndividualUse :
    AnonymousIndividualUseKind
  differentIndividualsUse :
    AnonymousIndividualUseKind
  classAssertionSubjectUse :
    AnonymousIndividualUseKind
  objectPropertyAssertionSubjectUse :
    AnonymousIndividualUseKind
  objectPropertyAssertionObjectUse :
    AnonymousIndividualUseKind
  negativeObjectPropertyAssertionSubjectUse :
    AnonymousIndividualUseKind
  negativeObjectPropertyAssertionObjectUse :
    AnonymousIndividualUseKind
  dataPropertyAssertionSubjectUse :
    AnonymousIndividualUseKind
  negativeDataPropertyAssertionSubjectUse :
    AnonymousIndividualUseKind
  annotationSubjectUse :
    AnonymousIndividualUseKind
  annotationValueUse :
    AnonymousIndividualUseKind

data AnonymousIndividualUseSource : Type₀ where
  ontologyAnnotationSource :
    P.Annotation → AnonymousIndividualUseSource
  axiomAnnotationSource :
    P.Annotated P.Axiom → AnonymousIndividualUseSource
  axiomBodySource :
    P.Annotated P.Axiom → AnonymousIndividualUseSource

record AnonymousIndividualUse : Type₀ where
  constructor anonymousIndividualUse
  field
    anonymousIndividualUseSource :
      AnonymousIndividualUseSource
    anonymousIndividualUseKind :
      AnonymousIndividualUseKind
    anonymousIndividualID :
      P.BlankNodeID

open AnonymousIndividualUse public

anonymousIndividualUseAt :
  AnonymousIndividualUseSource →
  AnonymousIndividualUseKind →
  P.BlankNodeID →
  List AnonymousIndividualUse
anonymousIndividualUseAt source kind bnode =
  anonymousIndividualUse source kind bnode ∷ []

anonymousIndividualUsesInIndividual :
  AnonymousIndividualUseSource →
  AnonymousIndividualUseKind →
  P.Individual →
  List AnonymousIndividualUse
anonymousIndividualUsesInIndividual source kind (P.namedIndividual i) =
  []
anonymousIndividualUsesInIndividual
  source kind (P.anonymousIndividual bnode) =
  anonymousIndividualUseAt source kind bnode

anonymousIndividualUsesInIndividuals :
  AnonymousIndividualUseSource →
  AnonymousIndividualUseKind →
  List P.Individual →
  List AnonymousIndividualUse
anonymousIndividualUsesInIndividuals source kind [] =
  []
anonymousIndividualUsesInIndividuals source kind (individual ∷ individuals) =
  anonymousIndividualUsesInIndividual source kind individual
  ++ anonymousIndividualUsesInIndividuals source kind individuals

anonymousIndividualUsesInIndividualsOneOrMore :
  AnonymousIndividualUseSource →
  AnonymousIndividualUseKind →
  P.OneOrMore P.Individual →
  List AnonymousIndividualUse
anonymousIndividualUsesInIndividualsOneOrMore source kind individuals =
  anonymousIndividualUsesInIndividual source kind (P.head individuals)
  ++ anonymousIndividualUsesInIndividuals source kind (P.tail individuals)

anonymousIndividualUsesInIndividualsTwoOrMore :
  AnonymousIndividualUseSource →
  AnonymousIndividualUseKind →
  P.TwoOrMore P.Individual →
  List AnonymousIndividualUse
anonymousIndividualUsesInIndividualsTwoOrMore source kind individuals =
  anonymousIndividualUsesInIndividual source kind (P.first individuals)
  ++
  anonymousIndividualUsesInIndividual source kind (P.second individuals)
  ++
  anonymousIndividualUsesInIndividuals source kind (P.rest individuals)

mutual
  anonymousIndividualUsesInAnnotationSubject :
    AnonymousIndividualUseSource →
    P.AnnotationSubject →
    List AnonymousIndividualUse
  anonymousIndividualUsesInAnnotationSubject
    source
    (P.annotationSubjectIRI subjectIRI) =
    []
  anonymousIndividualUsesInAnnotationSubject
    source
    (P.annotationSubjectAnonymous bnode) =
    anonymousIndividualUseAt source annotationSubjectUse bnode

  anonymousIndividualUsesInAnnotationValue :
    AnonymousIndividualUseSource →
    P.AnnotationValue →
    List AnonymousIndividualUse
  anonymousIndividualUsesInAnnotationValue
    source
    (P.annotationValueIRI valueIRI) =
    []
  anonymousIndividualUsesInAnnotationValue
    source
    (P.annotationValueAnonymous bnode) =
    anonymousIndividualUseAt source annotationValueUse bnode
  anonymousIndividualUsesInAnnotationValue
    source
    (P.annotationValueLiteral literal) =
    []

  anonymousIndividualUsesInAnnotation :
    AnonymousIndividualUseSource →
    P.Annotation →
    List AnonymousIndividualUse
  anonymousIndividualUsesInAnnotation
    source
    (P.annotation annotations property value) =
    anonymousIndividualUsesInAnnotations source annotations
    ++ anonymousIndividualUsesInAnnotationValue source value

  anonymousIndividualUsesInAnnotations :
    AnonymousIndividualUseSource →
    List P.Annotation →
    List AnonymousIndividualUse
  anonymousIndividualUsesInAnnotations source [] =
    []
  anonymousIndividualUsesInAnnotations source (ann ∷ annotations) =
    anonymousIndividualUsesInAnnotation source ann
    ++ anonymousIndividualUsesInAnnotations source annotations

  anonymousIndividualUsesInClassExpression :
    AnonymousIndividualUseSource →
    P.ClassExpression →
    List AnonymousIndividualUse
  anonymousIndividualUsesInClassExpression source (P.namedClass c) =
    []
  anonymousIndividualUsesInClassExpression source P.owlThing =
    []
  anonymousIndividualUsesInClassExpression source P.owlNothing =
    []
  anonymousIndividualUsesInClassExpression
    source
    (P.objectIntersectionOf classes) =
    anonymousIndividualUsesInClassExpressionsTwoOrMore source classes
  anonymousIndividualUsesInClassExpression
    source
    (P.objectUnionOf classes) =
    anonymousIndividualUsesInClassExpressionsTwoOrMore source classes
  anonymousIndividualUsesInClassExpression
    source
    (P.objectComplementOf class) =
    anonymousIndividualUsesInClassExpression source class
  anonymousIndividualUsesInClassExpression
    source
    (P.objectOneOf individuals) =
    anonymousIndividualUsesInIndividualsOneOrMore
      source
      classExpressionIndividualUse
      individuals
  anonymousIndividualUsesInClassExpression
    source
    (P.objectSomeValuesFrom property class) =
    anonymousIndividualUsesInClassExpression source class
  anonymousIndividualUsesInClassExpression
    source
    (P.objectAllValuesFrom property class) =
    anonymousIndividualUsesInClassExpression source class
  anonymousIndividualUsesInClassExpression
    source
    (P.objectHasValue property individual) =
    anonymousIndividualUsesInIndividual
      source
      classExpressionIndividualUse
      individual
  anonymousIndividualUsesInClassExpression
    source
    (P.objectHasSelf property) =
    []
  anonymousIndividualUsesInClassExpression
    source
    (P.objectMinCardinality n property qualifier) =
    anonymousIndividualUsesInOptionalClassExpression source qualifier
  anonymousIndividualUsesInClassExpression
    source
    (P.objectMaxCardinality n property qualifier) =
    anonymousIndividualUsesInOptionalClassExpression source qualifier
  anonymousIndividualUsesInClassExpression
    source
    (P.objectExactCardinality n property qualifier) =
    anonymousIndividualUsesInOptionalClassExpression source qualifier
  anonymousIndividualUsesInClassExpression
    source
    (P.dataSomeValuesFrom property range) =
    []
  anonymousIndividualUsesInClassExpression
    source
    (P.dataAllValuesFrom property range) =
    []
  anonymousIndividualUsesInClassExpression
    source
    (P.dataHasValue property literal) =
    []
  anonymousIndividualUsesInClassExpression
    source
    (P.dataMinCardinality n property qualifier) =
    []
  anonymousIndividualUsesInClassExpression
    source
    (P.dataMaxCardinality n property qualifier) =
    []
  anonymousIndividualUsesInClassExpression
    source
    (P.dataExactCardinality n property qualifier) =
    []

  anonymousIndividualUsesInClassExpressions :
    AnonymousIndividualUseSource →
    List P.ClassExpression →
    List AnonymousIndividualUse
  anonymousIndividualUsesInClassExpressions source [] =
    []
  anonymousIndividualUsesInClassExpressions source (class ∷ classes) =
    anonymousIndividualUsesInClassExpression source class
    ++ anonymousIndividualUsesInClassExpressions source classes

  anonymousIndividualUsesInClassExpressionsTwoOrMore :
    AnonymousIndividualUseSource →
    P.TwoOrMore P.ClassExpression →
    List AnonymousIndividualUse
  anonymousIndividualUsesInClassExpressionsTwoOrMore source classes =
    anonymousIndividualUsesInClassExpression source (P.first classes)
    ++
    anonymousIndividualUsesInClassExpression source (P.second classes)
    ++
    anonymousIndividualUsesInClassExpressions source (P.rest classes)

  anonymousIndividualUsesInOptionalClassExpression :
    AnonymousIndividualUseSource →
    Optional P.ClassExpression →
    List AnonymousIndividualUse
  anonymousIndividualUsesInOptionalClassExpression source absent =
    []
  anonymousIndividualUsesInOptionalClassExpression source (present class) =
    anonymousIndividualUsesInClassExpression source class

anonymousIndividualUsesInAxiom :
  AnonymousIndividualUseSource →
  P.Axiom →
  List AnonymousIndividualUse
anonymousIndividualUsesInAxiom source (P.declaration entity) =
  []
anonymousIndividualUsesInAxiom source (P.subClassOf subclass superclass) =
  anonymousIndividualUsesInClassExpression source subclass
  ++ anonymousIndividualUsesInClassExpression source superclass
anonymousIndividualUsesInAxiom source (P.equivalentClasses classes) =
  anonymousIndividualUsesInClassExpressionsTwoOrMore source classes
anonymousIndividualUsesInAxiom source (P.disjointClasses classes) =
  anonymousIndividualUsesInClassExpressionsTwoOrMore source classes
anonymousIndividualUsesInAxiom source (P.disjointUnion class classes) =
  anonymousIndividualUsesInClassExpressionsTwoOrMore source classes
anonymousIndividualUsesInAxiom source (P.subObjectPropertyOf left right) =
  []
anonymousIndividualUsesInAxiom
  source
  (P.equivalentObjectProperties properties) =
  []
anonymousIndividualUsesInAxiom
  source
  (P.disjointObjectProperties properties) =
  []
anonymousIndividualUsesInAxiom
  source
  (P.inverseObjectProperties left right) =
  []
anonymousIndividualUsesInAxiom source (P.objectPropertyDomain property class) =
  anonymousIndividualUsesInClassExpression source class
anonymousIndividualUsesInAxiom source (P.objectPropertyRange property class) =
  anonymousIndividualUsesInClassExpression source class
anonymousIndividualUsesInAxiom source (P.functionalObjectProperty property) =
  []
anonymousIndividualUsesInAxiom
  source
  (P.inverseFunctionalObjectProperty property) =
  []
anonymousIndividualUsesInAxiom source (P.reflexiveObjectProperty property) =
  []
anonymousIndividualUsesInAxiom source (P.irreflexiveObjectProperty property) =
  []
anonymousIndividualUsesInAxiom source (P.symmetricObjectProperty property) =
  []
anonymousIndividualUsesInAxiom source (P.asymmetricObjectProperty property) =
  []
anonymousIndividualUsesInAxiom source (P.transitiveObjectProperty property) =
  []
anonymousIndividualUsesInAxiom source (P.subDataPropertyOf left right) =
  []
anonymousIndividualUsesInAxiom
  source
  (P.equivalentDataProperties properties) =
  []
anonymousIndividualUsesInAxiom
  source
  (P.disjointDataProperties properties) =
  []
anonymousIndividualUsesInAxiom source (P.dataPropertyDomain property class) =
  anonymousIndividualUsesInClassExpression source class
anonymousIndividualUsesInAxiom source (P.dataPropertyRange property range) =
  []
anonymousIndividualUsesInAxiom source (P.functionalDataProperty property) =
  []
anonymousIndividualUsesInAxiom source (P.datatypeDefinition datatype range) =
  []
anonymousIndividualUsesInAxiom source (P.hasKey class key) =
  anonymousIndividualUsesInClassExpression source class
anonymousIndividualUsesInAxiom source (P.sameIndividual individuals) =
  anonymousIndividualUsesInIndividualsTwoOrMore
    source
    sameIndividualUse
    individuals
anonymousIndividualUsesInAxiom source (P.differentIndividuals individuals) =
  anonymousIndividualUsesInIndividualsTwoOrMore
    source
    differentIndividualsUse
    individuals
anonymousIndividualUsesInAxiom source (P.classAssertion class individual) =
  anonymousIndividualUsesInClassExpression source class
  ++
  anonymousIndividualUsesInIndividual
    source
    classAssertionSubjectUse
    individual
anonymousIndividualUsesInAxiom
  source
  (P.objectPropertyAssertion property subject object) =
  anonymousIndividualUsesInIndividual
    source
    objectPropertyAssertionSubjectUse
    subject
  ++
  anonymousIndividualUsesInIndividual
    source
    objectPropertyAssertionObjectUse
    object
anonymousIndividualUsesInAxiom
  source
  (P.negativeObjectPropertyAssertion property subject object) =
  anonymousIndividualUsesInIndividual
    source
    negativeObjectPropertyAssertionSubjectUse
    subject
  ++
  anonymousIndividualUsesInIndividual
    source
    negativeObjectPropertyAssertionObjectUse
    object
anonymousIndividualUsesInAxiom
  source
  (P.dataPropertyAssertion property subject value) =
  anonymousIndividualUsesInIndividual
    source
    dataPropertyAssertionSubjectUse
    subject
anonymousIndividualUsesInAxiom
  source
  (P.negativeDataPropertyAssertion property subject value) =
  anonymousIndividualUsesInIndividual
    source
    negativeDataPropertyAssertionSubjectUse
    subject
anonymousIndividualUsesInAxiom
  source
  (P.annotationAssertion property subject value) =
  anonymousIndividualUsesInAnnotationSubject source subject
  ++ anonymousIndividualUsesInAnnotationValue source value
anonymousIndividualUsesInAxiom
  source
  (P.subAnnotationPropertyOf subproperty superproperty) =
  []
anonymousIndividualUsesInAxiom
  source
  (P.annotationPropertyDomain property domain) =
  []
anonymousIndividualUsesInAxiom
  source
  (P.annotationPropertyRange property range) =
  []

anonymousIndividualUsesInAnnotatedAxiom :
  P.Annotated P.Axiom →
  List AnonymousIndividualUse
anonymousIndividualUsesInAnnotatedAxiom axiom =
  anonymousIndividualUsesInAnnotations
    (axiomAnnotationSource axiom)
    (P.annotations axiom)
  ++
  anonymousIndividualUsesInAxiom
    (axiomBodySource axiom)
    (P.body axiom)

anonymousIndividualUsesInOntologyAnnotation :
  P.Annotation →
  List AnonymousIndividualUse
anonymousIndividualUsesInOntologyAnnotation ann =
  anonymousIndividualUsesInAnnotation
    (ontologyAnnotationSource ann)
    ann

anonymousIndividualUsesInOntology :
  P.Ontology →
  List AnonymousIndividualUse
anonymousIndividualUsesInOntology ont =
  concatMap
    anonymousIndividualUsesInOntologyAnnotation
    (P.annotations ont)
  ++ concatMap anonymousIndividualUsesInAnnotatedAxiom (P.axioms ont)

ontologyDocumentAnonymousIndividualUses :
  P.OntologyDocument →
  List AnonymousIndividualUse
ontologyDocumentAnonymousIndividualUses document =
  anonymousIndividualUsesInOntology (P.documentOntology document)

NoAnonymousIndividualUses :
  List AnonymousIndividualUse →
  Type₀
NoAnonymousIndividualUses [] =
  Unit*
NoAnonymousIndividualUses (_ ∷ _) =
  ⊥

NoAnonymousIndividuals : P.OntologyDocument → Type₀
NoAnonymousIndividuals document =
  NoAnonymousIndividualUses
    (ontologyDocumentAnonymousIndividualUses document)

record WebProtegeNamedIndividualPolicy
  (document : P.OntologyDocument) : Type₀ where
  constructor webProtegeNamedIndividualPolicy
  field
    webProtegeNoAnonymousIndividuals :
      NoAnonymousIndividuals document

open WebProtegeNamedIndividualPolicy public

record OntologyIDFact : Type₀ where
  constructor ontologyIDFact
  field
    ontologyIDFactIRI :
      Optional P.IRI
    ontologyIDFactVersionIRI :
      Optional P.IRI

open OntologyIDFact public

ontologyIDFactOfID : P.OntologyID → OntologyIDFact
ontologyIDFactOfID P.anonymousOntology =
  ontologyIDFact absent absent
ontologyIDFactOfID (P.ontologyIRI ontologyIRI versionIRI) =
  ontologyIDFact (present ontologyIRI) versionIRI

ontologyIDFactOfOntology : P.Ontology → OntologyIDFact
ontologyIDFactOfOntology ont =
  ontologyIDFactOfID (P.id ont)

ontologyIDFactOfDocument :
  P.OntologyDocument →
  OntologyIDFact
ontologyIDFactOfDocument document =
  ontologyIDFactOfOntology (P.documentOntology document)

record OntologyIDReport : Type₀ where
  constructor ontologyIDReport
  field
    ontologyIDReportDocument :
      P.OntologyDocument
    ontologyIDReportIRI :
      Optional P.IRI
    ontologyIDReportVersionIRI :
      Optional P.IRI

open OntologyIDReport public

reportOntologyID : P.OntologyDocument → OntologyIDReport
reportOntologyID document =
  ontologyIDReport
    document
    (ontologyIDFactIRI fact)
    (ontologyIDFactVersionIRI fact)
  where
  fact : OntologyIDFact
  fact =
    ontologyIDFactOfDocument document

OntologyIDMatches :
  P.OntologyDocument →
  Optional P.IRI →
  Optional P.IRI →
  Type₀
OntologyIDMatches document ontologyIRI versionIRI =
  (ontologyIDFactIRI (ontologyIDFactOfDocument document) ≡ ontologyIRI)
  ×
  (ontologyIDFactVersionIRI (ontologyIDFactOfDocument document) ≡ versionIRI)

HasOntologyIRIAndVersion :
  P.OntologyDocument →
  P.IRI →
  Optional P.IRI →
  Type₀
HasOntologyIRIAndVersion document ontologyIRI versionIRI =
  OntologyIDMatches document (present ontologyIRI) versionIRI

ReportStatesOntologyIRIAndVersion :
  OntologyIDReport →
  Optional P.IRI →
  Optional P.IRI →
  Type₀
ReportStatesOntologyIRIAndVersion report ontologyIRI versionIRI =
  (ontologyIDReportIRI report ≡ ontologyIRI)
  ×
  (ontologyIDReportVersionIRI report ≡ versionIRI)

record DocumentPolicyReport : Type₀ where
  constructor documentPolicyReport
  field
    documentPolicyReportDocument :
      P.OntologyDocument
    documentPolicyReportAnonymousIndividualUses :
      List AnonymousIndividualUse
    documentPolicyReportAnonymousIndividualUseCount :
      ℕ
    documentPolicyReportOntologyID :
      OntologyIDReport

open DocumentPolicyReport public

reportDocumentPolicy : P.OntologyDocument → DocumentPolicyReport
reportDocumentPolicy document =
  documentPolicyReport
    document
    uses
    (listCount uses)
    (reportOntologyID document)
  where
  uses : List AnonymousIndividualUse
  uses =
    ontologyDocumentAnonymousIndividualUses document

NoReportAnonymousIndividuals : DocumentPolicyReport → Type₀
NoReportAnonymousIndividuals report =
  NoAnonymousIndividualUses
    (documentPolicyReportAnonymousIndividualUses report)