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

module OWL2.Examples.WebProtege.Datatype where

open import OWL2.Prelude
open import OWL2.Syntax
open import OWL2.DirectSemantics
import OWL2.Datatype.Map as DM
import OWL2.Datatype.XSD.Core as XSD

data WebProtegeDatatypeIRI : Type₀ where
  datatypeDocument : WebProtegeDatatypeIRI

data WebProtegeDatatypeClass : Type₀ where
  Dataset : WebProtegeDatatypeClass

data WebProtegeDatatypeObjectProperty : Type₀ where

data WebProtegeDatatypeDataProperty : Type₀ where
  hasTitle isPublished : WebProtegeDatatypeDataProperty

data WebProtegeDatatypeName : Type₀ where
  xsdStringDatatype xsdBooleanDatatype unsupportedDatatype :
    WebProtegeDatatypeName

data WebProtegeDatatypeIndividual : Type₀ where
  datasetOne : WebProtegeDatatypeIndividual

data WebProtegeDatatypeLiteral : Type₀ where
  titleLiteral publishedTrueLiteral publishedFalseLiteral :
    WebProtegeDatatypeLiteral

data WebProtegeDatatypeFacet : Type₀ where
  requiredBooleanValue : WebProtegeDatatypeFacet

data WebProtegeDatatypeAnnotationProperty : Type₀ where
  label : WebProtegeDatatypeAnnotationProperty

WebProtegeDatatypeSignature : Signature ℓ-zero
WebProtegeDatatypeSignature .IRI =
  WebProtegeDatatypeIRI
WebProtegeDatatypeSignature .ClassName =
  WebProtegeDatatypeClass
WebProtegeDatatypeSignature .ObjectPropertyName =
  WebProtegeDatatypeObjectProperty
WebProtegeDatatypeSignature .DataPropertyName =
  WebProtegeDatatypeDataProperty
WebProtegeDatatypeSignature .DatatypeName =
  WebProtegeDatatypeName
WebProtegeDatatypeSignature .IndividualName =
  WebProtegeDatatypeIndividual
WebProtegeDatatypeSignature .Literal =
  WebProtegeDatatypeLiteral
WebProtegeDatatypeSignature .FacetName =
  WebProtegeDatatypeFacet
WebProtegeDatatypeSignature .AnnotationPropertyName =
  WebProtegeDatatypeAnnotationProperty

webProtegeXSDNames :
  XSD.XSDCoreNames WebProtegeDatatypeSignature
webProtegeXSDNames .XSD.xsdString =
  xsdStringDatatype
webProtegeXSDNames .XSD.xsdBoolean =
  xsdBooleanDatatype
webProtegeXSDNames .XSD.datatypeKind xsdStringDatatype =
  XSD.xsdStringKind
webProtegeXSDNames .XSD.datatypeKind xsdBooleanDatatype =
  XSD.xsdBooleanKind
webProtegeXSDNames .XSD.datatypeKind unsupportedDatatype =
  XSD.unsupportedDatatypeKind

webProtegeLiteralView :
  XSD.XSDCoreLiteralView webProtegeXSDNames
webProtegeLiteralView .XSD.literalDatatypeName titleLiteral =
  xsdStringDatatype
webProtegeLiteralView .XSD.literalDatatypeName publishedTrueLiteral =
  xsdBooleanDatatype
webProtegeLiteralView .XSD.literalDatatypeName publishedFalseLiteral =
  xsdBooleanDatatype
webProtegeLiteralView .XSD.literalLexicalForm titleLiteral =
  XSD.lexicalString "Dataset one"
webProtegeLiteralView .XSD.literalLexicalForm publishedTrueLiteral =
  XSD.lexicalBooleanTrue
webProtegeLiteralView .XSD.literalLexicalForm publishedFalseLiteral =
  XSD.lexicalBooleanFalse
webProtegeLiteralView .XSD.literalValue titleLiteral =
  XSD.stringValue "Dataset one"
webProtegeLiteralView .XSD.literalValue publishedTrueLiteral =
  XSD.booleanValue true
webProtegeLiteralView .XSD.literalValue publishedFalseLiteral =
  XSD.booleanValue false
webProtegeLiteralView .XSD.literalToValue titleLiteral =
  XSD.stringToValue "Dataset one"
webProtegeLiteralView .XSD.literalToValue publishedTrueLiteral =
  XSD.booleanTrueToValue
webProtegeLiteralView .XSD.literalToValue publishedFalseLiteral =
  XSD.booleanFalseToValue

