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

module OWL2.DescriptionLogic where

open import OWL2.Prelude
open import OWL2.Syntax

record DLSignature (ℓ : Level) : Type (ℓ-suc ℓ) where
  field
    ConceptName    : Type ℓ
    RoleName       : Type ℓ
    IndividualName : Type ℓ
    DataRoleName   : Type ℓ
    DatatypeName   : Type ℓ
    Literal        : Type ℓ

open DLSignature public

data Role {ℓ : Level} (Sig : DLSignature ℓ) : Type ℓ where
  role :
    RoleName Sig → Role Sig
  topRole :
    Role Sig
  bottomRole :
    Role Sig
  inverse :
    Role Sig → Role Sig

data DataRole {ℓ : Level} (Sig : DLSignature ℓ) : Type ℓ where
  dataRole :
    DataRoleName Sig → DataRole Sig
  topDataRole :
    DataRole Sig
  bottomDataRole :
    DataRole Sig

data DataConcept {ℓ : Level} (Sig : DLSignature ℓ) : Type ℓ where
  datatypeConcept :
    DatatypeName Sig → DataConcept Sig
  dataConceptTop :
    DataConcept Sig
  dataConceptBottom :
    DataConcept Sig

data Concept {ℓ : Level} (Sig : DLSignature ℓ) : Type ℓ where
  atomic :
    ConceptName Sig → Concept Sig
  top :
    Concept Sig
  bottom :
    Concept Sig
  not :
    Concept Sig → Concept Sig
  and :
    List (Concept Sig) → Concept Sig
  or :
    List (Concept Sig) → Concept Sig
  nominal :
    List (IndividualName Sig) → Concept Sig
  exists :
    Role Sig → Concept Sig → Concept Sig
  allValues :
    Role Sig → Concept Sig → Concept Sig
  hasValue :
    Role Sig → IndividualName Sig → Concept Sig
  hasSelf :
    Role Sig → Concept Sig
  dataExists :
    DataRole Sig → DataConcept Sig → Concept Sig
  dataForall :
    DataRole Sig → DataConcept Sig → Concept Sig

data Inclusion {ℓ : Level} (Sig : DLSignature ℓ) : Type ℓ where
  conceptInclusion :
    Concept Sig → Concept Sig → Inclusion Sig
  roleInclusion :
    Role Sig → Role Sig → Inclusion Sig
  dataRoleInclusion :
    DataRole Sig → DataRole Sig → Inclusion Sig
  conceptEquivalence :
    List (Concept Sig) → Inclusion Sig
  conceptDisjointness :
    List (Concept Sig) → Inclusion Sig

record KnowledgeBase {ℓ : Level} (Sig : DLSignature ℓ) : Type ℓ where
  constructor knowledgeBase
  field
    terminology : List (Inclusion Sig)
    assertions  : List (Inclusion Sig)

fromOWLSignature : ∀ {ℓ} → Signature ℓ → DLSignature ℓ
fromOWLSignature Sig .ConceptName =
  ClassName Sig
fromOWLSignature Sig .RoleName =
  ObjectPropertyName Sig
fromOWLSignature Sig .IndividualName =
  OWL2.Syntax.IndividualName Sig
fromOWLSignature Sig .DataRoleName =
  DataPropertyName Sig
fromOWLSignature Sig .DatatypeName =
  OWL2.Syntax.DatatypeName Sig
fromOWLSignature Sig .Literal =
  OWL2.Syntax.Literal Sig

fromObjectProperty :
  ∀ {ℓ} {Sig : Signature ℓ} →
  ObjectPropertyExpression Sig →
  Role (fromOWLSignature Sig)
fromObjectProperty (objectProperty p) =
  role p
fromObjectProperty topObjectProperty =
  topRole
fromObjectProperty bottomObjectProperty =
  bottomRole
fromObjectProperty (objectInverseOf p) =
  inverse (fromObjectProperty p)

fromDataProperty :
  ∀ {ℓ} {Sig : Signature ℓ} →
  DataPropertyExpression Sig →
  DataRole (fromOWLSignature Sig)
fromDataProperty (dataProperty p) =
  dataRole p
fromDataProperty topDataProperty =
  topDataRole
fromDataProperty bottomDataProperty =
  bottomDataRole

fromDataRange :
  ∀ {ℓ} {Sig : Signature ℓ} →
  DataRange Sig →
  DataConcept (fromOWLSignature Sig)
fromDataRange (datatype d) =
  datatypeConcept d
fromDataRange (datatypeRestriction d facets) =
  dataConceptTop
fromDataRange dataTop =
  dataConceptTop
fromDataRange dataBottom =
  dataConceptBottom
fromDataRange (dataComplementOf d) =
  dataConceptTop
fromDataRange (dataIntersectionOf ds) =
  dataConceptTop
fromDataRange (dataUnionOf ds) =
  dataConceptTop
fromDataRange (dataOneOf xs) =
  dataConceptTop

fromClassExpression :
  ∀ {ℓ} {Sig : Signature ℓ} →
  ClassExpression Sig →
  Concept (fromOWLSignature Sig)
fromClassExpression (namedClass c) =
  atomic c
fromClassExpression owlThing =
  top
fromClassExpression owlNothing =
  bottom
fromClassExpression (objectIntersectionOf cs) =
  and (fromClassExpressions cs)
  where
  fromClassExpressions :
    ∀ {ℓ} {Sig : Signature ℓ} →
    List (ClassExpression Sig) →
    List (Concept (fromOWLSignature Sig))
  fromClassExpressions [] =
    []
  fromClassExpressions (c ∷ cs) =
    fromClassExpression c ∷ fromClassExpressions cs
fromClassExpression (objectUnionOf cs) =
  or (fromClassExpressions cs)
  where
  fromClassExpressions :
    ∀ {ℓ} {Sig : Signature ℓ} →
    List (ClassExpression Sig) →
    List (Concept (fromOWLSignature Sig))
  fromClassExpressions [] =
    []
  fromClassExpressions (c ∷ cs) =
    fromClassExpression c ∷ fromClassExpressions cs
fromClassExpression (objectComplementOf c) =
  not (fromClassExpression c)
fromClassExpression (objectOneOf xs) =
  nominal xs
fromClassExpression (objectSomeValuesFrom p c) =
  exists (fromObjectProperty p) (fromClassExpression c)
fromClassExpression (objectAllValuesFrom p c) =
  allValues (fromObjectProperty p) (fromClassExpression c)
fromClassExpression (objectHasValue p a) =
  hasValue (fromObjectProperty p) a
fromClassExpression (objectHasSelf p) =
  hasSelf (fromObjectProperty p)
fromClassExpression (objectMinCardinality n p c) =
  top
fromClassExpression (objectMaxCardinality n p c) =
  top
fromClassExpression (objectExactCardinality n p c) =
  top
fromClassExpression (dataSomeValuesFrom p d) =
  dataExists (fromDataProperty p) (fromDataRange d)
fromClassExpression (dataAllValuesFrom p d) =
  dataForall (fromDataProperty p) (fromDataRange d)
fromClassExpression (dataHasValue p v) =
  dataExists (fromDataProperty p) dataConceptTop
fromClassExpression (dataMinCardinality n p d) =
  top
fromClassExpression (dataMaxCardinality n p d) =
  top
fromClassExpression (dataExactCardinality n p d) =
  top