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

module OWL2.Examples.Portable.SemanticSupport where

open import OWL2.Prelude
import OWL2.Check.Result as CheckResult
import OWL2.Portable.Check.SemanticSupport as CheckSemantic
import OWL2.Portable.Semantics as Sem
import OWL2.Portable.Syntax as P

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

className : String → P.ClassName
className =
  name

axiom : P.Axiom → P.Annotated P.Axiom
axiom body =
  P.annotated [] body

document : List (P.Annotated P.Axiom) → P.OntologyDocument
document axioms =
  P.ontologyDocument [] (P.ontology P.anonymousOntology [] [] axioms)

person employee : P.ClassName
person =
  className "https://example.org/portable-semantic-support#Person"
employee =
  className "https://example.org/portable-semantic-support#Employee"

cleanAxiom : P.Annotated P.Axiom
cleanAxiom =
  axiom
    (P.subClassOf
      (P.namedClass employee)
      (P.namedClass person))

cleanDocument : P.OntologyDocument
cleanDocument =
  document (cleanAxiom ∷ [])

cleanCheckResult : CheckSemantic.SemanticSupportCheckResult
cleanCheckResult =
  CheckSemantic.checkSemanticSupport cleanDocument

cleanCheckDiagnostics :
  CheckResult.diagnostics cleanCheckResult ≡ []
cleanCheckDiagnostics =
  refl

cleanCheckClean :
  CheckResult.clean? cleanCheckResult ≡ true
cleanCheckClean =
  refl

cleanCheckEvidence :
  CheckSemantic.SemanticSupportEvidence cleanDocument
cleanCheckEvidence =
  CheckSemantic.semanticSupportEvidenceFromClean cleanDocument tt

cleanCompleteTranslation :
  Sem.CompleteSemanticTranslation cleanDocument
cleanCompleteTranslation =
  CheckSemantic.completeSemanticTranslationFromClean cleanDocument tt

syntheticUnsupportedAxiom : P.Annotated P.Axiom
syntheticUnsupportedAxiom =
  axiom
    (P.subClassOf
      (P.namedClass person)
      (P.namedClass employee))

syntheticUnsupportedDiagnostics :
  CheckSemantic.unsupportedSemanticAxiomDiagnostics
    (syntheticUnsupportedAxiom ∷ []) ≡
  CheckSemantic.unsupportedSemanticAxiomDiagnostic
    syntheticUnsupportedAxiom
  ∷ []
syntheticUnsupportedDiagnostics =
  refl