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

module OWL2.Semantics.ImportProject where

open import OWL2.Prelude
open import OWL2.Check.Result
open import OWL2.Elab.ImportProject
open import OWL2.Elab.CheckedImport
open import OWL2.Elab.Policy
open import OWL2.Foundation.List using (allAppend; allAppendLeft; allAppendRight)
open import OWL2.Raw
open import OWL2.Semantics.Complete
import OWL2.Kernel as K
import OWL2.Kernel.Semantics as KS

ProjectedOntologiesSatisfy :
  ∀ {Sig} →
  KS.Interpretation Sig →
  List (K.Ontology Sig) →
  Type₀
ProjectedOntologiesSatisfy interpretation [] =
  Unit
ProjectedOntologiesSatisfy interpretation (ont ∷ ontologies) =
  KS.SatisfiesOntology interpretation ont ×
  ProjectedOntologiesSatisfy interpretation ontologies

satisfiesProjectedOntologiesToMerged :
  ∀ {Sig} →
  (context : K.RegularityContext Sig) →
  (interpretation : KS.Interpretation Sig) →
  (root : K.Ontology Sig) →
  (imports : List (K.Ontology Sig)) →
  ProjectedOntologiesSatisfy interpretation (root ∷ imports) →
  KS.SatisfiesOntology
    interpretation
    (appendProjectedOntologies context root imports)
satisfiesProjectedOntologiesToMerged
  context
  interpretation
  root
  []
  (rootSatisfies , tt) =
  rootSatisfies
satisfiesProjectedOntologiesToMerged
  context
  interpretation
  root
  (ont ∷ ontologies)
  (rootSatisfies , importsSatisfy) =
  allAppend
    rootSatisfies
    (satisfiesProjectedOntologiesToMerged
      context
      interpretation
      ont
      ontologies
      importsSatisfy)

satisfiesMergedToProjectedOntologies :
  ∀ {Sig} →
  (context : K.RegularityContext Sig) →
  (interpretation : KS.Interpretation Sig) →
  (root : K.Ontology Sig) →
  (imports : List (K.Ontology Sig)) →
  KS.SatisfiesOntology
    interpretation
    (appendProjectedOntologies context root imports) →
  ProjectedOntologiesSatisfy interpretation (root ∷ imports)
satisfiesMergedToProjectedOntologies context interpretation root [] mergedSatisfies =
  mergedSatisfies , tt
satisfiesMergedToProjectedOntologies
  context
  interpretation
  root
  (ont ∷ ontologies)
  mergedSatisfies =
  allAppendLeft mergedSatisfies
  ,
  satisfiesMergedToProjectedOntologies
    context
    interpretation
    ont
    ontologies
    (allAppendRight mergedSatisfies)

ProjectScopedImportProjectInterpretation :
  ∀ {policy project} →
  ProjectScopedImportProject policy project →
  Type₁
ProjectScopedImportProjectInterpretation scoped =
  KS.Interpretation (signature (importProjectCheckedImport scoped))

ModelOfProjectScopedImportProject :
  ∀ {policy project} →
  (scoped : ProjectScopedImportProject policy project) →
  ProjectScopedImportProjectInterpretation scoped →
  Type₀
ModelOfProjectScopedImportProject scoped interpretation =
  ProjectedOntologiesSatisfy
    interpretation
    (importProjectOntologies scoped)

projectScopedModelToMergedOntology :
  ∀ {policy project} →
  (scoped : ProjectScopedImportProject policy project) →
  (interpretation : ProjectScopedImportProjectInterpretation scoped) →
  ModelOfProjectScopedImportProject scoped interpretation →
  KS.SatisfiesOntology interpretation (importProjectMergedOntology scoped)
projectScopedModelToMergedOntology scoped interpretation model =
  subst
    (KS.SatisfiesOntology interpretation)
    (importProjectProjectedOntologyIsMerged scoped)
    (satisfiesProjectedOntologiesToMerged
      (importProjectProjectionContext scoped)
      interpretation
      (importProjectRootOntology scoped)
      (importProjectImportOntologies scoped)
      model)

mergedOntologyToProjectScopedModel :
  ∀ {policy project} →
  (scoped : ProjectScopedImportProject policy project) →
  (interpretation : ProjectScopedImportProjectInterpretation scoped) →
  KS.SatisfiesOntology interpretation (importProjectMergedOntology scoped) →
  ModelOfProjectScopedImportProject scoped interpretation
