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

module OWL2.Portable.AnnotationErasure where

open import OWL2.Prelude
import OWL2.DirectSemantics as D
import OWL2.Portable.Semantics as Sem
import OWL2.Portable.Syntax as P
import OWL2.Syntax as S

data SemanticAxiom : P.Axiom → Type₀ where
  semanticDeclaration :
    ∀ {e} → SemanticAxiom (P.declaration e)

  semanticSubClassOf :
    ∀ {c d} → SemanticAxiom (P.subClassOf c d)
  semanticEquivalentClasses :
    ∀ {cs} → SemanticAxiom (P.equivalentClasses cs)
  semanticDisjointClasses :
    ∀ {cs} → SemanticAxiom (P.disjointClasses cs)
  semanticDisjointUnion :
    ∀ {c cs} → SemanticAxiom (P.disjointUnion c cs)

  semanticSubObjectPropertyOf :
    ∀ {p q} → SemanticAxiom (P.subObjectPropertyOf p q)
  semanticEquivalentObjectProperties :
    ∀ {ps} → SemanticAxiom (P.equivalentObjectProperties ps)
  semanticDisjointObjectProperties :
    ∀ {ps} → SemanticAxiom (P.disjointObjectProperties ps)
  semanticInverseObjectProperties :
    ∀ {p q} → SemanticAxiom (P.inverseObjectProperties p q)
  semanticObjectPropertyDomain :
    ∀ {p c} → SemanticAxiom (P.objectPropertyDomain p c)
  semanticObjectPropertyRange :
    ∀ {p c} → SemanticAxiom (P.objectPropertyRange p c)
  semanticFunctionalObjectProperty :
    ∀ {p} → SemanticAxiom (P.functionalObjectProperty p)
  semanticInverseFunctionalObjectProperty :
    ∀ {p} → SemanticAxiom (P.inverseFunctionalObjectProperty p)
  semanticReflexiveObjectProperty :
    ∀ {p} → SemanticAxiom (P.reflexiveObjectProperty p)
  semanticIrreflexiveObjectProperty :
    ∀ {p} → SemanticAxiom (P.irreflexiveObjectProperty p)
  semanticSymmetricObjectProperty :
    ∀ {p} → SemanticAxiom (P.symmetricObjectProperty p)
  semanticAsymmetricObjectProperty :
    ∀ {p} → SemanticAxiom (P.asymmetricObjectProperty p)
  semanticTransitiveObjectProperty :
    ∀ {p} → SemanticAxiom (P.transitiveObjectProperty p)

  semanticSubDataPropertyOf :
    ∀ {p q} → SemanticAxiom (P.subDataPropertyOf p q)
  semanticEquivalentDataProperties :
    ∀ {ps} → SemanticAxiom (P.equivalentDataProperties ps)
  semanticDisjointDataProperties :
    ∀ {ps} → SemanticAxiom (P.disjointDataProperties ps)
  semanticDataPropertyDomain :
    ∀ {p c} → SemanticAxiom (P.dataPropertyDomain p c)
  semanticDataPropertyRange :
    ∀ {p d} → SemanticAxiom (P.dataPropertyRange p d)
  semanticFunctionalDataProperty :
    ∀ {p} → SemanticAxiom (P.functionalDataProperty p)

  semanticDatatypeDefinition :
    ∀ {d r} → SemanticAxiom (P.datatypeDefinition d r)
  semanticHasKey :
    ∀ {c k} → SemanticAxiom (P.hasKey c k)

  semanticSameIndividual :
    ∀ {xs} → SemanticAxiom (P.sameIndividual xs)
  semanticDifferentIndividuals :
    ∀ {xs} → SemanticAxiom (P.differentIndividuals xs)
  semanticClassAssertion :
    ∀ {c x} → SemanticAxiom (P.classAssertion c x)
  semanticObjectPropertyAssertion :
    ∀ {p x y} → SemanticAxiom (P.objectPropertyAssertion p x y)
  semanticNegativeObjectPropertyAssertion :
    ∀ {p x y} → SemanticAxiom (P.negativeObjectPropertyAssertion p x y)
  semanticDataPropertyAssertion :
    ∀ {p x lit} → SemanticAxiom (P.dataPropertyAssertion p x lit)
  semanticNegativeDataPropertyAssertion :
    ∀ {p x lit} → SemanticAxiom (P.negativeDataPropertyAssertion p x lit)

