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

module OWL2.Portable.Semantics where

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

PortableSignature : S.Signature ℓ-zero
PortableSignature =
  record
    { IRI = P.IRI
    ; ClassName = P.ClassName
    ; ObjectPropertyName = P.ObjectPropertyName
    ; DataPropertyName = P.DataPropertyName
    ; DatatypeName = P.DatatypeName
    ; IndividualName = P.Individual
    ; Literal = P.Literal
    ; FacetName = P.FacetName
    ; AnnotationPropertyName = P.AnnotationPropertyName
    }

oneOrMoreToList : ∀ {ℓ} {A : Type ℓ} → P.OneOrMore A → List A
oneOrMoreToList xs =
  P.head xs ∷ P.tail xs

twoOrMoreToList : ∀ {ℓ} {A : Type ℓ} → P.TwoOrMore A → List A
twoOrMoreToList xs =
  P.first xs ∷ P.second xs ∷ P.rest xs

optionalMap :
  ∀ {ℓA ℓB} {A : Type ℓA} {B : Type ℓB} →
  (A → B) → Optional A → Optional B
optionalMap f absent =
  absent
optionalMap f (present x) =
  present (f x)

optionalBind :
  ∀ {ℓA ℓB} {A : Type ℓA} {B : Type ℓB} →
  Optional A → (A → Optional B) → Optional B
optionalBind absent f =
  absent
optionalBind (present x) f =
  f x

translateList :
  ∀ {ℓA ℓB} {A : Type ℓA} {B : Type ℓB} →
  (A → Optional B) → List A → Optional (List B)
translateList f [] =
  present []
translateList f (x ∷ xs) with f x | translateList f xs
... | present y | present ys =
  present (y ∷ ys)
... | absent | _ =
  absent
... | _ | absent =
  absent

translateReservedIRI : P.ReservedIRI → S.IRI PortableSignature
translateReservedIRI P.owlThingIRI =
  P.iri "http://www.w3.org/2002/07/owl#Thing"
translateReservedIRI P.owlNothingIRI =
  P.iri "http://www.w3.org/2002/07/owl#Nothing"
translateReservedIRI P.owlTopObjectPropertyIRI =
  P.iri "http://www.w3.org/2002/07/owl#topObjectProperty"
translateReservedIRI P.owlBottomObjectPropertyIRI =
  P.iri "http://www.w3.org/2002/07/owl#bottomObjectProperty"
translateReservedIRI P.owlTopDataPropertyIRI =
  P.iri "http://www.w3.org/2002/07/owl#topDataProperty"
translateReservedIRI P.owlBottomDataPropertyIRI =
  P.iri "http://www.w3.org/2002/07/owl#bottomDataProperty"
translateReservedIRI P.rdfPlainLiteralIRI =
  P.iri "http://www.w3.org/1999/02/22-rdf-syntax-ns#PlainLiteral"
translateReservedIRI P.rdfsLiteralIRI =
  P.iri "http://www.w3.org/2000/01/rdf-schema#Literal"
translateReservedIRI P.xsdStringIRI =
  P.iri "http://www.w3.org/2001/XMLSchema#string"

translateNameIRI : P.Name → S.IRI PortableSignature
translateNameIRI (P.named i) =
  i
translateNameIRI (P.reserved r) =
  translateReservedIRI r

translateObjectPropertyExpression :
  P.ObjectPropertyExpression → S.ObjectPropertyExpression PortableSignature
translateObjectPropertyExpression (P.objectProperty p) =
  S.objectProperty p
translateObjectPropertyExpression P.topObjectProperty =
  S.topObjectProperty
translateObjectPropertyExpression P.bottomObjectProperty =
  S.bottomObjectProperty
translateObjectPropertyExpression (P.objectInverseOf p) =
  S.objectInverseOf (translateObjectPropertyExpression p)

translateDataPropertyExpression :
  P.DataPropertyExpression → S.DataPropertyExpression PortableSignature
