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

module OWL2.Portable.Check.SemanticSupport where

open import OWL2.Prelude
open import OWL2.Check.Result
open import OWL2.Diagnostics
import OWL2.DirectSemantics as D
import OWL2.Portable.Check.Core as Core
import OWL2.Portable.Semantics as Semantics
import OWL2.Portable.Syntax as P

record SemanticSupportEvidence
  (document : P.OntologyDocument)
  : Type₀ where
  constructor semanticSupportEvidence
  field
    sourceDocument :
      P.OntologyDocument
    sourcePreserved :
      sourceDocument ≡ document
    translation :
      Semantics.SemanticTranslation
    unsupportedAxioms :
      List (P.Annotated P.Axiom)

open SemanticSupportEvidence public

record SemanticSupportCheckMeaning
  (document : P.OntologyDocument)
  (evidence : SemanticSupportEvidence document)
  : Type₀ where
  constructor semanticSupportCheckMeaning
  field
    semanticSupportSourcePreserved :
      sourceDocument evidence ≡ document
    semanticTranslationRecorded :
      translation evidence ≡
      Semantics.partialTranslateOntologyDocument document
    unsupportedAxiomsRecorded :
      unsupportedAxioms evidence ≡
      Semantics.unsupported (translation evidence)

open SemanticSupportCheckMeaning public

SemanticSupportCheckResult : Type₀
SemanticSupportCheckResult =
  CheckResult
    P.OntologyDocument
    SemanticSupportEvidence
    SemanticSupportCheckMeaning

semanticSupportDiagnosticNamespace : String
semanticSupportDiagnosticNamespace =
  "owl2.portable.semanticSupport"

unsupportedSemanticAxiomCode : DiagnosticCode
unsupportedSemanticAxiomCode =
  mkDiagnosticCode
    semanticSupportDiagnosticNamespace
    "unsupportedSemanticAxiom"

unsupportedSemanticAxiomDiagnostic :
  P.Annotated P.Axiom →
  Diagnostic
unsupportedSemanticAxiomDiagnostic axiom =
  diagnostic
    unsupportedSemanticAxiomCode
    severityError
    rootSourcePath
    "axiom is outside the current portable Direct Semantics translation"

unsupportedSemanticAxiomDiagnostics :
  List (P.Annotated P.Axiom) →
  Diagnostics
unsupportedSemanticAxiomDiagnostics [] =
  []
unsupportedSemanticAxiomDiagnostics (axiom ∷ axioms) =
  unsupportedSemanticAxiomDiagnostic axiom
  ∷ unsupportedSemanticAxiomDiagnostics axioms

semanticSupportDiagnostics : P.OntologyDocument → Diagnostics
semanticSupportDiagnostics document =
  unsupportedSemanticAxiomDiagnostics
    (Semantics.unsupported
      (Semantics.partialTranslateOntologyDocument document))

semanticSupportEvidenceFor :
  (document : P.OntologyDocument) →
  SemanticSupportEvidence document
semanticSupportEvidenceFor document =
  semanticSupportEvidence
    document
    refl
    (Semantics.partialTranslateOntologyDocument document)
    (Semantics.unsupported (Semantics.partialTranslateOntologyDocument document))

semanticSupportMeaningFor :
  (document : P.OntologyDocument) →
  (evidence : SemanticSupportEvidence document) →
  sourceDocument evidence ≡ document →
  translation evidence ≡
    Semantics.partialTranslateOntologyDocument document →
  unsupportedAxioms evidence ≡
    Semantics.unsupported (translation evidence) →
  SemanticSupportCheckMeaning document evidence
semanticSupportMeaningFor document evidence preserved translated unsupported =
  semanticSupportCheckMeaning preserved translated unsupported

checkSemanticSupport :
  P.OntologyDocument →
  SemanticSupportCheckResult
checkSemanticSupport document =
  Core.successfulResultWithDiagnostics
    (semanticSupportDiagnostics document)
    document
    evidence
    (semanticSupportMeaningFor document evidence refl refl refl)
  where
  evidence : SemanticSupportEvidence document
  evidence =
    semanticSupportEvidenceFor document

completeSemanticTranslationFromDiagnostics :
  (unsupported : List (P.Annotated P.Axiom)) →
  CleanDiagnostics (unsupportedSemanticAxiomDiagnostics unsupported) →
  unsupported ≡ []
completeSemanticTranslationFromDiagnostics [] clean =
  refl
completeSemanticTranslationFromDiagnostics (axiom ∷ unsupported) ()

semanticSupportEvidenceFromClean :
  (document : P.OntologyDocument) →
  Clean (checkSemanticSupport document) →
  SemanticSupportEvidence document
semanticSupportEvidenceFromClean document clean =
  evidenceFromClean (checkSemanticSupport document) clean

semanticSupportSoundFromClean :
  (document : P.OntologyDocument) →
  (clean : Clean (checkSemanticSupport document)) →
  SemanticSupportCheckMeaning
    document
    (semanticSupportEvidenceFromClean document clean)
semanticSupportSoundFromClean document clean =
  soundFromClean (checkSemanticSupport document) clean

completeSemanticTranslationFromClean :
  (document : P.OntologyDocument) →
  Clean (checkSemanticSupport document) →
  Semantics.CompleteSemanticTranslation document
completeSemanticTranslationFromClean document clean =
  completeSemanticTranslationFromDiagnostics
    (Semantics.unsupported (Semantics.partialTranslateOntologyDocument document))
    clean

ModelOfCompletePortableDocument :
  ∀ {ℓObj ℓData ℓSem} →
  (document : P.OntologyDocument) →
  Clean (checkSemanticSupport document) →
  D.Interpretation Semantics.PortableSignature ℓObj ℓData ℓSem →
  Type (D.SemLevel ℓ-zero ℓObj ℓData ℓSem)
ModelOfCompletePortableDocument document clean interpretation =
  Semantics.PartialModel interpretation document

record CompletePortableDocumentModel
  {ℓObj ℓData ℓSem}
  (document : P.OntologyDocument)
  (clean : Clean (checkSemanticSupport document))
  : Type (ℓ-suc (D.SemLevel ℓ-zero ℓObj ℓData ℓSem)) where
  constructor completePortableDocumentModel
  field
    completePortableInterpretation :
      D.Interpretation Semantics.PortableSignature ℓObj ℓData ℓSem
    completePortableSatisfies :
      ModelOfCompletePortableDocument
        document
        clean
        completePortableInterpretation

open CompletePortableDocumentModel public