data AnnotationAxiom : P.Axiom → Type₀ where
  erasedAnnotationAssertion :
    ∀ {p s v} → AnnotationAxiom (P.annotationAssertion p s v)
  erasedSubAnnotationPropertyOf :
    ∀ {p q} → AnnotationAxiom (P.subAnnotationPropertyOf p q)
  erasedAnnotationPropertyDomain :
    ∀ {p i} → AnnotationAxiom (P.annotationPropertyDomain p i)
  erasedAnnotationPropertyRange :
    ∀ {p i} → AnnotationAxiom (P.annotationPropertyRange p i)

record SemanticAxiomTranslation (ax : P.Axiom) : Type₀ where
  constructor semanticAxiomTranslation
  field
    semanticWitness :
      SemanticAxiom ax
    translatedAxioms :
      List (S.Axiom Sem.PortableSignature)
    translationProof :
      Sem.translateAxiom ax ≡ present translatedAxioms

open SemanticAxiomTranslation public

translateSemanticAxiom :
  ∀ {ax} →
  SemanticAxiom ax →
  Optional (List (S.Axiom Sem.PortableSignature))
translateSemanticAxiom {ax = ax} semantic =
  Sem.translateAxiom ax

annotationAxiomErasedBySemantics :
  ∀ {ax} →
  AnnotationAxiom ax →
  Sem.translateAxiom ax ≡ present []
annotationAxiomErasedBySemantics erasedAnnotationAssertion =
  refl
annotationAxiomErasedBySemantics erasedSubAnnotationPropertyOf =
  refl
annotationAxiomErasedBySemantics erasedAnnotationPropertyDomain =
  refl
annotationAxiomErasedBySemantics erasedAnnotationPropertyRange =
  refl

record AnnotationAxiomErasure (ax : P.Axiom) : Type₀ where
  constructor annotationAxiomErasure
  field
    annotationWitness :
      AnnotationAxiom ax
    erasedProof :
      Sem.translateAxiom ax ≡ present []

open AnnotationAxiomErasure public

eraseAnnotationAxiom :
  ∀ {ax} →
  AnnotationAxiom ax →
  AnnotationAxiomErasure ax
eraseAnnotationAxiom annotation =
  annotationAxiomErasure annotation
    (annotationAxiomErasedBySemantics annotation)

data AxiomErasure : Type₀ where
  translatesToSemanticAxioms :
    List (S.Axiom Sem.PortableSignature) → AxiomErasure
  semanticallyErasedAnnotationAxiom :
    AxiomErasure
  unsupportedByPortableSemantics :
    AxiomErasure

eraseAxiom : P.Axiom → AxiomErasure
eraseAxiom (P.annotationAssertion p s v) =
  semanticallyErasedAnnotationAxiom
eraseAxiom (P.subAnnotationPropertyOf p q) =
  semanticallyErasedAnnotationAxiom
eraseAxiom (P.annotationPropertyDomain p i) =
  semanticallyErasedAnnotationAxiom
eraseAxiom (P.annotationPropertyRange p i) =
  semanticallyErasedAnnotationAxiom
eraseAxiom ax with Sem.translateAxiom ax
... | present axioms =
  translatesToSemanticAxioms axioms
... | absent =
  unsupportedByPortableSemantics

semanticAxiomsFromErasure :
  AxiomErasure → List (S.Axiom Sem.PortableSignature)
semanticAxiomsFromErasure (translatesToSemanticAxioms axioms) =
  axioms
semanticAxiomsFromErasure semanticallyErasedAnnotationAxiom =
  []
semanticAxiomsFromErasure unsupportedByPortableSemantics =
  []

semanticAxiomsOfAxiom :
  P.Axiom → List (S.Axiom Sem.PortableSignature)
semanticAxiomsOfAxiom ax with Sem.translateAxiom ax
... | present axioms =
  axioms
... | absent =
  []

stripAxiomAnnotations : P.Annotated P.Axiom → P.Annotated P.Axiom
stripAxiomAnnotations ax =
  P.annotated [] (P.body ax)

