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

module OWL2.Semantics.Complete where

open import OWL2.Prelude
open import OWL2.Check.Bundle
open import OWL2.Check.Result
open import OWL2.Elab.CheckedImport
open import OWL2.Elab.Result
import OWL2.Kernel.Semantics as KS

ModelOfCheckedImport :
  (checked : CheckedImport) →
  CheckedEvidence checked semanticSupportEvidence →
  KS.Interpretation (signature checked) →
  Type₀
ModelOfCheckedImport checked semanticSupport I =
  KS.SatisfiesOntology I (ontology checked)

ModelOfCompleteCheckedImport :
  (checked : CheckedImport) →
  CheckedSourceEvidence checked →
  KS.Interpretation (signature checked) →
  Type₀
ModelOfCompleteCheckedImport checked sourceEvidence I =
  ModelOfCheckedImport
    checked
    (sourceSemanticSupportEvidence sourceEvidence)
    I

record CheckedImportModel (checked : CheckedImport) : Type₁ where
  constructor checkedImportModel
  field
    semanticSupport :
      CheckedEvidence checked semanticSupportEvidence
    interpretation :
      KS.Interpretation (signature checked)
    satisfies :
      ModelOfCheckedImport checked semanticSupport interpretation

open CheckedImportModel public

record CompleteCheckedImportModel (checked : CheckedImport) : Type₁ where
  constructor completeCheckedImportModel
  field
    completeSourceEvidence :
      CheckedSourceEvidence checked
    completeInterpretation :
      KS.Interpretation (signature checked)
    completeSatisfies :
      ModelOfCompleteCheckedImport
        checked
        completeSourceEvidence
        completeInterpretation

open CompleteCheckedImportModel public

checkedFromClean :
  (result : ElaborationResult) →
  Clean result →
  CheckedImport
checkedFromClean result clean =
  evidenceFromClean result clean

sourceEvidenceFromClean :
  (result : ElaborationResult) →
  (clean : Clean result) →
  CheckedSourceEvidence (checkedFromClean result clean)
sourceEvidenceFromClean result clean =
  checkedSourceEvidenceOf (checkedFromClean result clean)

completeSourceSound :
  (result : ElaborationResult) →
  (clean : Clean result) →
  ElaboratesToCheckedImport
    (input result)
    (checkedFromClean result clean)
completeSourceSound result clean =
  soundFromClean result clean

ModelOfCompleteSource :
  (result : ElaborationResult) →
  (clean : Clean result) →
  KS.Interpretation (signature (checkedFromClean result clean)) →
  Type₀
ModelOfCompleteSource result clean I =
  ModelOfCompleteCheckedImport
    (checkedFromClean result clean)
    (sourceEvidenceFromClean result clean)
    I

record CompleteSourceModel
  (result : ElaborationResult)
  (clean : Clean result)
  : Type₁ where
  constructor completeSourceModel
  field
    sourceInterpretation :
      KS.Interpretation (signature (checkedFromClean result clean))
    sourceSatisfies :
      ModelOfCompleteSource result clean sourceInterpretation

open CompleteSourceModel public

ModelOfElaboratedSource :
  (result : ElaborationResult) →
  (evidence : EvidenceAvailable result) →
  CheckedEvidence (elaborationSucceeded result evidence) semanticSupportEvidence →
  KS.Interpretation (signature (elaborationSucceeded result evidence)) →
  Type₀
ModelOfElaboratedSource result evidence semanticSupport I =
  ModelOfCheckedImport
    (elaborationSucceeded result evidence)
    semanticSupport
    I