data WebProtegeFacetSatisfied :
  WebProtegeDatatypeName →
  WebProtegeDatatypeFacet →
  WebProtegeDatatypeLiteral →
  XSD.XSDCoreValue →
  Type₀ where
  publishedTrueSatisfiesRequiredBoolean :
    WebProtegeFacetSatisfied
      xsdBooleanDatatype
      requiredBooleanValue
      publishedTrueLiteral
      (XSD.booleanValue true)

webProtegeFacetRespectsValueEqual :
  (d : WebProtegeDatatypeName) →
  (facet : WebProtegeDatatypeFacet) →
  (restrictionValue : WebProtegeDatatypeLiteral) →
  (left right : XSD.XSDCoreValue) →
  XSD.XSDCoreValueEqual {ℓ-zero} left right →
  WebProtegeFacetSatisfied d facet restrictionValue left →
  WebProtegeFacetSatisfied d facet restrictionValue right
webProtegeFacetRespectsValueEqual
  .xsdBooleanDatatype
  .requiredBooleanValue
  .publishedTrueLiteral
  .(XSD.booleanValue true)
  .(XSD.booleanValue true)
  (XSD.sameBooleanValue true)
  publishedTrueSatisfiesRequiredBoolean =
  publishedTrueSatisfiesRequiredBoolean

webProtegeFacetSemantics :
  XSD.XSDCoreFacetSemantics webProtegeXSDNames
webProtegeFacetSemantics .XSD.FacetSatisfied =
  WebProtegeFacetSatisfied
webProtegeFacetSemantics .XSD.facetRespectsValueEqual =
  webProtegeFacetRespectsValueEqual

webProtegeDatatypeMap :
  DM.DatatypeMap WebProtegeDatatypeSignature ℓ-zero ℓ-zero ℓ-zero
webProtegeDatatypeMap =
  XSD.xsdCoreDatatypeMap
    webProtegeLiteralView
    webProtegeFacetSemantics

titleLiteralInStringDatatype :
  DM.LiteralDatatypeMembership
    (DM.rawMap webProtegeDatatypeMap)
    xsdStringDatatype
    titleLiteral
titleLiteralInStringDatatype =
  XSD.stringValue "Dataset one" ,
  (XSD.stringToValue "Dataset one" , XSD.stringMember "Dataset one")

publishedTrueInBooleanDatatype :
  DM.LiteralDatatypeMembership
    (DM.rawMap webProtegeDatatypeMap)
    xsdBooleanDatatype
    publishedTrueLiteral
publishedTrueInBooleanDatatype =
  XSD.booleanValue true ,
  (XSD.booleanTrueToValue , XSD.booleanMember true)

publishedFalseInBooleanDatatype :
  DM.LiteralDatatypeMembership
    (DM.rawMap webProtegeDatatypeMap)
    xsdBooleanDatatype
    publishedFalseLiteral
publishedFalseInBooleanDatatype =
  XSD.booleanValue false ,
  (XSD.booleanFalseToValue , XSD.booleanMember false)

publishedTrueSatisfiesRequiredFacet :
  DM.LiteralSatisfiesFacet
    webProtegeDatatypeMap
    xsdBooleanDatatype
    requiredBooleanValue
    publishedTrueLiteral
    publishedTrueLiteral
publishedTrueSatisfiesRequiredFacet =
  publishedTrueSatisfiesRequiredBoolean

DatasetC :
  ClassExpression WebProtegeDatatypeSignature
DatasetC =
  namedClass Dataset

HasTitle IsPublished :
  DataPropertyExpression WebProtegeDatatypeSignature
HasTitle =
  dataProperty hasTitle
IsPublished =
  dataProperty isPublished

StringRange BooleanRange RequiredTrueRange TitleOneOfRange :
  DataRange WebProtegeDatatypeSignature
StringRange =
  datatype xsdStringDatatype
BooleanRange =
  datatype xsdBooleanDatatype
RequiredTrueRange =
  datatypeRestriction
    xsdBooleanDatatype
    (facetRestriction requiredBooleanValue publishedTrueLiteral ∷ [])
TitleOneOfRange =
  dataOneOf (titleLiteral ∷ [])

data WebProtegeDatatypeObject : Type₀ where
  datasetOneObject : WebProtegeDatatypeObject

data DatasetObject : WebProtegeDatatypeObject → Type₀ where
  datasetOneDataset : DatasetObject datasetOneObject

WebProtegeDatatypeClassDenotation :
  WebProtegeDatatypeClass → WebProtegeDatatypeObject → Type₀
WebProtegeDatatypeClassDenotation Dataset =
  DatasetObject

WebProtegeDatatypeObjectPropertyDenotation :
  WebProtegeDatatypeObjectProperty →
  WebProtegeDatatypeObject → WebProtegeDatatypeObject → Type₀
WebProtegeDatatypeObjectPropertyDenotation ()

