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

module OWL2.Syntax where

open import OWL2.Prelude

record Signature (ℓ : Level) : Type (ℓ-suc ℓ) where
  field
    IRI                    : Type ℓ
    ClassName              : Type ℓ
    ObjectPropertyName     : Type ℓ
    DataPropertyName       : Type ℓ
    DatatypeName           : Type ℓ
    IndividualName         : Type ℓ
    Literal                : Type ℓ
    FacetName              : Type ℓ
    AnnotationPropertyName : Type ℓ

open Signature public

data EntityKind : Type₀ where
  class objectProperty dataProperty datatype individual annotationProperty : EntityKind

data Entity {ℓ : Level} (Sig : Signature ℓ) : Type ℓ where
  classEntity :
    ClassName Sig → Entity Sig
  objectPropertyEntity :
    ObjectPropertyName Sig → Entity Sig
  dataPropertyEntity :
    DataPropertyName Sig → Entity Sig
  datatypeEntity :
    DatatypeName Sig → Entity Sig
  individualEntity :
    IndividualName Sig → Entity Sig
  annotationPropertyEntity :
    AnnotationPropertyName Sig → Entity Sig

data ObjectPropertyExpression {ℓ : Level} (Sig : Signature ℓ) : Type ℓ where
  objectProperty :
    ObjectPropertyName Sig → ObjectPropertyExpression Sig
  topObjectProperty :
    ObjectPropertyExpression Sig
  bottomObjectProperty :
    ObjectPropertyExpression Sig
  objectInverseOf :
    ObjectPropertyExpression Sig → ObjectPropertyExpression Sig

data SubObjectPropertyExpression {ℓ : Level} (Sig : Signature ℓ) : Type ℓ where
  subObjectProperty :
    ObjectPropertyExpression Sig → SubObjectPropertyExpression Sig
  subObjectPropertyChain :
    ObjectPropertyExpression Sig →
    ObjectPropertyExpression Sig →
    List (ObjectPropertyExpression Sig) →
    SubObjectPropertyExpression Sig

data DataPropertyExpression {ℓ : Level} (Sig : Signature ℓ) : Type ℓ where
  dataProperty :
    DataPropertyName Sig → DataPropertyExpression Sig
  topDataProperty :
    DataPropertyExpression Sig
  bottomDataProperty :
    DataPropertyExpression Sig

record FacetRestriction {ℓ : Level} (Sig : Signature ℓ) : Type ℓ where
  constructor facetRestriction
  field
    facet : FacetName Sig
    value : Literal Sig

open FacetRestriction public

data DataRange {ℓ : Level} (Sig : Signature ℓ) : Type ℓ where
  datatype :
    DatatypeName Sig → DataRange Sig
  datatypeRestriction :
    DatatypeName Sig → List (FacetRestriction Sig) → DataRange Sig
  dataTop :
    DataRange Sig
  dataBottom :
    DataRange Sig
  dataComplementOf :
    DataRange Sig → DataRange Sig
  dataIntersectionOf :
    List (DataRange Sig) → DataRange Sig
  dataUnionOf :
    List (DataRange Sig) → DataRange Sig
  dataOneOf :
    List (Literal Sig) → DataRange Sig

data ClassExpression {ℓ : Level} (Sig : Signature ℓ) : Type ℓ where
  namedClass :
    ClassName Sig → ClassExpression Sig
  owlThing :
    ClassExpression Sig
  owlNothing :
    ClassExpression Sig
  objectIntersectionOf :
    List (ClassExpression Sig) → ClassExpression Sig
  objectUnionOf :
    List (ClassExpression Sig) → ClassExpression Sig
  objectComplementOf :
    ClassExpression Sig → ClassExpression Sig
  objectOneOf :
    List (IndividualName Sig) → ClassExpression Sig
  objectSomeValuesFrom :
    ObjectPropertyExpression Sig → ClassExpression Sig → ClassExpression Sig
  objectAllValuesFrom :
    ObjectPropertyExpression Sig → ClassExpression Sig → ClassExpression Sig
  objectHasValue :
    ObjectPropertyExpression Sig → IndividualName Sig → ClassExpression Sig
  objectHasSelf :
    ObjectPropertyExpression Sig → ClassExpression Sig
  objectMinCardinality :
    ℕ → ObjectPropertyExpression Sig → Optional (ClassExpression Sig) → ClassExpression Sig
  objectMaxCardinality :
    ℕ → ObjectPropertyExpression Sig → Optional (ClassExpression Sig) → ClassExpression Sig
  objectExactCardinality :
    ℕ → ObjectPropertyExpression Sig → Optional (ClassExpression Sig) → ClassExpression Sig
  dataSomeValuesFrom :
    DataPropertyExpression Sig → DataRange Sig → ClassExpression Sig
  dataAllValuesFrom :
    DataPropertyExpression Sig → DataRange Sig → ClassExpression Sig
  dataHasValue :
    DataPropertyExpression Sig → Literal Sig → ClassExpression Sig
  dataMinCardinality :
    ℕ → DataPropertyExpression Sig → Optional (DataRange Sig) → ClassExpression Sig
  dataMaxCardinality :
    ℕ → DataPropertyExpression Sig → Optional (DataRange Sig) → ClassExpression Sig
  dataExactCardinality :
    ℕ → DataPropertyExpression Sig → Optional (DataRange Sig) → ClassExpression Sig

