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

module OWL2.Examples.OBOGraph.Json.PropertyChainAxiom where

open import OWL2.Prelude
  using (String; List; []; _∷_; _≡_; refl; absent; present; tt; tt*)
open import OWL2.Check.Result using (Clean)
import OWL2.OBOGraph.Check as Check
import OWL2.OBOGraph.Report as Report
import OWL2.OBOGraph.Syntax as OG
import OWL2.OBOGraph.ToPortable as OGP
import OWL2.OBOGraph.Validate as Validate
import OWL2.Portable.Syntax as P

hasParent hasGrandparent : String
hasParent =
  "http://example.org/hasParent"
hasGrandparent =
  "http://example.org/hasGrandparent"

objectPropertyNode : String → OG.Node
objectPropertyNode text =
  OG.node text absent OG.propertyNode (present OG.objectProperty) OG.emptyMeta

propertyNodes : List OG.Node
propertyNodes =
  objectPropertyNode hasParent ∷
  objectPropertyNode hasGrandparent ∷
  []

grandparentChain : OG.PropertyChainAxiom
grandparentChain =
  OG.propertyChainAxiom hasGrandparent (hasParent ∷ hasParent ∷ []) OG.emptyMeta

name : String → P.Name
name text =
  P.named (P.iri text)

objectPropertyExpression : String → P.ObjectPropertyExpression
objectPropertyExpression text =
  P.objectProperty (name text)

objectPropertyDeclaration : String → P.Annotated P.Axiom
objectPropertyDeclaration text =
  P.annotated [] (P.declaration (P.objectPropertyEntity (name text)))

annotationPropertyDeclaration : String → P.Annotated P.Axiom
annotationPropertyDeclaration text =
  P.annotated [] (P.declaration (P.annotationPropertyEntity (P.iri text)))

expectedGrandparentChainAxiom : P.Annotated P.Axiom
expectedGrandparentChainAxiom =
  P.annotated []
    (P.subObjectPropertyOf
      (P.subObjectPropertyChain
        (P.objectPropertyChain
          (P.twoOrMore
            (objectPropertyExpression hasParent)
            (objectPropertyExpression hasParent)
            [])))
      (objectPropertyExpression hasGrandparent))

propertyChainAxiomToPortable-ok :
  OGP.propertyChainAxiomToPortable propertyNodes grandparentChain
  ≡ expectedGrandparentChainAxiom ∷ []
propertyChainAxiomToPortable-ok =
  refl

propertyChainGraph : OG.Graph
propertyChainGraph =
  OG.graph
    absent
    absent
    OG.emptyMeta
    propertyNodes
    []
    []
    []
    []
    (grandparentChain ∷ [])
    []

propertyChainGraphDocument : OG.GraphDocument
propertyChainGraphDocument =
  OG.graphDocument (propertyChainGraph ∷ [])

ontologyDocument : P.OntologyDocument
ontologyDocument =
  OGP.toOntologyDocument propertyChainGraphDocument

ontologyAxioms :
  List (P.Annotated P.Axiom)
ontologyAxioms =
  P.axioms (P.documentOntology ontologyDocument)

ontologyAxioms-ok :
  ontologyAxioms
  ≡
  objectPropertyDeclaration hasParent ∷
  objectPropertyDeclaration hasGrandparent ∷
  expectedGrandparentChainAxiom ∷
  []
ontologyAxioms-ok =
  refl

checkResult : Check.OBOGraphDocumentCheckResult
checkResult =
  Check.checkOBOGraphDocument propertyChainGraphDocument

checkClean : Clean checkResult
checkClean =
  tt

complete :
  Validate.CompleteGraphDocument propertyChainGraphDocument
complete =
  Check.completeGraphDocumentFromClean checkResult checkClean

shortGrandparentChain : OG.PropertyChainAxiom
shortGrandparentChain =
  OG.propertyChainAxiom hasGrandparent (hasParent ∷ []) OG.emptyMeta

shortChainWarningAxiom : P.Annotated P.Axiom
shortChainWarningAxiom =
  P.annotated []
    (P.annotationAssertion
      (P.iri OGP.ffImportWarning)
      (P.annotationSubjectIRI (P.iri hasGrandparent))
      (P.annotationValueLiteral
        (P.stringLiteral
          "unsupported property chain shorter than two properties")))

shortChainAxiomToPortable-warning :
  OGP.propertyChainAxiomToPortable propertyNodes shortGrandparentChain
  ≡ shortChainWarningAxiom ∷ []
shortChainAxiomToPortable-warning =
  refl

shortChainGraph : OG.Graph
shortChainGraph =
  OG.graph
    absent
    absent
    OG.emptyMeta
    propertyNodes
    []
    []
    []
    []
    (shortGrandparentChain ∷ [])
    []

shortChainGraphDocument : OG.GraphDocument
shortChainGraphDocument =
  OG.graphDocument (shortChainGraph ∷ [])

shortChainOntologyDocument : P.OntologyDocument
shortChainOntologyDocument =
  OGP.toOntologyDocument shortChainGraphDocument

shortChainOntologyAxioms :
  List (P.Annotated P.Axiom)
shortChainOntologyAxioms =
  P.axioms (P.documentOntology shortChainOntologyDocument)

shortChainOntologyAxioms-warning :
  shortChainOntologyAxioms
  ≡
  objectPropertyDeclaration hasParent ∷
  objectPropertyDeclaration hasGrandparent ∷
  annotationPropertyDeclaration OGP.ffImportWarning ∷
  shortChainWarningAxiom ∷
  []
shortChainOntologyAxioms-warning =
  refl

shortChainImportWarningCount :
  Report.documentReportImportWarningCount
    (Report.reportDocument shortChainGraphDocument)
  ≡ 
shortChainImportWarningCount =
  refl