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

module OWL2.Portable.Syntax where

open import OWL2.Prelude public
  using (Level; Type; String; List; []; ℕ; Optional; absent; present)

-- This module is the portable concrete syntax layer.
--
-- Unlike OWL2.Syntax, it is not parameterized by arbitrary Agda name types.
-- Atomic names are finite lexical payloads for checked import diagnostics and
-- semantic translation. The payload strings below are opaque concrete data,
-- not raw IRI, blank-node, or language-tag fragments.

record OneOrMore {ℓ : Level} (A : Type ℓ) : Type ℓ where
  constructor oneOrMore
  field
    head : A
    tail : List A

open OneOrMore public

record TwoOrMore {ℓ : Level} (A : Type ℓ) : Type ℓ where
  constructor twoOrMore
  field
    first  : A
    second : A
    rest   : List A

open TwoOrMore public

record IRI : Type₀ where
  constructor iri
  field
    payload : String

open IRI public

record PrefixName : Type₀ where
  constructor prefixName
  field
    payload : String

open PrefixName public

record BlankNodeID : Type₀ where
  constructor blankNodeID
  field
    payload : String

open BlankNodeID public

record LanguageTag : Type₀ where
  constructor languageTag
  field
    primary : String
    subtags : List String

open LanguageTag public

record PrefixDeclaration : Type₀ where
  constructor prefix
  field
    name : PrefixName
    namespace : IRI

open PrefixDeclaration public

data ReservedIRI : Type₀ where
  owlThingIRI owlNothingIRI :
    ReservedIRI
  owlTopObjectPropertyIRI owlBottomObjectPropertyIRI :
    ReservedIRI
  owlTopDataPropertyIRI owlBottomDataPropertyIRI :
    ReservedIRI
  rdfPlainLiteralIRI rdfsLiteralIRI xsdStringIRI :
    ReservedIRI

data Name : Type₀ where
  named    : IRI → Name
  reserved : ReservedIRI → Name

ClassName ObjectPropertyName DataPropertyName DatatypeName NamedIndividualName
  AnnotationPropertyName FacetName : Type₀
ClassName =
  Name
ObjectPropertyName =
  Name
DataPropertyName =
  Name
DatatypeName =
  Name
NamedIndividualName =
  IRI
AnnotationPropertyName =
  IRI
FacetName =
  IRI

data Literal : Type₀ where
  typedLiteral :
    String → DatatypeName → Literal
  stringLiteral :
    String → Literal
  languageLiteral :
    String → LanguageTag → Literal

data Individual : Type₀ where
  namedIndividual :
    NamedIndividualName → Individual
  anonymousIndividual :
    BlankNodeID → Individual

data Entity : Type₀ where
  classEntity :
    ClassName → Entity
  objectPropertyEntity :
    ObjectPropertyName → Entity
  dataPropertyEntity :
    DataPropertyName → Entity
  datatypeEntity :
    DatatypeName → Entity
  namedIndividualEntity :
    NamedIndividualName → Entity
  annotationPropertyEntity :
    AnnotationPropertyName → Entity

data AnnotationSubject : Type₀ where
  annotationSubjectIRI :
    IRI → AnnotationSubject
  annotationSubjectAnonymous :
    BlankNodeID → AnnotationSubject

data AnnotationValue : Type₀ where
  annotationValueIRI :
    IRI → AnnotationValue
  annotationValueAnonymous :
    BlankNodeID → AnnotationValue
  annotationValueLiteral :
    Literal → AnnotationValue

data Annotation : Type₀ where
  annotation :
    List Annotation →
    AnnotationPropertyName →
    AnnotationValue →
    Annotation

record Annotated {ℓ : Level} (A : Type ℓ) : Type ℓ where
  constructor annotated
  field
    annotations : List Annotation
    body        : A

open Annotated public

data ObjectPropertyExpression : Type₀ where
  objectProperty :
    ObjectPropertyName → ObjectPropertyExpression
  topObjectProperty :
    ObjectPropertyExpression
  bottomObjectProperty :
    ObjectPropertyExpression
  objectInverseOf :
    ObjectPropertyExpression → ObjectPropertyExpression

data ObjectPropertyChain : Type₀ where
  objectPropertyChain :
    TwoOrMore ObjectPropertyExpression → ObjectPropertyChain

data SubObjectPropertyExpression : Type₀ where
  subObjectProperty :
    ObjectPropertyExpression → SubObjectPropertyExpression
  subObjectPropertyChain :
    ObjectPropertyChain → SubObjectPropertyExpression

data DataPropertyExpression : Type₀ where
  dataProperty :
    DataPropertyName → DataPropertyExpression
  topDataProperty :
    DataPropertyExpression
  bottomDataProperty :
    DataPropertyExpression

record FacetRestriction : Type₀ where
  constructor facetRestriction
  field
    facet : FacetName
    value : Literal

open FacetRestriction public

data DataRange : Type₀ where
  datatype :
    DatatypeName → DataRange
  dataTop :
    DataRange
  dataBottom :
    DataRange
  dataComplementOf :
    DataRange → DataRange
  dataIntersectionOf :
    TwoOrMore DataRange → DataRange
  dataUnionOf :
    TwoOrMore DataRange → DataRange
  dataOneOf :
    OneOrMore Literal → DataRange
  datatypeRestriction :
    DatatypeName → List FacetRestriction → DataRange

