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

module OWL2.Examples.OBOGraph.Json.Showcase where

open import OWL2.Prelude
import FF.Json.Native as JSON
import OWL2.OBOGraph.Schema as Schema
import OWL2.OBOGraph.Syntax as OG
import OWL2.Portable.Syntax as P

import OWL2.Examples.OBOGraph.Json.ABox as ABox
import OWL2.Examples.OBOGraph.Json.EquivNodeSetTest as EquivNodeSetTest
import OWL2.Examples.OBOGraph.Json.LogicalDefinitionTest as LogicalDefinitionTest
import OWL2.Examples.OBOGraph.Json.Nucleus as Nucleus
import OWL2.Examples.OBOGraph.Json.ObsoletionExample as ObsoletionExample
import OWL2.Examples.OBOGraph.Json.PropertyChainAllValues as PropertyChainAllValues
import OWL2.Examples.OBOGraph.Json.RO as RO
import OWL2.Examples.OBOGraph.Json.ROCore as ROCore
import OWL2.Examples.OBOGraph.Json.SYMP as SYMP
import OWL2.Examples.OBOGraph.Json.UO as UO

record JsonImportedOntology : Type₀ where
  constructor jsonImportedOntology
  field
    sourceFile       : String
    jsonValue        : JSON.JsonValue
    jsonDiagnostics  : List Schema.SchemaDiagnostic
    graphDocument    : OG.GraphDocument
    ontologyDocument : P.OntologyDocument

open JsonImportedOntology public

abox : JsonImportedOntology
abox =
  jsonImportedOntology
    ABox.sourceJson
    ABox.jsonValue
    ABox.jsonDiagnostics
    ABox.graphDocument
    ABox.ontologyDocument

equivNodeSetTest : JsonImportedOntology
equivNodeSetTest =
  jsonImportedOntology
    EquivNodeSetTest.sourceJson
    EquivNodeSetTest.jsonValue
    EquivNodeSetTest.jsonDiagnostics
    EquivNodeSetTest.graphDocument
    EquivNodeSetTest.ontologyDocument

logicalDefinitionTest : JsonImportedOntology
logicalDefinitionTest =
  jsonImportedOntology
    LogicalDefinitionTest.sourceJson
    LogicalDefinitionTest.jsonValue
    LogicalDefinitionTest.jsonDiagnostics
    LogicalDefinitionTest.graphDocument
    LogicalDefinitionTest.ontologyDocument

nucleus : JsonImportedOntology
nucleus =
  jsonImportedOntology
    Nucleus.sourceJson
    Nucleus.jsonValue
    Nucleus.jsonDiagnostics
    Nucleus.graphDocument
    Nucleus.ontologyDocument

obsoletionExample : JsonImportedOntology
obsoletionExample =
  jsonImportedOntology
    ObsoletionExample.sourceJson
    ObsoletionExample.jsonValue
    ObsoletionExample.jsonDiagnostics
    ObsoletionExample.graphDocument
    ObsoletionExample.ontologyDocument

propertyChainAllValues : JsonImportedOntology
propertyChainAllValues =
  jsonImportedOntology
    PropertyChainAllValues.sourceJson
    PropertyChainAllValues.jsonValue
    PropertyChainAllValues.jsonDiagnostics
    PropertyChainAllValues.graphDocument
    PropertyChainAllValues.ontologyDocument

ro : JsonImportedOntology
ro =
  jsonImportedOntology
    RO.sourceJson
    RO.jsonValue
    RO.jsonDiagnostics
    RO.graphDocument
    RO.ontologyDocument

roCore : JsonImportedOntology
roCore =
  jsonImportedOntology
    ROCore.sourceJson
    ROCore.jsonValue
    ROCore.jsonDiagnostics
    ROCore.graphDocument
    ROCore.ontologyDocument

symp : JsonImportedOntology
symp =
  jsonImportedOntology
    SYMP.sourceJson
    SYMP.jsonValue
    SYMP.jsonDiagnostics
    SYMP.graphDocument
    SYMP.ontologyDocument

uo : JsonImportedOntology
uo =
  jsonImportedOntology
    UO.sourceJson
    UO.jsonValue
    UO.jsonDiagnostics
    UO.graphDocument
    UO.ontologyDocument

jsonImportedOntologies : List JsonImportedOntology
jsonImportedOntologies =
  abox ∷
  equivNodeSetTest ∷
  logicalDefinitionTest ∷
  nucleus ∷
  obsoletionExample ∷
  propertyChainAllValues ∷
  ro ∷
  roCore ∷
  symp ∷
  uo ∷
  []

jsonValues : List JSON.JsonValue
jsonValues =
  ABox.jsonValue ∷
  EquivNodeSetTest.jsonValue ∷
  LogicalDefinitionTest.jsonValue ∷
  Nucleus.jsonValue ∷
  ObsoletionExample.jsonValue ∷
  PropertyChainAllValues.jsonValue ∷
  RO.jsonValue ∷
  ROCore.jsonValue ∷
  SYMP.jsonValue ∷
  UO.jsonValue ∷
  []

portableOntologyDocuments : List P.OntologyDocument
portableOntologyDocuments =
  ABox.ontologyDocument ∷
  EquivNodeSetTest.ontologyDocument ∷
  LogicalDefinitionTest.ontologyDocument ∷
  Nucleus.ontologyDocument ∷
  ObsoletionExample.ontologyDocument ∷
  PropertyChainAllValues.ontologyDocument ∷
  RO.ontologyDocument ∷
  ROCore.ontologyDocument ∷
  SYMP.ontologyDocument ∷
  UO.ontologyDocument ∷
  []