translateDataPropertyExpression (P.dataProperty p) =
  S.dataProperty p
translateDataPropertyExpression P.topDataProperty =
  S.topDataProperty
translateDataPropertyExpression P.bottomDataProperty =
  S.bottomDataProperty

translateFacetRestriction :
  P.FacetRestriction → S.FacetRestriction PortableSignature
translateFacetRestriction restriction =
  S.facetRestriction (P.facet restriction) (P.value restriction)

translateFacetRestrictions :
  List P.FacetRestriction → List (S.FacetRestriction PortableSignature)
translateFacetRestrictions [] =
  []
translateFacetRestrictions (restriction ∷ restrictions) =
  translateFacetRestriction restriction
  ∷
  translateFacetRestrictions restrictions

mutual
  translateDataRange :
    P.DataRange → Optional (S.DataRange PortableSignature)
  translateDataRange (P.datatype d) =
    present (S.datatype d)
  translateDataRange P.dataTop =
    present S.dataTop
  translateDataRange P.dataBottom =
    present S.dataBottom
  translateDataRange (P.dataComplementOf d) =
    optionalMap S.dataComplementOf (translateDataRange d)
  translateDataRange (P.dataIntersectionOf ds) =
    optionalMap S.dataIntersectionOf (translateDataRangeTwoOrMore ds)
  translateDataRange (P.dataUnionOf ds) =
    optionalMap S.dataUnionOf (translateDataRangeTwoOrMore ds)
  translateDataRange (P.dataOneOf xs) =
    present (S.dataOneOf (oneOrMoreToList xs))
  translateDataRange (P.datatypeRestriction d facets) =
    present (S.datatypeRestriction d (translateFacetRestrictions facets))

  translateDataRanges :
    List P.DataRange → Optional (List (S.DataRange PortableSignature))
  translateDataRanges [] =
    present []
  translateDataRanges (d ∷ ds) with translateDataRange d | translateDataRanges ds
  ... | present d′ | present ds′ =
    present (d′ ∷ ds′)
  ... | absent | _ =
    absent
  ... | _ | absent =
    absent

  translateDataRangeTwoOrMore :
    P.TwoOrMore P.DataRange → Optional (List (S.DataRange PortableSignature))
  translateDataRangeTwoOrMore ds with
    translateDataRange (P.first ds) |
    translateDataRange (P.second ds) |
    translateDataRanges (P.rest ds)
  ... | present first′ | present second′ | present rest′ =
    present (first′ ∷ second′ ∷ rest′)
  ... | absent | _ | _ =
    absent
  ... | _ | absent | _ =
    absent
  ... | _ | _ | absent =
    absent

  translateClassExpression :
    P.ClassExpression → Optional (S.ClassExpression PortableSignature)
  translateClassExpression (P.namedClass c) =
    present (S.namedClass c)
  translateClassExpression P.owlThing =
    present S.owlThing
  translateClassExpression P.owlNothing =
    present S.owlNothing
  translateClassExpression (P.objectIntersectionOf cs) =
    optionalMap S.objectIntersectionOf
      (translateClassExpressionTwoOrMore cs)
  translateClassExpression (P.objectUnionOf cs) =
    optionalMap S.objectUnionOf
      (translateClassExpressionTwoOrMore cs)
  translateClassExpression (P.objectComplementOf c) =
    optionalMap S.objectComplementOf (translateClassExpression c)
  translateClassExpression (P.objectOneOf xs) =
    present (S.objectOneOf (oneOrMoreToList xs))
  translateClassExpression (P.objectSomeValuesFrom p c) =
    optionalMap
      (S.objectSomeValuesFrom (translateObjectPropertyExpression p))
      (translateClassExpression c)
  translateClassExpression (P.objectAllValuesFrom p c) =
    optionalMap
      (S.objectAllValuesFrom (translateObjectPropertyExpression p))
      (translateClassExpression c)
  translateClassExpression (P.objectHasValue p x) =
    present (S.objectHasValue (translateObjectPropertyExpression p) x)
  translateClassExpression (P.objectHasSelf p) =
    present (S.objectHasSelf (translateObjectPropertyExpression p))
  translateClassExpression (P.objectMinCardinality n p c) =
    optionalMap
      (S.objectMinCardinality n (translateObjectPropertyExpression p))
      (translateOptionalClassExpression c)
  translateClassExpression (P.objectMaxCardinality n p c) =
    optionalMap
      (S.objectMaxCardinality n (translateObjectPropertyExpression p))
      (translateOptionalClassExpression c)
  translateClassExpression (P.objectExactCardinality n p c) =
    optionalMap
      (S.objectExactCardinality n (translateObjectPropertyExpression p))
      (translateOptionalClassExpression c)
  translateClassExpression (P.dataSomeValuesFrom p d) with translateDataRange d
  ... | present d′ =
    present (S.dataSomeValuesFrom (translateDataPropertyExpression p) d′)
  ... | absent =
    absent
  translateClassExpression (P.dataAllValuesFrom p d) with translateDataRange d
  ... | present d′ =
    present (S.dataAllValuesFrom (translateDataPropertyExpression p) d′)
  ... | absent =
    absent
  translateClassExpression (P.dataHasValue p lit) =
    present (S.dataHasValue (translateDataPropertyExpression p) lit)
  translateClassExpression (P.dataMinCardinality n p d) =
    optionalMap
      (S.dataMinCardinality n (translateDataPropertyExpression p))
      (translateOptionalDataRange d)
  translateClassExpression (P.dataMaxCardinality n p d) =
    optionalMap
      (S.dataMaxCardinality n (translateDataPropertyExpression p))
      (translateOptionalDataRange d)
  translateClassExpression (P.dataExactCardinality n p d) =
    optionalMap
      (S.dataExactCardinality n (translateDataPropertyExpression p))
      (translateOptionalDataRange d)

  translateOptionalClassExpression :
    Optional P.ClassExpression →
    Optional (Optional (S.ClassExpression PortableSignature))
  translateOptionalClassExpression absent =
    present absent
  translateOptionalClassExpression (present c) =
    optionalMap present (translateClassExpression c)

  translateOptionalDataRange :
    Optional P.DataRange →
    Optional (Optional (S.DataRange PortableSignature))
  translateOptionalDataRange absent =
    present absent
  translateOptionalDataRange (present d) =
    optionalMap present (translateDataRange d)

  translateClassExpressions :
    List P.ClassExpression → Optional (List (S.ClassExpression PortableSignature))
  translateClassExpressions [] =
    present []
  translateClassExpressions (c ∷ cs) with
    translateClassExpression c | translateClassExpressions cs
  ... | present c′ | present cs′ =
    present (c′ ∷ cs′)
  ... | absent | _ =
    absent
  ... | _ | absent =
    absent

  translateClassExpressionTwoOrMore :
    P.TwoOrMore P.ClassExpression →
    Optional (List (S.ClassExpression PortableSignature))
  translateClassExpressionTwoOrMore cs with
    translateClassExpression (P.first cs) |
    translateClassExpression (P.second cs) |
    translateClassExpressions (P.rest cs)
  ... | present first′ | present second′ | present rest′ =
    present (first′ ∷ second′ ∷ rest′)
  ... | absent | _ | _ =
    absent
  ... | _ | absent | _ =
    absent
  ... | _ | _ | absent =
    absent

