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

module OWL2.Examples.OBOGraph.Json.AllValuesFromEdges where

open import OWL2.Prelude
  using
    ([]; _∷_; _,_; _≡_; refl; List; Optional; String; absent; false; present;
     tt; tt*)
open import OWL2.Check.Result using (Clean)
import FF.Json.Native as JSON
import OWL2.OBOGraph.Decode as Decode
import OWL2.OBOGraph.Schema as Schema
import OWL2.OBOGraph.Check as Check
import OWL2.OBOGraph.Syntax as OG
import OWL2.OBOGraph.ToPortable as OGP
import OWL2.OBOGraph.Validate as Validate
import OWL2.Portable.Syntax as P

nodeClass : String → OG.Node
nodeClass text =
  OG.node text absent OG.classNode absent OG.emptyMeta

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

nodeDataProperty : String → OG.Node
nodeDataProperty text =
  OG.node text absent OG.propertyNode (present OG.dataProperty) OG.emptyMeta

nodeAnnotationProperty : String → OG.Node
nodeAnnotationProperty text =
  OG.node text absent OG.propertyNode
    (present OG.annotationProperty)
    OG.emptyMeta

nodeUnknownProperty : String → OG.Node
nodeUnknownProperty text =
  OG.node text absent OG.propertyNode (present OG.unknownProperty) OG.emptyMeta

allValuesFromEdge : OG.Edge
allValuesFromEdge =
  OG.edge "A" "R" "B" OG.emptyMeta

domainRangeMetadata : OG.Meta
domainRangeMetadata =
  OG.meta
    absent
    ("domain/range metadata" ∷ [])
    []
    []
    []
    []
    false
    []

dataPropertyAllValuesFromEdge : OG.Edge
dataPropertyAllValuesFromEdge =
  OG.edge "A" "D" "B" OG.emptyMeta

annotationPropertyAllValuesFromEdge : OG.Edge
annotationPropertyAllValuesFromEdge =
  OG.edge "A" "Ann" "B" OG.emptyMeta

unknownPropertyAllValuesFromEdge : OG.Edge
unknownPropertyAllValuesFromEdge =
  OG.edge "A" "UnknownR" "B" OG.emptyMeta

absentPropertyAllValuesFromEdge : OG.Edge
absentPropertyAllValuesFromEdge =
  OG.edge "A" "AbsentR" "B" OG.emptyMeta

nonPropertyAllValuesFromEdge : OG.Edge
nonPropertyAllValuesFromEdge =
  OG.edge "A" "NonPropertyR" "B" OG.emptyMeta

nodes : List OG.Node
nodes =
  nodeClass "A" ∷
  nodeClass "B" ∷
  nodeObjectProperty "R" ∷
  []

policyNodes : List OG.Node
policyNodes =
  nodeClass "A" ∷
  nodeClass "B" ∷
  nodeObjectProperty "R" ∷
  nodeDataProperty "D" ∷
  nodeAnnotationProperty "Ann" ∷
  nodeUnknownProperty "UnknownR" ∷
  nodeClass "NonPropertyR" ∷
  []

allValuesFromDomainRangeAxiom : OG.DomainRangeAxiom
allValuesFromDomainRangeAxiom =
  OG.domainRangeAxiom "R" [] [] (allValuesFromEdge ∷ []) domainRangeMetadata

graph : OG.Graph
graph =
  OG.graph
    absent
    absent
    OG.emptyMeta
    nodes
    []
    []
    []
    (allValuesFromDomainRangeAxiom ∷ [])
    []
    []

graphDocument : OG.GraphDocument
graphDocument =
  OG.graphDocument (graph ∷ [])

