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

module OWL2.Semantics.ImportProject.Legacy where

open import OWL2.Prelude
open import OWL2.Check.Bundle
open import OWL2.Check.Result
open import OWL2.Elab.CheckedImport
open import OWL2.Elab.ImportProject
open import OWL2.Elab.Policy
open import OWL2.Elab.SymbolTable using (symbolTableSignature)
open import OWL2.Raw
open import OWL2.Semantics.Complete
open import OWL2.Semantics.ImportProject
import OWL2.Kernel as K
import OWL2.Kernel.Semantics as KS

ProjectDocumentSemanticSupport :
  ∀ {policy sources} →
  CheckedProjectDocuments policy sources → Type₀
ProjectDocumentSemanticSupport checkedProjectDocuments[] =
  Unit
ProjectDocumentSemanticSupport
  (checkedProjectDocuments∷ document documents) =
  CheckedEvidence (projectDocumentChecked document) semanticSupportEvidence ×
  ProjectDocumentSemanticSupport documents

ProjectDocumentInterpretations :
  ∀ {policy sources} →
  CheckedProjectDocuments policy sources → Type₁
ProjectDocumentInterpretations checkedProjectDocuments[] =
  Lift (ℓ-suc ℓ-zero) Unit
ProjectDocumentInterpretations
  (checkedProjectDocuments∷ document documents) =
  KS.Interpretation (signature (projectDocumentChecked document)) ×
  ProjectDocumentInterpretations documents

ModelOfCheckedProjectDocuments :
  ∀ {policy sources} →
  (documents : CheckedProjectDocuments policy sources) →
  ProjectDocumentSemanticSupport documents →
  ProjectDocumentInterpretations documents →
  Type₀
ModelOfCheckedProjectDocuments checkedProjectDocuments[] tt (lift tt) =
  Unit
ModelOfCheckedProjectDocuments
  (checkedProjectDocuments∷ document documents)
  (support , supports)
  (interpretation , interpretations) =
  ModelOfCheckedImport
    (projectDocumentChecked document)
    support
    interpretation
  ×
  ModelOfCheckedProjectDocuments documents supports interpretations

completeProjectDocumentSemanticSupport :
  ∀ {policy sources} →
  (documents : CheckedProjectDocuments policy sources) →
  ProjectDocumentSemanticSupport documents
completeProjectDocumentSemanticSupport checkedProjectDocuments[] =
  tt
completeProjectDocumentSemanticSupport
  (checkedProjectDocuments∷ document documents) =
  sourceSemanticSupportEvidence
    (checkedSourceEvidenceOf (projectDocumentChecked document))
  ,
  completeProjectDocumentSemanticSupport documents

projectedOntologies :
  ∀ {policy project context}
    {checked : CheckedImportProject policy project} →
  CheckedImportProjectProjection checked context →
  List (K.Ontology (symbolTableSignature (projectSymbolTable project)))
projectedOntologies projection =
  projectedRootOntology projection ∷ projectedImportOntologies projection

projectedOntologiesAxioms :
  ∀ {Sig} →
  List (K.Ontology Sig) →
  List (K.Axiom Sig)
projectedOntologiesAxioms [] =
  []
projectedOntologiesAxioms (ont ∷ ontologies) =
  K.axioms ont ++ projectedOntologiesAxioms ontologies

projectedOntologiesPropertyChainFree :
  ∀ {Sig} →
  (ontologies : List (K.Ontology Sig)) →
  K.AxiomsPropertyChainFree (projectedOntologiesAxioms ontologies)
projectedOntologiesPropertyChainFree [] =
  tt
projectedOntologiesPropertyChainFree (ont ∷ ontologies) =
  K.axiomsPropertyChainFreeAppend
    (K.axioms ont)
    (projectedOntologiesAxioms ontologies)
    (K.propertyChainsFree (K.regularity ont))
    (projectedOntologiesPropertyChainFree ontologies)

mergedProjectedOntology :
  ∀ {policy project context}
    {checked : CheckedImportProject policy project} →
  CheckedImportProjectProjection checked context →
  K.Ontology (symbolTableSignature (projectSymbolTable project))
mergedProjectedOntology {context = context} projection =
  appendProjectedOntologies
    context
    (projectedRootOntology projection)
    (projectedImportOntologies projection)

ProjectedCheckedImportProjectInterpretation :
  ∀ {policy project} →
  CheckedImportProject policy project →
  Type₁
ProjectedCheckedImportProjectInterpretation {project = project} checked =
  KS.Interpretation (symbolTableSignature (projectSymbolTable project))

ModelOfProjectedCheckedImportProject :
  ∀ {policy project context} →
  {checked : CheckedImportProject policy project} →
  CheckedImportProjectProjection checked context →
  ProjectedCheckedImportProjectInterpretation checked →
  Type₀
ModelOfProjectedCheckedImportProject projection interpretation =
  ProjectedOntologiesSatisfy
    interpretation
    (projectedOntologies projection)

projectedCheckedModelToMergedOntology :
  ∀ {policy project context}
    {checked : CheckedImportProject policy project} →
  (projection : CheckedImportProjectProjection checked context) →
  (interpretation : ProjectedCheckedImportProjectInterpretation checked) →
  ModelOfProjectedCheckedImportProject projection interpretation →
  KS.SatisfiesOntology interpretation (mergedProjectedOntology projection)
projectedCheckedModelToMergedOntology {context = context} projection interpretation model =
  satisfiesProjectedOntologiesToMerged
    context
    interpretation
    (projectedRootOntology projection)
    (projectedImportOntologies projection)
    model

