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

module OWL2.OBOGraph.Syntax where

open import OWL2.Prelude

data NodeType : Type₀ where
  classNode individualNode propertyNode unknownNode : NodeType

data PropertyType : Type₀ where
  objectProperty annotationProperty dataProperty unknownProperty : PropertyType

record PropertyValue : Type₀ where
  constructor propertyValue
  field
    propertyPredicate : String
    propertyValueText : String
    propertyValueType : Optional String

open PropertyValue public

record Synonym : Type₀ where
  constructor synonym
  field
    synonymPredicate : String
    synonymValue     : String

open Synonym public

record Meta : Type₀ where
  constructor meta
  field
    definition          : Optional String
    comments            : List String
    xrefs               : List String
    subsets             : List String
    synonyms            : List Synonym
    basicPropertyValues : List PropertyValue
    deprecated          : Bool
    unsupported         : List String

open Meta public

emptyMeta : Meta
emptyMeta =
  meta absent [] [] [] [] [] false []

record Node : Type₀ where
  constructor node
  field
    nodeId           : String
    nodeLabel        : Optional String
    nodeType         : NodeType
    nodePropertyType : Optional PropertyType
    nodeMeta         : Meta

open Node public

record Edge : Type₀ where
  constructor edge
  field
    edgeSubject   : String
    edgePredicate : String
    edgeObject    : String
    edgeMeta      : Meta

open Edge public

record DomainRangeAxiom : Type₀ where
  constructor domainRangeAxiom
  field
    domainRangePredicate : String
    domainClassIds       : List String
    rangeClassIds        : List String
    allValuesFromEdges   : List Edge
    domainRangeMeta      : Meta

open DomainRangeAxiom public

record PropertyChainAxiom : Type₀ where
  constructor propertyChainAxiom
  field
    chainPredicateId  : String
    chainPredicateIds : List String
    chainMeta         : Meta

open PropertyChainAxiom public

record ExistentialRestriction : Type₀ where
  constructor existentialRestriction
  field
    restrictionPropertyId : String
    restrictionFillerId   : String

open ExistentialRestriction public

record LogicalDefinitionAxiom : Type₀ where
  constructor logicalDefinitionAxiom
  field
    definedClassId : String
    genusIds       : List String
    restrictions   : List ExistentialRestriction
    logicalDefinitionMeta : Meta

open LogicalDefinitionAxiom public

record EquivalentNodesSet : Type₀ where
  constructor equivalentNodesSet
  field
    representativeNodeId : Optional String
    nodeIds              : List String
    equivalentMeta       : Meta

open EquivalentNodesSet public

record Graph : Type₀ where
  constructor graph
  field
    graphId                  : Optional String
    graphVersion             : Optional String
    graphMeta                : Meta
    nodes                    : List Node
    edges                    : List Edge
    equivalentNodesSets      : List EquivalentNodesSet
    logicalDefinitionAxioms  : List LogicalDefinitionAxiom
    domainRangeAxioms        : List DomainRangeAxiom
    propertyChainAxioms      : List PropertyChainAxiom
    graphUnsupported         : List String

open Graph public

record GraphDocument : Type₀ where
  constructor graphDocument
  field
    graphs : List Graph

open GraphDocument public