stripAxiomAnnotationsList :
  List (P.Annotated P.Axiom) → List (P.Annotated P.Axiom)
stripAxiomAnnotationsList =
  map stripAxiomAnnotations

eraseAnnotatedAxiom : P.Annotated P.Axiom → AxiomErasure
eraseAnnotatedAxiom ax =
  eraseAxiom (P.body ax)

semanticAxiomsOfAnnotatedAxiom :
  P.Annotated P.Axiom → List (S.Axiom Sem.PortableSignature)
semanticAxiomsOfAnnotatedAxiom ax =
  semanticAxiomsOfAxiom (P.body ax)

semanticAxiomsOfAnnotatedAxiomMatchesSemantics :
  (ax : P.Annotated P.Axiom) →
  semanticAxiomsOfAnnotatedAxiom ax ≡
  Sem.semanticAxioms (Sem.translateAnnotatedAxiom ax)
semanticAxiomsOfAnnotatedAxiomMatchesSemantics (P.annotated annotations body)
  with Sem.translateAxiom body
... | present axioms =
  refl
... | absent =
  refl

eraseAnnotatedAxioms :
  List (P.Annotated P.Axiom) → List (S.Axiom Sem.PortableSignature)
eraseAnnotatedAxioms [] =
  []
eraseAnnotatedAxioms (ax ∷ axioms) =
  semanticAxiomsOfAnnotatedAxiom ax ++ eraseAnnotatedAxioms axioms

eraseAnnotatedAxiomsMatchesSemantics :
  (axioms : List (P.Annotated P.Axiom)) →
  eraseAnnotatedAxioms axioms ≡
  Sem.semanticAxioms (Sem.translateAnnotatedAxioms axioms)
eraseAnnotatedAxiomsMatchesSemantics [] =
  refl
eraseAnnotatedAxiomsMatchesSemantics (P.annotated annotations body ∷ axioms)
  with Sem.translateAxiom body | eraseAnnotatedAxiomsMatchesSemantics axioms
... | present translated | tailProof =
  cong (λ tail → translated ++ tail) tailProof
... | absent | tailProof =
  tailProof

eraseOntology : P.Ontology → S.Ontology Sem.PortableSignature
eraseOntology ont =
  S.ontology
    (Sem.ontologyIdIRIs (P.id ont))
    (P.imports ont)
    (eraseAnnotatedAxioms (P.axioms ont))

eraseOntologyMatchesSemantics :
  (ontology : P.Ontology) →
  eraseOntology ontology ≡
  Sem.semanticOntology (Sem.partialTranslateOntology ontology)
eraseOntologyMatchesSemantics
  (P.ontology id imports annotations axioms) =
  cong
    (λ semanticAxioms →
      S.ontology (Sem.ontologyIdIRIs id) imports semanticAxioms)
    (eraseAnnotatedAxiomsMatchesSemantics axioms)

eraseOntologyDocument :
  P.OntologyDocument → S.Ontology Sem.PortableSignature
eraseOntologyDocument document =
  eraseOntology (P.documentOntology document)

eraseOntologyDocumentMatchesSemantics :
  (document : P.OntologyDocument) →
  eraseOntologyDocument document ≡
  Sem.semanticOntology (Sem.partialTranslateOntologyDocument document)
eraseOntologyDocumentMatchesSemantics
  (P.ontologyDocument prefixes ont) =
  eraseOntologyMatchesSemantics ont

unsupportedAxiomsOfAnnotatedAxiom :
  P.Annotated P.Axiom → List (P.Annotated P.Axiom)
unsupportedAxiomsOfAnnotatedAxiom ax =
  Sem.unsupportedAxioms (Sem.translateAnnotatedAxiom ax)

unsupportedAxiomsOfOntology :
  P.Ontology → List (P.Annotated P.Axiom)
unsupportedAxiomsOfOntology ont =
  Sem.unsupported (Sem.partialTranslateOntology ont)

unsupportedAxiomsOfOntologyDocument :
  P.OntologyDocument → List (P.Annotated P.Axiom)
unsupportedAxiomsOfOntologyDocument document =
  Sem.unsupported (Sem.partialTranslateOntologyDocument document)