jsonValue : JSON.JsonValue
jsonValue =
  JSON.jobject
    (("graphs" ,
      JSON.jarray
        (JSON.jobject
          (("nodes" ,
            JSON.jarray
              (JSON.jobject
                (("id" , JSON.jstring "A") ∷
                 ("type" , JSON.jstring "CLASS") ∷ []) ∷
               JSON.jobject
                (("id" , JSON.jstring "B") ∷
                 ("type" , JSON.jstring "CLASS") ∷ []) ∷
               JSON.jobject
                (("id" , JSON.jstring "R") ∷
                 ("type" , JSON.jstring "PROPERTY") ∷
                 ("propertyType" , JSON.jstring "OBJECT") ∷ []) ∷
               [])) ∷
           ("domainRangeAxioms" ,
            JSON.jarray
              (JSON.jobject
                (("predicateId" , JSON.jstring "R") ∷
                 ("allValuesFromEdges" ,
                  JSON.jarray
                    (JSON.jobject
                      (("sub" , JSON.jstring "A") ∷
                       ("pred" , JSON.jstring "R") ∷
                       ("obj" , JSON.jstring "B") ∷ []) ∷ [])) ∷
                 ("meta" ,
                  JSON.jobject
                    (("comments" ,
                      JSON.jarray
                        (JSON.jstring "domain/range metadata" ∷ [])) ∷ [])) ∷
                 []) ∷
               [])) ∷ []) ∷
         [])) ∷ [])

jsonDiagnostics : List Schema.SchemaDiagnostic
jsonDiagnostics =
  Schema.schemaDiagnostics jsonValue

jsonDiagnostics-ok : jsonDiagnostics ≡ []
jsonDiagnostics-ok =
  refl

decodedGraphDocument : Optional OG.GraphDocument
decodedGraphDocument =
  Decode.decodeGraphDocument jsonValue

decodeGraphDocument-ok : decodedGraphDocument ≡ present graphDocument
decodeGraphDocument-ok =
  refl

allValuesFromPortableAxioms :
  OGP.domainRangeAxiomsToPortable nodes allValuesFromDomainRangeAxiom
  ≡
  P.annotated []
    (P.subClassOf
      (OGP.classExpression "A")
      (P.objectAllValuesFrom
        (OGP.objectPropertyExpression "R")
        (OGP.classExpression "B")))
  ∷ []
allValuesFromPortableAxioms =
  refl

unknownPropertyAllValuesFromPortableAxioms :
  OGP.allValuesFromEdgeToPortable
    policyNodes
    unknownPropertyAllValuesFromEdge
  ≡ OGP.allValuesFromEdgeAxiom unknownPropertyAllValuesFromEdge ∷ []
unknownPropertyAllValuesFromPortableAxioms =
  refl

absentPropertyAllValuesFromPortableAxioms :
  OGP.allValuesFromEdgeToPortable
    policyNodes
    absentPropertyAllValuesFromEdge
  ≡ OGP.allValuesFromEdgeAxiom absentPropertyAllValuesFromEdge ∷ []
absentPropertyAllValuesFromPortableAxioms =
  refl

dataPropertyAllValuesFromWarning :
  OGP.allValuesFromEdgeToPortable
    policyNodes
    dataPropertyAllValuesFromEdge
  ≡ OGP.unsupportedAllValuesFromEdgeAxiom
      dataPropertyAllValuesFromEdge
    ∷ []
dataPropertyAllValuesFromWarning =
  refl

annotationPropertyAllValuesFromWarning :
  OGP.allValuesFromEdgeToPortable
    policyNodes
    annotationPropertyAllValuesFromEdge
  ≡ OGP.unsupportedAllValuesFromEdgeAxiom
      annotationPropertyAllValuesFromEdge
    ∷ []
annotationPropertyAllValuesFromWarning =
  refl

nonPropertyAllValuesFromWarning :
  OGP.allValuesFromEdgeToPortable
    policyNodes
    nonPropertyAllValuesFromEdge
  ≡ OGP.unsupportedAllValuesFromEdgeAxiom
      nonPropertyAllValuesFromEdge
    ∷ []
nonPropertyAllValuesFromWarning =
  refl

ontologyDocument : P.OntologyDocument
ontologyDocument =
  OGP.toOntologyDocument graphDocument

checkResult : Check.OBOGraphDocumentCheckResult
checkResult =
  Check.checkOBOGraphDocument graphDocument

checkClean : Clean checkResult
checkClean =
  tt

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