mergedOntologyToProjectScopedModel scoped interpretation model =
  satisfiesMergedToProjectedOntologies
    (importProjectProjectionContext scoped)
    interpretation
    (importProjectRootOntology scoped)
    (importProjectImportOntologies scoped)
    (subst
      (KS.SatisfiesOntology interpretation)
      (sym (importProjectProjectedOntologyIsMerged scoped))
      model)

record ProjectScopedImportProjectModel
  {policy : ImportPolicy}
  {project : RawImportProject}
  (scoped : ProjectScopedImportProject policy project)
  : Type₁ where
  constructor projectScopedImportProjectModel
  field
    projectScopedInterpretation :
      ProjectScopedImportProjectInterpretation scoped
    projectScopedSatisfies :
      ModelOfProjectScopedImportProject
        scoped
        projectScopedInterpretation

open ProjectScopedImportProjectModel public

ImportProjectInterpretation :
  ∀ {policy project} →
  ProjectScopedImportProject policy project →
  Type₁
ImportProjectInterpretation =
  ProjectScopedImportProjectInterpretation

ModelOfImportProject :
  ∀ {policy project} →
  (scoped : ProjectScopedImportProject policy project) →
  ImportProjectInterpretation scoped →
  Type₀
ModelOfImportProject =
  ModelOfProjectScopedImportProject

importProjectModelToMergedOntology :
  ∀ {policy project} →
  (scoped : ProjectScopedImportProject policy project) →
  (interpretation : ImportProjectInterpretation scoped) →
  ModelOfImportProject scoped interpretation →
  KS.SatisfiesOntology interpretation (importProjectMergedOntology scoped)
importProjectModelToMergedOntology =
  projectScopedModelToMergedOntology

mergedOntologyToImportProjectModel :
  ∀ {policy project} →
  (scoped : ProjectScopedImportProject policy project) →
  (interpretation : ImportProjectInterpretation scoped) →
  KS.SatisfiesOntology interpretation (importProjectMergedOntology scoped) →
  ModelOfImportProject scoped interpretation
mergedOntologyToImportProjectModel =
  mergedOntologyToProjectScopedModel

record ImportProjectModel
  {policy : ImportPolicy}
  {project : RawImportProject}
  (scoped : ProjectScopedImportProject policy project)
  : Type₁ where
  constructor importProjectModel
  field
    importProjectInterpretation :
      ImportProjectInterpretation scoped
    importProjectSatisfies :
      ModelOfImportProject
        scoped
        importProjectInterpretation

open ImportProjectModel public

ModelOfImportProjectCheckedImport :
  ∀ {policy project} →
  (scoped : ProjectScopedImportProject policy project) →
  ImportProjectInterpretation scoped →
  Type₀
ModelOfImportProjectCheckedImport scoped interpretation =
  ModelOfCompleteCheckedImport
    (importProjectCheckedImport scoped)
    (importProjectCheckedSourceEvidence scoped)
    interpretation

ImportProjectCheckedImportModel :
  ∀ {policy project} →
  ProjectScopedImportProject policy project →
  Type₁
ImportProjectCheckedImportModel scoped =
  CompleteCheckedImportModel (importProjectCheckedImport scoped)

importProjectModelToCheckedImportModel :
  ∀ {policy project} →
  (scoped : ProjectScopedImportProject policy project) →
  ImportProjectModel scoped →
  ImportProjectCheckedImportModel scoped
importProjectModelToCheckedImportModel scoped model =
  completeCheckedImportModel
    (importProjectCheckedSourceEvidence scoped)
    (importProjectInterpretation model)
    (importProjectModelToMergedOntology
      scoped
      (importProjectInterpretation model)
      (importProjectSatisfies model))

checkedImportModelToImportProjectModel :
  ∀ {policy project} →
  (scoped : ProjectScopedImportProject policy project) →
  ImportProjectCheckedImportModel scoped →
  ImportProjectModel scoped
checkedImportModelToImportProjectModel scoped model =
  importProjectModel
    (completeInterpretation model)
    (mergedOntologyToImportProjectModel
      scoped
      (completeInterpretation model)
      (completeSatisfies model))

projectScopedFromClean :
  ∀ {policy} →
  (result : ImportProjectElaborationResult policy) →
  Clean result →
  ProjectScopedImportProject policy (input result)
projectScopedFromClean result clean =
  evidenceFromClean result clean

projectScopedSoundFromClean :
  ∀ {policy} →
  (result : ImportProjectElaborationResult policy) →
  (clean : Clean result) →
  ElaboratesToProjectScopedImportProject
    policy
    (input result)
    (projectScopedFromClean result clean)
projectScopedSoundFromClean result clean =
  soundFromClean result clean