OWL2.Examples.OBOGraph.Json.EquivNodeSetTest

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

module OWL2.Examples.OBOGraph.Json.EquivNodeSetTest where

open import OWL2.Prelude
  using ([]; _∷_; _,_; _≡_; refl; Bool; List; ℕ; false; true; Optional; String; present)
import FF.Json.Native as JSON
import OWL2.OBOGraph.Decode as Decode
import OWL2.OBOGraph.Schema as Schema
import OWL2.OBOGraph.Syntax as OG
import OWL2.OBOGraph.ToPortable as OGP
import OWL2.Portable.Syntax as P

sourceJson : String
sourceJson =
  "/Users/marcin/obographs-small/equivNodeSetTest.json"

sourceJsonBytes : ℕ
sourceJsonBytes =
  11167

sourceJsonSha256 : String
sourceJsonSha256 =
  "sha256:e4c84cc71f6cbd15e9722cd961d703b9d701d931798ff74adb629d034824260d"

sourceGenerator : String
sourceGenerator =
  "/Users/marcin/agdaLibs/ff-owl/scripts/json_to_agda_value.py"

jsonValue : JSON.JsonValue
jsonValue =
  JSON.jobject (("graphs" , JSON.jarray (JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/TEMP") ∷ ("nodes" , JSON.jarray (JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/DOID_0001816") ∷ ("lbl" , JSON.jstring "angiosarcoma") ∷ ("type" , JSON.jstring "CLASS") ∷ ("meta" , JSON.jobject (("definition" , JSON.jobject (("val" , JSON.jstring "A malignant Vascular tumor that results_in rapidly proliferating, extensively infiltrating anaplastic cells derived_from blood vessels and derived_from the lining of irregular blood-filled spaces.") ∷ ("xrefs" , JSON.jarray (JSON.jstring "url:http://emedicine.medscape.com/article/276512-overview" ∷ JSON.jstring "url:http://en.wikipedia.org/wiki/Hemangiosarcoma" ∷ JSON.jstring "url:http://www.ncbi.nlm.nih.gov/pubmed/23327728" ∷ [])) ∷ [])) ∷ ("subsets" , JSON.jarray (JSON.jstring "http://purl.obolibrary.org/obo/TEMP#NCIthesaurus" ∷ [])) ∷ ("synonyms" , JSON.jarray (JSON.jobject (("pred" , JSON.jstring "hasExactSynonym") ∷ ("val" , JSON.jstring "hemangiosarcoma") ∷ []) ∷ [])) ∷ ("xrefs" , JSON.jarray (JSON.jobject (("val" , JSON.jstring "MESH:D006394") ∷ []) ∷ JSON.jobject (("val" , JSON.jstring "NCIT:C3088") ∷ []) ∷ JSON.jobject (("val" , JSON.jstring "NCIT:C9275") ∷ []) ∷ JSON.jobject (("val" , JSON.jstring "Orphanet:263413") ∷ []) ∷ JSON.jobject (("val" , JSON.jstring "SCTID:33176006") ∷ []) ∷ JSON.jobject (("val" , JSON.jstring "SCTID:39000009") ∷ []) ∷ JSON.jobject (("val" , JSON.jstring "SCTID:403977003") ∷ []) ∷ JSON.jobject (("val" , JSON.jstring "UMLS:C0018923") ∷ []) ∷ JSON.jobject (("val" , JSON.jstring "UMLS:C0854893") ∷ []) ∷ [])) ∷ ("basicPropertyValues" , JSON.jarray (JSON.jobject (("pred" , JSON.jstring "http://www.geneontology.org/formats/oboInOwl#hasAlternativeId") ∷ ("val" , JSON.jstring "DOID:267") ∷ []) ∷ JSON.jobject (("pred" , JSON.jstring "http://www.geneontology.org/formats/oboInOwl#hasAlternativeId") ∷ ("val" , JSON.jstring "DOID:4508") ∷ []) ∷ [])) ∷ [])) ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/DOID_267") ∷ ("type" , JSON.jstring "CLASS") ∷ ("meta" , JSON.jobject (("basicPropertyValues" , JSON.jarray (JSON.jobject (("pred" , JSON.jstring "http://purl.obolibrary.org/obo/IAO_0000231") ∷ ("val" , JSON.jstring "http://purl.obolibrary.org/obo/IAO_0000227") ∷ []) ∷ JSON.jobject (("pred" , JSON.jstring "http://purl.obolibrary.org/obo/IAO_0100001") ∷ ("val" , JSON.jstring "http://purl.obolibrary.org/obo/DOID_0001816") ∷ []) ∷ [])) ∷ ("deprecated" , JSON.jbool true) ∷ [])) ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/DOID_4508") ∷ ("type" , JSON.jstring "CLASS") ∷ ("meta" , JSON.jobject (("basicPropertyValues" , JSON.jarray (JSON.jobject (("pred" , JSON.jstring "http://purl.obolibrary.org/obo/IAO_0000231") ∷ ("val" , JSON.jstring "http://purl.obolibrary.org/obo/IAO_0000227") ∷ []) ∷ JSON.jobject (("pred" , JSON.jstring "http://purl.obolibrary.org/obo/IAO_0100001") ∷ ("val" , JSON.jstring "http://purl.obolibrary.org/obo/DOID_0001816") ∷ []) ∷ [])) ∷ ("deprecated" , JSON.jbool true) ∷ [])) ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/NCIT_C121671") ∷ ("lbl" , JSON.jstring "Angiosarcoma of Soft Tissue") ∷ ("type" , JSON.jstring "CLASS") ∷ ("meta" , JSON.jobject (("definition" , JSON.jobject (("val" , JSON.jstring "An angiosarcoma that arises from the soft tissues, usually in the deep muscles of the lower extremities, retroperitoneum, mediastinum, and mesentery.") ∷ ("meta" , JSON.jobject (("basicPropertyValues" , JSON.jarray (JSON.jobject (("pred" , JSON.jstring "http://www.geneontology.org/formats/oboInOwl#http://purl.obolibrary.org/obo/IAO_0000119") ∷ ("val" , JSON.jstring "NCI") ∷ []) ∷ [])) ∷ [])) ∷ [])) ∷ ("synonyms" , JSON.jarray (JSON.jobject (("pred" , JSON.jstring "hasExactSynonym") ∷ ("val" , JSON.jstring "Angiosarcoma of Soft Tissue") ∷ ("meta" , JSON.jobject (("basicPropertyValues" , JSON.jarray (JSON.jobject (("pred" , JSON.jstring "http://www.geneontology.org/formats/oboInOwl#http://purl.obolibrary.org/obo/IAO_0000117") ∷ ("val" , JSON.jstring "NCI") ∷ []) ∷ [])) ∷ [])) ∷ []) ∷ [])) ∷ [])) ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/NCIT_C3088") ∷ ("lbl" , JSON.jstring "Angiosarcoma") ∷ ("type" , JSON.jstring "CLASS") ∷ ("meta" , JSON.jobject (("definition" , JSON.jobject (("val" , JSON.jstring "A malignant tumor arising from the endothelial cells of the blood vessels.  Microscopically, it is characterized by frequently open vascular anastomosing and branching channels.  The malignant cells that line the vascular channels are spindle or epithelioid and often display hyperchromatic nuclei.  Angiosarcomas most frequently occur in the skin and breast.  Patients with long-standing lymphedema are at increased risk of developing angiosarcoma.") ∷ ("meta" , JSON.jobject (("basicPropertyValues" , JSON.jarray (JSON.jobject (("pred" , JSON.jstring "http://www.geneontology.org/formats/oboInOwl#http://purl.obolibrary.org/obo/IAO_0000119") ∷ ("val" , JSON.jstring "NCI") ∷ []) ∷ [])) ∷ [])) ∷ [])) ∷ ("synonyms" , JSON.jarray (JSON.jobject (("pred" , JSON.jstring "hasExactSynonym") ∷ ("val" , JSON.jstring "Angiosarcoma") ∷ ("meta" , JSON.jobject (("basicPropertyValues" , JSON.jarray (JSON.jobject (("pred" , JSON.jstring "http://www.geneontology.org/formats/oboInOwl#http://purl.obolibrary.org/obo/IAO_0000117") ∷ ("val" , JSON.jstring "NCI") ∷ []) ∷ [])) ∷ [])) ∷ []) ∷ JSON.jobject (("pred" , JSON.jstring "hasExactSynonym") ∷ ("val" , JSON.jstring "HEMANGIOSARCOMA, MALIGNANT") ∷ ("meta" , JSON.jobject (("basicPropertyValues" , JSON.jarray (JSON.jobject (("pred" , JSON.jstring "http://www.geneontology.org/formats/oboInOwl#http://purl.obolibrary.org/obo/IAO_0000117") ∷ ("val" , JSON.jstring "CDISC") ∷ []) ∷ [])) ∷ [])) ∷ []) ∷ JSON.jobject (("pred" , JSON.jstring "hasExactSynonym") ∷ ("val" , JSON.jstring "Hemangiosarcoma") ∷ ("meta" , JSON.jobject (("basicPropertyValues" , JSON.jarray (JSON.jobject (("pred" , JSON.jstring "http://www.geneontology.org/formats/oboInOwl#http://purl.obolibrary.org/obo/IAO_0000117") ∷ ("val" , JSON.jstring "CDISC") ∷ []) ∷ [])) ∷ [])) ∷ []) ∷ JSON.jobject (("pred" , JSON.jstring "hasExactSynonym") ∷ ("val" , JSON.jstring "Hemangiosarcoma") ∷ ("meta" , JSON.jobject (("basicPropertyValues" , JSON.jarray (JSON.jobject (("pred" , JSON.jstring "http://www.geneontology.org/formats/oboInOwl#http://purl.obolibrary.org/obo/IAO_0000117") ∷ ("val" , JSON.jstring "NCI") ∷ []) ∷ [])) ∷ [])) ∷ []) ∷ JSON.jobject (("pred" , JSON.jstring "hasExactSynonym") ∷ ("val" , JSON.jstring "Malignant Angioendothelioma") ∷ ("meta" , JSON.jobject (("basicPropertyValues" , JSON.jarray (JSON.jobject (("pred" , JSON.jstring "http://www.geneontology.org/formats/oboInOwl#http://purl.obolibrary.org/obo/IAO_0000117") ∷ ("val" , JSON.jstring "NCI") ∷ []) ∷ [])) ∷ [])) ∷ []) ∷ JSON.jobject (("pred" , JSON.jstring "hasExactSynonym") ∷ ("val" , JSON.jstring "Malignant Hemangioendothelioma") ∷ ("meta" , JSON.jobject (("basicPropertyValues" , JSON.jarray (JSON.jobject (("pred" , JSON.jstring "http://www.geneontology.org/formats/oboInOwl#http://purl.obolibrary.org/obo/IAO_0000117") ∷ ("val" , JSON.jstring "NCI") ∷ []) ∷ [])) ∷ [])) ∷ []) ∷ JSON.jobject (("pred" , JSON.jstring "hasExactSynonym") ∷ ("val" , JSON.jstring "angiosarcoma") ∷ ("meta" , JSON.jobject (("basicPropertyValues" , JSON.jarray (JSON.jobject (("pred" , JSON.jstring "http://www.geneontology.org/formats/oboInOwl#http://purl.obolibrary.org/obo/IAO_0000117") ∷ ("val" , JSON.jstring "NCI-GLOSS") ∷ []) ∷ [])) ∷ [])) ∷ []) ∷ JSON.jobject (("pred" , JSON.jstring "hasExactSynonym") ∷ ("val" , JSON.jstring "hemangiosarcoma") ∷ ("meta" , JSON.jobject (("basicPropertyValues" , JSON.jarray (JSON.jobject (("pred" , JSON.jstring "http://www.geneontology.org/formats/oboInOwl#http://purl.obolibrary.org/obo/IAO_0000117") ∷ ("val" , JSON.jstring "NCI-GLOSS") ∷ []) ∷ [])) ∷ [])) ∷ []) ∷ [])) ∷ [])) ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/Orphanet_263413") ∷ ("lbl" , JSON.jstring "Angiosarcoma") ∷ ("type" , JSON.jstring "CLASS") ∷ ("meta" , JSON.jobject (("subsets" , JSON.jarray (JSON.jstring "http://purl.obolibrary.org/obo/Orphanet_377788" ∷ [])) ∷ ("xrefs" , JSON.jarray (JSON.jobject (("val" , JSON.jstring "MedDRA:10002476") ∷ []) ∷ [])) ∷ [])) ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://purl.obolibrary.org/obo/IAO_0000115") ∷ ("lbl" , JSON.jstring "definition") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "ANNOTATION") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://www.geneontology.org/formats/oboInOwl#comments") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "ANNOTATION") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://www.geneontology.org/formats/oboInOwl#confidence") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "ANNOTATION") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://www.geneontology.org/formats/oboInOwl#hasAlternativeId") ∷ ("lbl" , JSON.jstring "has_alternative_id") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "ANNOTATION") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://www.geneontology.org/formats/oboInOwl#hasDbXref") ∷ ("lbl" , JSON.jstring "database_cross_reference") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "ANNOTATION") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://www.geneontology.org/formats/oboInOwl#hasExactSynonym") ∷ ("lbl" , JSON.jstring "has_exact_synonym") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "ANNOTATION") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://www.geneontology.org/formats/oboInOwl#id") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "ANNOTATION") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://www.geneontology.org/formats/oboInOwl#inSubset") ∷ ("lbl" , JSON.jstring "in_subset") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "ANNOTATION") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://www.geneontology.org/formats/oboInOwl#source") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "ANNOTATION") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://www.geneontology.org/formats/oboInOwl#http://purl.obolibrary.org/obo/IAO_0000117") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "ANNOTATION") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://www.geneontology.org/formats/oboInOwl#http://purl.obolibrary.org/obo/IAO_0000119") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "ANNOTATION") ∷ []) ∷ JSON.jobject (("id" , JSON.jstring "http://www.w3.org/2000/01/rdf-schema#label") ∷ ("type" , JSON.jstring "PROPERTY") ∷ ("propertyType" , JSON.jstring "ANNOTATION") ∷ []) ∷ [])) ∷ ("edges" , JSON.jarray (JSON.jobject (("sub" , JSON.jstring "http://purl.obolibrary.org/obo/DOID_0001816") ∷ ("pred" , JSON.jstring "is_a") ∷ ("obj" , JSON.jstring "http://purl.obolibrary.org/obo/DOID_1115") ∷ []) ∷ JSON.jobject (("sub" , JSON.jstring "http://purl.obolibrary.org/obo/NCIT_C121671") ∷ ("pred" , JSON.jstring "is_a") ∷ ("obj" , JSON.jstring "http://purl.obolibrary.org/obo/NCIT_C3088") ∷ []) ∷ JSON.jobject (("sub" , JSON.jstring "http://purl.obolibrary.org/obo/NCIT_C121671") ∷ ("pred" , JSON.jstring "is_a") ∷ ("obj" , JSON.jstring "http://purl.obolibrary.org/obo/NCIT_C9306") ∷ []) ∷ JSON.jobject (("sub" , JSON.jstring "http://purl.obolibrary.org/obo/NCIT_C3088") ∷ ("pred" , JSON.jstring "is_a") ∷ ("obj" , JSON.jstring "http://purl.obolibrary.org/obo/NCIT_C8538") ∷ []) ∷ JSON.jobject (("sub" , JSON.jstring "http://purl.obolibrary.org/obo/NCIT_C3088") ∷ ("pred" , JSON.jstring "is_a") ∷ ("obj" , JSON.jstring "http://purl.obolibrary.org/obo/NCIT_C9118") ∷ []) ∷ JSON.jobject (("sub" , JSON.jstring "http://purl.obolibrary.org/obo/Orphanet_263413") ∷ ("pred" , JSON.jstring "is_a") ∷ ("obj" , JSON.jstring "http://purl.obolibrary.org/obo/Orphanet_3394") ∷ ("meta" , JSON.jobject (("basicPropertyValues" , JSON.jarray (JSON.jobject (("pred" , JSON.jstring "http://www.geneontology.org/formats/oboInOwl#comments") ∷ ("val" , JSON.jstring "test comments") ∷ []) ∷ JSON.jobject (("pred" , JSON.jstring "http://www.geneontology.org/formats/oboInOwl#source") ∷ ("val" , JSON.jstring "Orphanet") ∷ []) ∷ [])) ∷ [])) ∷ []) ∷ [])) ∷ ("equivalentNodesSets" , JSON.jarray (JSON.jobject (("representativeNodeId" , JSON.jstring "http://purl.obolibrary.org/obo/DOID_0001816") ∷ ("nodeIds" , JSON.jarray (JSON.jstring "http://purl.obolibrary.org/obo/DOID_0001816" ∷ JSON.jstring "http://purl.obolibrary.org/obo/NCIT_C3088" ∷ [])) ∷ ("meta" , JSON.jobject (("basicPropertyValues" , JSON.jarray (JSON.jobject (("pred" , JSON.jstring "http://www.geneontology.org/formats/oboInOwl#comments") ∷ ("val" , JSON.jstring "foo bar") ∷ []) ∷ JSON.jobject (("pred" , JSON.jstring "http://www.geneontology.org/formats/oboInOwl#confidence") ∷ ("val" , JSON.jstring "0.8") ∷ []) ∷ [])) ∷ [])) ∷ []) ∷ JSON.jobject (("representativeNodeId" , JSON.jstring "http://purl.obolibrary.org/obo/DOID_0001816") ∷ ("nodeIds" , JSON.jarray (JSON.jstring "http://purl.obolibrary.org/obo/DOID_0001816" ∷ JSON.jstring "http://purl.obolibrary.org/obo/Orphanet_263413" ∷ [])) ∷ []) ∷ [])) ∷ []) ∷ [])) ∷ [])

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

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


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

graphDocument : OG.GraphDocument
graphDocument =
  Decode.fromMaybe (OG.graphDocument []) decodedGraphDocument

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

ontologyDocument : P.OntologyDocument
ontologyDocument =
  OGP.toOntologyDocument graphDocument