record PropertyKey {ℓ : Level} (Sig : Signature ℓ) : Type ℓ where
  constructor propertyKey
  field
    objectProperties : List (ObjectPropertyExpression Sig)
    dataProperties   : List (DataPropertyExpression Sig)

open PropertyKey public

data Axiom {ℓ : Level} (Sig : Signature ℓ) : Type ℓ where
  declaration :
    Entity Sig → Axiom Sig

  subClassOf :
    ClassExpression Sig → ClassExpression Sig → Axiom Sig
  equivalentClasses :
    List (ClassExpression Sig) → Axiom Sig
  disjointClasses :
    List (ClassExpression Sig) → Axiom Sig

  subObjectPropertyOf :
    SubObjectPropertyExpression Sig → ObjectPropertyExpression Sig → Axiom Sig
  equivalentObjectProperties :
    List (ObjectPropertyExpression Sig) → Axiom Sig
  disjointObjectProperties :
    List (ObjectPropertyExpression Sig) → Axiom Sig
  objectPropertyDomain :
    ObjectPropertyExpression Sig → ClassExpression Sig → Axiom Sig
  objectPropertyRange :
    ObjectPropertyExpression Sig → ClassExpression Sig → Axiom Sig
  functionalObjectProperty :
    ObjectPropertyExpression Sig → Axiom Sig
  inverseFunctionalObjectProperty :
    ObjectPropertyExpression Sig → Axiom Sig
  reflexiveObjectProperty :
    ObjectPropertyExpression Sig → Axiom Sig
  irreflexiveObjectProperty :
    ObjectPropertyExpression Sig → Axiom Sig
  symmetricObjectProperty :
    ObjectPropertyExpression Sig → Axiom Sig
  asymmetricObjectProperty :
    ObjectPropertyExpression Sig → Axiom Sig
  transitiveObjectProperty :
    ObjectPropertyExpression Sig → Axiom Sig

  subDataPropertyOf :
    DataPropertyExpression Sig → DataPropertyExpression Sig → Axiom Sig
  equivalentDataProperties :
    List (DataPropertyExpression Sig) → Axiom Sig
  disjointDataProperties :
    List (DataPropertyExpression Sig) → Axiom Sig
  dataPropertyDomain :
    DataPropertyExpression Sig → ClassExpression Sig → Axiom Sig
  dataPropertyRange :
    DataPropertyExpression Sig → DataRange Sig → Axiom Sig
  functionalDataProperty :
    DataPropertyExpression Sig → Axiom Sig

  datatypeDefinition :
    DatatypeName Sig → DataRange Sig → Axiom Sig
  hasKey :
    ClassExpression Sig → PropertyKey Sig → Axiom Sig

  sameIndividual :
    List (IndividualName Sig) → Axiom Sig
  differentIndividuals :
    List (IndividualName Sig) → Axiom Sig
  classAssertion :
    ClassExpression Sig → IndividualName Sig → Axiom Sig
  objectPropertyAssertion :
    ObjectPropertyExpression Sig → IndividualName Sig → IndividualName Sig → Axiom Sig
  negativeObjectPropertyAssertion :
    ObjectPropertyExpression Sig → IndividualName Sig → IndividualName Sig → Axiom Sig
  dataPropertyAssertion :
    DataPropertyExpression Sig → IndividualName Sig → Literal Sig → Axiom Sig
  negativeDataPropertyAssertion :
    DataPropertyExpression Sig → IndividualName Sig → Literal Sig → Axiom Sig

record Ontology {ℓ : Level} (Sig : Signature ℓ) : Type ℓ where
  constructor ontology
  field
    ontologyIRI : List (IRI Sig)
    imports     : List (IRI Sig)
    axioms      : List (Axiom Sig)

open Ontology public

record DeclaredClassExpression {ℓ : Level} (Sig : Signature ℓ) : Type ℓ where
  constructor checkedClassExpression
  field
    expression : ClassExpression Sig
    mentions   : List (Entity Sig)

open DeclaredClassExpression public