data ClassExpression : Type₀ where
  namedClass :
    ClassName → ClassExpression
  owlThing :
    ClassExpression
  owlNothing :
    ClassExpression
  objectIntersectionOf :
    TwoOrMore ClassExpression → ClassExpression
  objectUnionOf :
    TwoOrMore ClassExpression → ClassExpression
  objectComplementOf :
    ClassExpression → ClassExpression
  objectOneOf :
    OneOrMore Individual → ClassExpression
  objectSomeValuesFrom :
    ObjectPropertyExpression → ClassExpression → ClassExpression
  objectAllValuesFrom :
    ObjectPropertyExpression → ClassExpression → ClassExpression
  objectHasValue :
    ObjectPropertyExpression → Individual → ClassExpression
  objectHasSelf :
    ObjectPropertyExpression → ClassExpression
  objectMinCardinality :
    ℕ → ObjectPropertyExpression → Optional ClassExpression → ClassExpression
  objectMaxCardinality :
    ℕ → ObjectPropertyExpression → Optional ClassExpression → ClassExpression
  objectExactCardinality :
    ℕ → ObjectPropertyExpression → Optional ClassExpression → ClassExpression
  dataSomeValuesFrom :
    DataPropertyExpression → DataRange → ClassExpression
  dataAllValuesFrom :
    DataPropertyExpression → DataRange → ClassExpression
  dataHasValue :
    DataPropertyExpression → Literal → ClassExpression
  dataMinCardinality :
    ℕ → DataPropertyExpression → Optional DataRange → ClassExpression
  dataMaxCardinality :
    ℕ → DataPropertyExpression → Optional DataRange → ClassExpression
  dataExactCardinality :
    ℕ → DataPropertyExpression → Optional DataRange → ClassExpression

record PropertyKey : Type₀ where
  constructor propertyKey
  field
    objectProperties : List ObjectPropertyExpression
    dataProperties   : List DataPropertyExpression

open PropertyKey public

data Axiom : Type₀ where
  declaration :
    Entity → Axiom

  subClassOf :
    ClassExpression → ClassExpression → Axiom
  equivalentClasses :
    TwoOrMore ClassExpression → Axiom
  disjointClasses :
    TwoOrMore ClassExpression → Axiom
  disjointUnion :
    ClassName → TwoOrMore ClassExpression → Axiom

  subObjectPropertyOf :
    SubObjectPropertyExpression → ObjectPropertyExpression → Axiom
  equivalentObjectProperties :
    TwoOrMore ObjectPropertyExpression → Axiom
  disjointObjectProperties :
    TwoOrMore ObjectPropertyExpression → Axiom
  inverseObjectProperties :
    ObjectPropertyExpression → ObjectPropertyExpression → Axiom
  objectPropertyDomain :
    ObjectPropertyExpression → ClassExpression → Axiom
  objectPropertyRange :
    ObjectPropertyExpression → ClassExpression → Axiom
  functionalObjectProperty :
    ObjectPropertyExpression → Axiom
  inverseFunctionalObjectProperty :
    ObjectPropertyExpression → Axiom
  reflexiveObjectProperty :
    ObjectPropertyExpression → Axiom
  irreflexiveObjectProperty :
    ObjectPropertyExpression → Axiom
  symmetricObjectProperty :
    ObjectPropertyExpression → Axiom
  asymmetricObjectProperty :
    ObjectPropertyExpression → Axiom
  transitiveObjectProperty :
    ObjectPropertyExpression → Axiom

  subDataPropertyOf :
    DataPropertyExpression → DataPropertyExpression → Axiom
  equivalentDataProperties :
    TwoOrMore DataPropertyExpression → Axiom
  disjointDataProperties :
    TwoOrMore DataPropertyExpression → Axiom
  dataPropertyDomain :
    DataPropertyExpression → ClassExpression → Axiom
  dataPropertyRange :
    DataPropertyExpression → DataRange → Axiom
  functionalDataProperty :
    DataPropertyExpression → Axiom

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

  sameIndividual :
    TwoOrMore Individual → Axiom
  differentIndividuals :
    TwoOrMore Individual → Axiom
  classAssertion :
    ClassExpression → Individual → Axiom
  objectPropertyAssertion :
    ObjectPropertyExpression → Individual → Individual → Axiom
  negativeObjectPropertyAssertion :
    ObjectPropertyExpression → Individual → Individual → Axiom
  dataPropertyAssertion :
    DataPropertyExpression → Individual → Literal → Axiom
  negativeDataPropertyAssertion :
    DataPropertyExpression → Individual → Literal → Axiom

  annotationAssertion :
    AnnotationPropertyName → AnnotationSubject → AnnotationValue → Axiom
  subAnnotationPropertyOf :
    AnnotationPropertyName → AnnotationPropertyName → Axiom
  annotationPropertyDomain :
    AnnotationPropertyName → IRI → Axiom
  annotationPropertyRange :
    AnnotationPropertyName → IRI → Axiom

data OntologyID : Type₀ where
  anonymousOntology :
    OntologyID
  ontologyIRI :
    IRI → Optional IRI → OntologyID

record Ontology : Type₀ where
  constructor ontology
  field
    id          : OntologyID
    imports     : List IRI
    annotations : List Annotation
    axioms      : List (Annotated Axiom)

open Ontology public

record OntologyDocument : Type₀ where
  constructor ontologyDocument
  field
    prefixes         : List PrefixDeclaration
    documentOntology : Ontology

open OntologyDocument public

emptyOntology : Ontology
emptyOntology =
  ontology anonymousOntology [] [] []