translateEntity : P.Entity → S.Entity PortableSignature
translateEntity (P.classEntity c) =
  S.classEntity c
translateEntity (P.objectPropertyEntity p) =
  S.objectPropertyEntity p
translateEntity (P.dataPropertyEntity p) =
  S.dataPropertyEntity p
translateEntity (P.datatypeEntity d) =
  S.datatypeEntity d
translateEntity (P.namedIndividualEntity i) =
  S.individualEntity (P.namedIndividual i)
translateEntity (P.annotationPropertyEntity p) =
  S.annotationPropertyEntity p

translateClassExpressionList :
  List P.ClassExpression → Optional (List (S.ClassExpression PortableSignature))
translateClassExpressionList =
  translateClassExpressions

translateObjectPropertyExpressionList :
  List P.ObjectPropertyExpression →
  List (S.ObjectPropertyExpression PortableSignature)
translateObjectPropertyExpressionList [] =
  []
translateObjectPropertyExpressionList (p ∷ ps) =
  translateObjectPropertyExpression p ∷ translateObjectPropertyExpressionList ps

translateObjectPropertyChain :
  P.ObjectPropertyChain → S.SubObjectPropertyExpression PortableSignature
translateObjectPropertyChain (P.objectPropertyChain ps) =
  S.subObjectPropertyChain
    (translateObjectPropertyExpression (P.first ps))
    (translateObjectPropertyExpression (P.second ps))
    (translateObjectPropertyExpressionList (P.rest ps))