mergedOntologyToProjectedCheckedModel :
  ∀ {policy project context}
    {checked : CheckedImportProject policy project} →
  (projection : CheckedImportProjectProjection checked context) →
  (interpretation : ProjectedCheckedImportProjectInterpretation checked) →
  KS.SatisfiesOntology interpretation (mergedProjectedOntology projection) →
  ModelOfProjectedCheckedImportProject projection interpretation
mergedOntologyToProjectedCheckedModel {context = context} projection interpretation model =
  satisfiesMergedToProjectedOntologies
    context
    interpretation
    (projectedRootOntology projection)
    (projectedImportOntologies projection)
    model

record ProjectedCheckedImportProjectModel
  {policy : ImportPolicy}
  {project : RawImportProject}
  {context :
    K.RegularityContext (symbolTableSignature (projectSymbolTable project))}
  (checked : CheckedImportProject policy project)
  : Type₁ where
  constructor projectedCheckedImportProjectModel
  field
    projectedImportProject :
      CheckedImportProjectProjection checked context
    projectedInterpretation :
      ProjectedCheckedImportProjectInterpretation checked
    projectedSatisfies :
      ModelOfProjectedCheckedImportProject
        projectedImportProject
        projectedInterpretation

open ProjectedCheckedImportProjectModel public

record CheckedImportProjectSemantics
  {policy : ImportPolicy}
  {project : RawImportProject}
  (checked : CheckedImportProject policy project)
  : Type₁ where
  constructor checkedImportProjectSemantics
  field
    rootSemanticSupport :
      CheckedEvidence
        (projectDocumentChecked (checkedRootDocument checked))
        semanticSupportEvidence
    importSemanticSupport :
      ProjectDocumentSemanticSupport (checkedImportDocuments checked)
    rootInterpretation :
      KS.Interpretation
        (signature (projectDocumentChecked (checkedRootDocument checked)))
    importInterpretations :
      ProjectDocumentInterpretations (checkedImportDocuments checked)
    rootSatisfies :
      ModelOfCheckedImport
        (projectDocumentChecked (checkedRootDocument checked))
        rootSemanticSupport
        rootInterpretation
    importsSatisfy :
      ModelOfCheckedProjectDocuments
        (checkedImportDocuments checked)
        importSemanticSupport
        importInterpretations

open CheckedImportProjectSemantics public

CheckedImportProjectSemanticSupport :
  ∀ {policy project} →
  CheckedImportProject policy project → Type₀
CheckedImportProjectSemanticSupport checked =
  CheckedEvidence
    (projectDocumentChecked (checkedRootDocument checked))
    semanticSupportEvidence
  ×
  ProjectDocumentSemanticSupport (checkedImportDocuments checked)

CheckedImportProjectInterpretations :
  ∀ {policy project} →
  CheckedImportProject policy project → Type₁
CheckedImportProjectInterpretations checked =
  KS.Interpretation
    (signature (projectDocumentChecked (checkedRootDocument checked)))
  ×
  ProjectDocumentInterpretations (checkedImportDocuments checked)

ModelOfCheckedImportProject :
  ∀ {policy project} →
  (checked : CheckedImportProject policy project) →
  CheckedImportProjectSemanticSupport checked →
  CheckedImportProjectInterpretations checked →
  Type₀
ModelOfCheckedImportProject
  checked
  (rootSupport , importSupport)
  (rootInterpretation , importInterpretations) =
  ModelOfCheckedImport
    (projectDocumentChecked (checkedRootDocument checked))
    rootSupport
    rootInterpretation
  ×
  ModelOfCheckedProjectDocuments
    (checkedImportDocuments checked)
    importSupport
    importInterpretations

completeCheckedImportProjectSemanticSupport :
  ∀ {policy project} →
  (checked : CheckedImportProject policy project) →
  CheckedImportProjectSemanticSupport checked
completeCheckedImportProjectSemanticSupport checked =
  sourceSemanticSupportEvidence
    (checkedSourceEvidenceOf
      (projectDocumentChecked (checkedRootDocument checked)))
  ,
  completeProjectDocumentSemanticSupport
    (checkedImportDocuments checked)

ModelOfCompleteCheckedImportProject :
  ∀ {policy project} →
  (checked : CheckedImportProject policy project) →
  CheckedImportProjectInterpretations checked →
  Type₀
ModelOfCompleteCheckedImportProject checked interpretations =
  ModelOfCheckedImportProject
    checked
    (completeCheckedImportProjectSemanticSupport checked)
    interpretations

record CompleteCheckedImportProjectModel
  {policy : ImportPolicy}
  {project : RawImportProject}
  (checked : CheckedImportProject policy project)
  : Type₁ where
  constructor completeCheckedImportProjectModel
  field
    completeProjectInterpretations :
      CheckedImportProjectInterpretations checked
    completeProjectSatisfies :
      ModelOfCompleteCheckedImportProject
        checked
        completeProjectInterpretations

open CompleteCheckedImportProjectModel public

checkedImportProjectFromResultClean :
  ∀ {policy} →
  (result : CheckedImportProjectElaborationResult policy) →
  Clean result →
  CheckedImportProject policy (input result)
checkedImportProjectFromResultClean result clean =
  evidenceFromClean result clean

checkedImportProjectSoundFromResultClean :
  ∀ {policy} →
  (result : CheckedImportProjectElaborationResult policy) →
  (clean : Clean result) →
  ElaboratesToCheckedImportProject
    policy
    (input result)
    (checkedImportProjectFromResultClean result clean)
checkedImportProjectSoundFromResultClean result clean =
  soundFromClean result clean