stripOntologyAnnotations : P.Ontology → P.Ontology
stripOntologyAnnotations ont =
  P.ontology
    (P.id ont)
    (P.imports ont)
    []
    (stripAxiomAnnotationsList (P.axioms ont))

stripOntologyDocumentAnnotations :
  P.OntologyDocument → P.OntologyDocument
stripOntologyDocumentAnnotations document =
  P.ontologyDocument
    (P.prefixes document)
    (stripOntologyAnnotations (P.documentOntology document))

semanticAxiomsIgnoreAxiomAnnotations :
  (axioms : List (P.Annotated P.Axiom)) →
  eraseAnnotatedAxioms axioms ≡
  eraseAnnotatedAxioms (stripAxiomAnnotationsList axioms)
semanticAxiomsIgnoreAxiomAnnotations [] =
  refl
semanticAxiomsIgnoreAxiomAnnotations (P.annotated annotations body ∷ axioms) =
  cong
    (λ tail → semanticAxiomsOfAxiom body ++ tail)
    (semanticAxiomsIgnoreAxiomAnnotations axioms)

semanticErasureIgnoresAnnotations :
  (document : P.OntologyDocument) →
  eraseOntologyDocument document ≡
  eraseOntologyDocument (stripOntologyDocumentAnnotations document)
semanticErasureIgnoresAnnotations
  (P.ontologyDocument prefixes (P.ontology id imports annotations axioms)) =
  cong
    (λ semanticAxioms →
      S.ontology (Sem.ontologyIdIRIs id) imports semanticAxioms)
    (semanticAxiomsIgnoreAxiomAnnotations axioms)

SatisfiesErasedOntologyDocument :
  ∀ {ℓObj ℓData ℓSem} →
  D.Interpretation Sem.PortableSignature ℓObj ℓData ℓSem →
  P.OntologyDocument →
  Type (D.SemLevel ℓ-zero ℓObj ℓData ℓSem)
SatisfiesErasedOntologyDocument I document =
  D.SatisfiesOntology I (eraseOntologyDocument document)

satisfiesErasedToPortableSemantics :
  ∀ {ℓObj ℓData ℓSem}
    (I : D.Interpretation Sem.PortableSignature ℓObj ℓData ℓSem)
    (document : P.OntologyDocument) →
  SatisfiesErasedOntologyDocument I document →
  Sem.PartialSatisfiesOntologyDocument I document
satisfiesErasedToPortableSemantics I document =
  subst (D.SatisfiesOntology I)
    (eraseOntologyDocumentMatchesSemantics document)

satisfiesPortableSemanticsToErased :
  ∀ {ℓObj ℓData ℓSem}
    (I : D.Interpretation Sem.PortableSignature ℓObj ℓData ℓSem)
    (document : P.OntologyDocument) →
  Sem.PartialSatisfiesOntologyDocument I document →
  SatisfiesErasedOntologyDocument I document
satisfiesPortableSemanticsToErased I document =
  subst (D.SatisfiesOntology I)
    (sym (eraseOntologyDocumentMatchesSemantics document))

satisfiesAfterAnnotationStripping :
  ∀ {ℓObj ℓData ℓSem}
    (I : D.Interpretation Sem.PortableSignature ℓObj ℓData ℓSem)
    (document : P.OntologyDocument) →
  SatisfiesErasedOntologyDocument I document →
  SatisfiesErasedOntologyDocument I
    (stripOntologyDocumentAnnotations document)
satisfiesAfterAnnotationStripping I document =
  subst (D.SatisfiesOntology I)
    (semanticErasureIgnoresAnnotations document)

satisfiesBeforeAnnotationStripping :
  ∀ {ℓObj ℓData ℓSem}
    (I : D.Interpretation Sem.PortableSignature ℓObj ℓData ℓSem)
    (document : P.OntologyDocument) →
  SatisfiesErasedOntologyDocument I
    (stripOntologyDocumentAnnotations document) →
  SatisfiesErasedOntologyDocument I document
satisfiesBeforeAnnotationStripping I document =
  subst (D.SatisfiesOntology I)
    (sym (semanticErasureIgnoresAnnotations document))