translateDataPropertyExpressionList :
  List P.DataPropertyExpression →
  List (S.DataPropertyExpression PortableSignature)
translateDataPropertyExpressionList [] =
  []
translateDataPropertyExpressionList (p ∷ ps) =
  translateDataPropertyExpression p ∷ translateDataPropertyExpressionList ps

translateIndividuals : List P.Individual → List (S.IndividualName PortableSignature)
translateIndividuals xs =
  xs

translatePropertyKey : P.PropertyKey → S.PropertyKey PortableSignature
translatePropertyKey key =
  S.propertyKey
    (translateObjectPropertyExpressionList (P.objectProperties key))
    (translateDataPropertyExpressionList (P.dataProperties key))

translateSubObjectPropertyExpression :
  P.SubObjectPropertyExpression →
  S.SubObjectPropertyExpression PortableSignature
translateSubObjectPropertyExpression (P.subObjectProperty p) =
  S.subObjectProperty (translateObjectPropertyExpression p)
translateSubObjectPropertyExpression (P.subObjectPropertyChain c) =
  translateObjectPropertyChain c

translateAxiom : P.Axiom → Optional (List (S.Axiom PortableSignature))
translateAxiom (P.declaration e) =
  present (S.declaration (translateEntity e) ∷ [])
translateAxiom (P.subClassOf c d) with
  translateClassExpression c | translateClassExpression d
... | present c′ | present d′ =
  present (S.subClassOf c′ d′ ∷ [])
... | _ | _ =
  absent
translateAxiom (P.equivalentClasses cs) =
  optionalMap (λ xs → S.equivalentClasses xs ∷ [])
    (translateClassExpressionList (twoOrMoreToList cs))
translateAxiom (P.disjointClasses cs) =
  optionalMap (λ xs → S.disjointClasses xs ∷ [])
    (translateClassExpressionList (twoOrMoreToList cs))
translateAxiom (P.disjointUnion c cs) =
  optionalMap
    (λ xs →
      S.equivalentClasses (S.namedClass c ∷ S.objectUnionOf xs ∷ []) ∷
      S.disjointClasses xs ∷ [])
    (translateClassExpressionList (twoOrMoreToList cs))
translateAxiom (P.subObjectPropertyOf p q) =
  present
    (S.subObjectPropertyOf
      (translateSubObjectPropertyExpression p)
      (translateObjectPropertyExpression q)
     ∷ [])
translateAxiom (P.equivalentObjectProperties ps) =
  present
    (S.equivalentObjectProperties
      (translateObjectPropertyExpressionList (twoOrMoreToList ps))
     ∷ [])
translateAxiom (P.disjointObjectProperties ps) =
  present
    (S.disjointObjectProperties
      (translateObjectPropertyExpressionList (twoOrMoreToList ps))
     ∷ [])
translateAxiom (P.inverseObjectProperties p q) =
  present
    (S.equivalentObjectProperties
      (translateObjectPropertyExpression p ∷
       S.objectInverseOf (translateObjectPropertyExpression q) ∷ [])
     ∷ [])
