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

module OWL2.Raw.Syntax where

open import OWL2.Prelude
open import OWL2.Raw.Provenance

record RawIRI : Type₀ where
  constructor rawIRI
  field
    text : String

open RawIRI public

record RawLiteral : Type₀ where
  constructor rawLiteral
  field
    lexicalForm : String
    datatypeIRI : Optional RawIRI
    languageTag : Optional String

open RawLiteral public

data RawEntityKind : Type₀ where
  rawClass rawObjectProperty rawDataProperty rawDatatype
    rawIndividual rawAnnotationProperty rawUnknownEntityKind :
    RawEntityKind

record RawEntity : Type₀ where
  constructor rawEntity
  field
    kind : RawEntityKind
    iri  : RawIRI

open RawEntity public

data RawObjectPropertyExpression : Type₀ where
  rawObjectProperty :
    RawIRI → RawObjectPropertyExpression
  rawTopObjectProperty rawBottomObjectProperty :
    RawObjectPropertyExpression
  rawObjectInverseOf :
    RawObjectPropertyExpression → RawObjectPropertyExpression

data RawDataPropertyExpression : Type₀ where
  rawDataProperty :
    RawIRI → RawDataPropertyExpression
  rawTopDataProperty rawBottomDataProperty :
    RawDataPropertyExpression

record RawFacetRestriction : Type₀ where
  constructor rawFacetRestriction
  field
    facet : RawIRI
    value : RawLiteral

open RawFacetRestriction public

data RawDataRange : Type₀ where
  rawDatatype :
    RawIRI → RawDataRange
  rawDatatypeRestriction :
    RawIRI → List RawFacetRestriction → RawDataRange
  rawDataTop rawDataBottom :
    RawDataRange
  rawDataComplementOf :
    RawDataRange → RawDataRange
  rawDataIntersectionOf rawDataUnionOf :
    List RawDataRange → RawDataRange
  rawDataOneOf :
    List RawLiteral → RawDataRange

data RawIndividual : Type₀ where
  rawNamedIndividual :
    RawIRI → RawIndividual
  rawAnonymousIndividual :
    String → RawIndividual

data RawClassExpression : Type₀ where
  rawNamedClass :
    RawIRI → RawClassExpression
  rawOwlThing rawOwlNothing :
    RawClassExpression
  rawObjectIntersectionOf rawObjectUnionOf :
    List RawClassExpression → RawClassExpression
  rawObjectOneOf :
    List RawIndividual → RawClassExpression
  rawObjectComplementOf :
    RawClassExpression → RawClassExpression
  rawObjectSomeValuesFrom rawObjectAllValuesFrom :
    RawObjectPropertyExpression → RawClassExpression → RawClassExpression
  rawObjectHasValue :
    RawObjectPropertyExpression → RawIndividual → RawClassExpression
  rawObjectHasSelf :
    RawObjectPropertyExpression → RawClassExpression
  rawObjectMinCardinality rawObjectMaxCardinality rawObjectExactCardinality :
    ℕ → RawObjectPropertyExpression → Optional RawClassExpression →
    RawClassExpression
  rawDataSomeValuesFrom rawDataAllValuesFrom :
    RawDataPropertyExpression → RawDataRange → RawClassExpression
  rawDataHasValue :
    RawDataPropertyExpression → RawLiteral → RawClassExpression
  rawDataMinCardinality rawDataMaxCardinality rawDataExactCardinality :
    ℕ → RawDataPropertyExpression → Optional RawDataRange →
    RawClassExpression

data RawSubObjectPropertyExpression : Type₀ where
  rawSubObjectProperty :
    RawObjectPropertyExpression → RawSubObjectPropertyExpression
  rawSubObjectPropertyChain :
    List RawObjectPropertyExpression → RawSubObjectPropertyExpression

data RawAnnotationSubject : Type₀ where
  rawAnnotationSubjectIRI :
    RawIRI → RawAnnotationSubject
  rawAnnotationSubjectAnonymous :
    String → RawAnnotationSubject

data RawAnnotationValue : Type₀ where
  rawAnnotationValueIRI :
    RawIRI → RawAnnotationValue
  rawAnnotationValueAnonymous :
    String → RawAnnotationValue
  rawAnnotationValueLiteral :
    RawLiteral → RawAnnotationValue