data WebProtegeDatatypeDataPropertyRel :
  WebProtegeDatatypeDataProperty →
  WebProtegeDatatypeObject →
  XSD.XSDCoreValue →
  Type₀ where
  datasetOneTitle :
    WebProtegeDatatypeDataPropertyRel
      hasTitle
      datasetOneObject
      (XSD.stringValue "Dataset one")
  datasetOnePublished :
    WebProtegeDatatypeDataPropertyRel
      isPublished
      datasetOneObject
      (XSD.booleanValue true)

WebProtegeDatatypeDataPropertyDenotation :
  WebProtegeDatatypeDataProperty →
  WebProtegeDatatypeObject →
  XSD.XSDCoreValue →
  Type₀
WebProtegeDatatypeDataPropertyDenotation =
  WebProtegeDatatypeDataPropertyRel

WebProtegeDatatypeIndividualDenotation :
  WebProtegeDatatypeIndividual → WebProtegeDatatypeObject
WebProtegeDatatypeIndividualDenotation datasetOne =
  datasetOneObject

webProtegeDatatypeInterpretation :
  Interpretation WebProtegeDatatypeSignature ℓ-zero ℓ-zero ℓ-zero
webProtegeDatatypeInterpretation .ObjectDomain =
  WebProtegeDatatypeObject
webProtegeDatatypeInterpretation .DataDomain =
  XSD.XSDCoreValue
webProtegeDatatypeInterpretation .classDenotation =
  WebProtegeDatatypeClassDenotation
webProtegeDatatypeInterpretation .objectPropertyDenotation =
  WebProtegeDatatypeObjectPropertyDenotation
webProtegeDatatypeInterpretation .dataPropertyDenotation =
  WebProtegeDatatypeDataPropertyDenotation
webProtegeDatatypeInterpretation .datatypeDenotation =
  DM.mapDatatypeMembership webProtegeDatatypeMap
webProtegeDatatypeInterpretation .facetDenotation =
  DM.mapFacetSatisfaction webProtegeDatatypeMap
webProtegeDatatypeInterpretation .individualDenotation =
  WebProtegeDatatypeIndividualDenotation
webProtegeDatatypeInterpretation .literalDenotation =
  DM.literalDenotation webProtegeDatatypeMap

titleValueInStringRange :
  evalDataRange
    webProtegeDatatypeInterpretation
    StringRange
    (XSD.stringValue "Dataset one")
titleValueInStringRange =
  XSD.stringMember "Dataset one"

publishedTrueValueInBooleanRange :
  evalDataRange
    webProtegeDatatypeInterpretation
    BooleanRange
    (XSD.booleanValue true)
publishedTrueValueInBooleanRange =
  XSD.booleanMember true

publishedTrueValueInRequiredTrueRange :
  evalDataRange
    webProtegeDatatypeInterpretation
    RequiredTrueRange
    (XSD.booleanValue true)
publishedTrueValueInRequiredTrueRange =
  XSD.booleanMember true ,
  (publishedTrueSatisfiesRequiredBoolean , tt*)

publishedFalseValueNotInRequiredTrueRange :
  ¬ evalDataRange
      webProtegeDatatypeInterpretation
      RequiredTrueRange
      (XSD.booleanValue false)
publishedFalseValueNotInRequiredTrueRange
  (XSD.booleanMember false , (() , _))

titleValueInOneOfRange :
  evalDataRange
    webProtegeDatatypeInterpretation
    TitleOneOfRange
    (XSD.stringValue "Dataset one")
titleValueInOneOfRange =
  inl (lift refl)

hasTitleRangeString :
  SatisfiesAxiom
    webProtegeDatatypeInterpretation
    (dataPropertyRange HasTitle StringRange)
hasTitleRangeString
  .datasetOneObject
  .(XSD.stringValue "Dataset one")
  datasetOneTitle =
  titleValueInStringRange

isPublishedRangeBoolean :
  SatisfiesAxiom
    webProtegeDatatypeInterpretation
    (dataPropertyRange IsPublished BooleanRange)
isPublishedRangeBoolean
  .datasetOneObject
  .(XSD.booleanValue true)
  datasetOnePublished =
  publishedTrueValueInBooleanRange

datasetOneHasTitle :
  SatisfiesAxiom
    webProtegeDatatypeInterpretation
    (dataPropertyAssertion HasTitle datasetOne titleLiteral)
datasetOneHasTitle =
  datasetOneTitle

datasetOneIsPublished :
  SatisfiesAxiom
    webProtegeDatatypeInterpretation
    (dataPropertyAssertion IsPublished datasetOne publishedTrueLiteral)
datasetOneIsPublished =
  datasetOnePublished