translateAxiom (P.objectPropertyDomain p c) with translateClassExpression c
... | present c′ =
  present (S.objectPropertyDomain (translateObjectPropertyExpression p) c′ ∷ [])
... | absent =
  absent
translateAxiom (P.objectPropertyRange p c) with translateClassExpression c
... | present c′ =
  present (S.objectPropertyRange (translateObjectPropertyExpression p) c′ ∷ [])
... | absent =
  absent
translateAxiom (P.functionalObjectProperty p) =
  present (S.functionalObjectProperty (translateObjectPropertyExpression p) ∷ [])
translateAxiom (P.inverseFunctionalObjectProperty p) =
  present (S.inverseFunctionalObjectProperty (translateObjectPropertyExpression p) ∷ [])
translateAxiom (P.reflexiveObjectProperty p) =
  present (S.reflexiveObjectProperty (translateObjectPropertyExpression p) ∷ [])
translateAxiom (P.irreflexiveObjectProperty p) =
  present (S.irreflexiveObjectProperty (translateObjectPropertyExpression p) ∷ [])
translateAxiom (P.symmetricObjectProperty p) =
  present (S.symmetricObjectProperty (translateObjectPropertyExpression p) ∷ [])
translateAxiom (P.asymmetricObjectProperty p) =
  present (S.asymmetricObjectProperty (translateObjectPropertyExpression p) ∷ [])
translateAxiom (P.transitiveObjectProperty p) =
  present (S.transitiveObjectProperty (translateObjectPropertyExpression p) ∷ [])
translateAxiom (P.subDataPropertyOf p q) =
  present
    (S.subDataPropertyOf
      (translateDataPropertyExpression p)
      (translateDataPropertyExpression q)
     ∷ [])
translateAxiom (P.equivalentDataProperties ps) =
  present
    (S.equivalentDataProperties
      (translateDataPropertyExpressionList (twoOrMoreToList ps))
     ∷ [])
translateAxiom (P.disjointDataProperties ps) =
  present
    (S.disjointDataProperties
      (translateDataPropertyExpressionList (twoOrMoreToList ps))
     ∷ [])
translateAxiom (P.dataPropertyDomain p c) with translateClassExpression c
... | present c′ =
  present (S.dataPropertyDomain (translateDataPropertyExpression p) c′ ∷ [])
... | absent =
  absent
translateAxiom (P.dataPropertyRange p d) with translateDataRange d
... | present d′ =
  present (S.dataPropertyRange (translateDataPropertyExpression p) d′ ∷ [])
... | absent =
  absent
translateAxiom (P.functionalDataProperty p) =
  present (S.functionalDataProperty (translateDataPropertyExpression p) ∷ [])
translateAxiom (P.datatypeDefinition d r) with translateDataRange r
... | present r′ =
  present (S.datatypeDefinition d r′ ∷ [])
... | absent =
  absent
translateAxiom (P.hasKey c k) with translateClassExpression c
... | present c′ =
  present (S.hasKey c′ (translatePropertyKey k) ∷ [])
... | absent =
  absent
translateAxiom (P.sameIndividual xs) =
  present (S.sameIndividual (translateIndividuals (twoOrMoreToList xs)) ∷ [])
translateAxiom (P.differentIndividuals xs) =
  present (S.differentIndividuals (translateIndividuals (twoOrMoreToList xs)) ∷ [])
translateAxiom (P.classAssertion c x) with translateClassExpression c
... | present c′ =
  present (S.classAssertion c′ x ∷ [])
... | absent =
  absent
translateAxiom (P.objectPropertyAssertion p x y) =
  present
    (S.objectPropertyAssertion
      (translateObjectPropertyExpression p)
      x y
     ∷ [])
translateAxiom (P.negativeObjectPropertyAssertion p x y) =
  present
    (S.negativeObjectPropertyAssertion
      (translateObjectPropertyExpression p)
      x y
     ∷ [])