data RawAnnotation : Type₀ where
  rawAnnotation :
    List RawAnnotation →
    RawIRI →
    RawAnnotationValue →
    RawAnnotation

open RawAnnotation public

record RawAnnotated {ℓ : Level} (A : Type ℓ) : Type ℓ where
  constructor rawAnnotated
  field
    annotations : List RawAnnotation
    body        : A

open RawAnnotated public

data RawAxiom : Type₀ where
  rawDeclaration :
    RawEntity → RawAxiom
  rawSubClassOf :
    RawClassExpression → RawClassExpression → RawAxiom
  rawEquivalentClasses rawDisjointClasses :
    List RawClassExpression → RawAxiom
  rawDisjointUnion :
    RawIRI → List RawClassExpression → RawAxiom
  rawSubObjectPropertyOf :
    RawSubObjectPropertyExpression → RawObjectPropertyExpression → RawAxiom
  rawEquivalentObjectProperties :
    List RawObjectPropertyExpression → RawAxiom
  rawDisjointObjectProperties :
    List RawObjectPropertyExpression → RawAxiom
  rawInverseObjectProperties :
    RawObjectPropertyExpression → RawObjectPropertyExpression → RawAxiom
  rawObjectPropertyDomain rawObjectPropertyRange :
    RawObjectPropertyExpression → RawClassExpression → RawAxiom
  rawFunctionalObjectProperty rawInverseFunctionalObjectProperty
    rawReflexiveObjectProperty rawIrreflexiveObjectProperty
    rawSymmetricObjectProperty rawAsymmetricObjectProperty
    rawTransitiveObjectProperty :
    RawObjectPropertyExpression → RawAxiom
  rawSubDataPropertyOf :
    RawDataPropertyExpression → RawDataPropertyExpression → RawAxiom
  rawEquivalentDataProperties rawDisjointDataProperties :
    List RawDataPropertyExpression → RawAxiom
  rawDataPropertyDomain :
    RawDataPropertyExpression → RawClassExpression → RawAxiom
  rawDataPropertyRange :
    RawDataPropertyExpression → RawDataRange → RawAxiom
  rawFunctionalDataProperty :
    RawDataPropertyExpression → RawAxiom
  rawDatatypeDefinition :
    RawIRI → RawDataRange → RawAxiom
  rawHasKey :
    RawClassExpression →
    List RawObjectPropertyExpression →
    List RawDataPropertyExpression →
    RawAxiom
  rawSameIndividual rawDifferentIndividuals :
    List RawIndividual → RawAxiom
  rawClassAssertion :
    RawClassExpression → RawIndividual → RawAxiom
  rawObjectPropertyAssertion :
    RawObjectPropertyExpression → RawIndividual → RawIndividual → RawAxiom
  rawNegativeObjectPropertyAssertion :
    RawObjectPropertyExpression → RawIndividual → RawIndividual → RawAxiom
  rawDataPropertyAssertion :
    RawDataPropertyExpression → RawIndividual → RawLiteral → RawAxiom
  rawNegativeDataPropertyAssertion :
    RawDataPropertyExpression → RawIndividual → RawLiteral → RawAxiom
  rawAnnotationAssertion :
    RawIRI → RawAnnotationSubject → RawAnnotationValue → RawAxiom
  rawSubAnnotationPropertyOf :
    RawIRI → RawIRI → RawAxiom
  rawAnnotationPropertyDomain rawAnnotationPropertyRange :
    RawIRI → RawIRI → RawAxiom
  rawUnsupportedAxiom :
    String → RawAxiom

record RawOntology : Type₀ where
  constructor rawOntology
  field
    provenance  : SourceProvenance
    ontologyIRI : Optional RawIRI
    versionIRI  : Optional RawIRI
    imports     : List RawIRI
    annotations : List RawAnnotation
    axioms      : List (RawAnnotated RawAxiom)

open RawOntology public

emptyRawOntology : SourceProvenance → RawOntology
emptyRawOntology provenance =
  rawOntology provenance absent absent [] [] []