translateAxiom (P.dataPropertyAssertion p x lit) =
  present
    (S.dataPropertyAssertion
      (translateDataPropertyExpression p)
      x lit
     ∷ [])
translateAxiom (P.negativeDataPropertyAssertion p x lit) =
  present
    (S.negativeDataPropertyAssertion
      (translateDataPropertyExpression p)
      x lit
     ∷ [])
translateAxiom (P.annotationAssertion p s v) =
  present []
translateAxiom (P.subAnnotationPropertyOf p q) =
  present []
translateAxiom (P.annotationPropertyDomain p i) =
  present []
translateAxiom (P.annotationPropertyRange p i) =
  present []

record AxiomTranslation : Type₀ where
  constructor axiomTranslation
  field
    semanticAxioms  : List (S.Axiom PortableSignature)
    unsupportedAxioms : List (P.Annotated P.Axiom)

open AxiomTranslation public

appendAxiomTranslation : AxiomTranslation → AxiomTranslation → AxiomTranslation
appendAxiomTranslation left right =
  axiomTranslation
    (semanticAxioms left ++ semanticAxioms right)
    (unsupportedAxioms left ++ unsupportedAxioms right)

translateAnnotatedAxiom : P.Annotated P.Axiom → AxiomTranslation
translateAnnotatedAxiom ax with translateAxiom (P.body ax)
... | present axioms =
  axiomTranslation axioms []
... | absent =
  axiomTranslation [] (ax ∷ [])

translateAnnotatedAxioms : List (P.Annotated P.Axiom) → AxiomTranslation
translateAnnotatedAxioms [] =
  axiomTranslation [] []
translateAnnotatedAxioms (ax ∷ axs) =
  appendAxiomTranslation
    (translateAnnotatedAxiom ax)
    (translateAnnotatedAxioms axs)

ontologyIdIRIs : P.OntologyID → List (S.IRI PortableSignature)
ontologyIdIRIs P.anonymousOntology =
  []
ontologyIdIRIs (P.ontologyIRI i v) =
  i ∷ optionalVersion v
  where
  optionalVersion : Optional P.IRI → List P.IRI
  optionalVersion absent =
    []
  optionalVersion (present versionIRI) =
    versionIRI ∷ []

record SemanticTranslation : Type₀ where
  constructor semanticTranslation
  field
    semanticOntology : S.Ontology PortableSignature
    unsupported : List (P.Annotated P.Axiom)

open SemanticTranslation public

partialTranslateOntology : P.Ontology → SemanticTranslation
partialTranslateOntology o =
  semanticTranslation
    (S.ontology
      (ontologyIdIRIs (P.id o))
      (P.imports o)
      (semanticAxioms axiomResult))
    (unsupportedAxioms axiomResult)
  where
  axiomResult : AxiomTranslation
  axiomResult =
    translateAnnotatedAxioms (P.axioms o)

partialTranslateOntologyDocument : P.OntologyDocument → SemanticTranslation
partialTranslateOntologyDocument doc =
  partialTranslateOntology (P.documentOntology doc)

CompleteSemanticTranslation : P.OntologyDocument → Type₀
CompleteSemanticTranslation doc =
  unsupported (partialTranslateOntologyDocument doc) ≡ []

PartialSatisfiesOntologyDocument :
  ∀ {ℓObj ℓData ℓSem} →
  D.Interpretation PortableSignature ℓObj ℓData ℓSem →
  P.OntologyDocument →
  Type (D.SemLevel ℓ-zero ℓObj ℓData ℓSem)
PartialSatisfiesOntologyDocument I doc =
  D.SatisfiesOntology I
    (semanticOntology (partialTranslateOntologyDocument doc))

PartialModel :
  ∀ {ℓObj ℓData ℓSem} →
  D.Interpretation PortableSignature ℓObj ℓData ℓSem →
  P.OntologyDocument →
  Type (D.SemLevel ℓ-zero ℓObj ℓData ℓSem)
PartialModel =
  PartialSatisfiesOntologyDocument