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

module OWL2.Elab.ImportProject where

open import OWL2.Prelude
open import OWL2.Check.Result
open import OWL2.Diagnostics
open import OWL2.Elab.CheckedImport
open import OWL2.Elab.Policy
open import OWL2.Elab.Punning
open import OWL2.Elab.Regularity
open import OWL2.Elab.Result
open import OWL2.Elab.Structural
open import OWL2.Elab.SymbolTable
open import OWL2.Foundation.Maybe
open import OWL2.Raw hiding (SourcePath; sourcePath; rootPath; fieldPath; indexPath)
import OWL2.Kernel as K

private
  elabCode : String → DiagnosticCode
  elabCode name =
    mkDiagnosticCode "elab.import-project" name

  importsPath : SourcePath
  importsPath =
    sourcePath (fieldSegment "imports" ∷ [])

  documentsPath : SourcePath
  documentsPath =
    sourcePath (fieldSegment "documents" ∷ [])

record RawImportProject : Type₀ where
  constructor rawImportProject
  field
    projectRoot :
      RawOntology
    projectImports :
      List RawOntology

open RawImportProject public

record RawOntologyID : Type₀ where
  constructor rawOntologyID
  field
    ontologyIDIRI :
      Optional RawIRI
    ontologyIDVersionIRI :
      Optional RawIRI

open RawOntologyID public

sourceOntologyID : RawOntology → RawOntologyID
sourceOntologyID raw =
  rawOntologyID (ontologyIRI raw) (versionIRI raw)

documentOntologyIDs : List RawOntology → List RawOntologyID
documentOntologyIDs [] =
  []
documentOntologyIDs (document ∷ documents) =
  sourceOntologyID document ∷ documentOntologyIDs documents

sameOptionalRawIRI : Optional RawIRI → Optional RawIRI → Bool
sameOptionalRawIRI absent absent =
  true
sameOptionalRawIRI absent (present right) =
  false
sameOptionalRawIRI (present left) absent =
  false
sameOptionalRawIRI (present left) (present right) =
  sameRawIRI left right

sameRawOntologyID : RawOntologyID → RawOntologyID → Bool
sameRawOntologyID left right with
  sameOptionalRawIRI (ontologyIDIRI left) (ontologyIDIRI right) |
  sameOptionalRawIRI (ontologyIDVersionIRI left) (ontologyIDVersionIRI right)
... | true | true =
  true
... | true | false =
  false
... | false | versionMatches =
  false

rawOntologyIDInList : RawOntologyID → List RawOntologyID → Bool
rawOntologyIDInList id [] =
  false
rawOntologyIDInList id (candidate ∷ candidates) with
  sameRawOntologyID id candidate
... | true =
  true
... | false =
  rawOntologyIDInList id candidates

rawOntologyIDIRIInList : RawIRI → List RawOntologyID → Bool
rawOntologyIDIRIInList iri [] =
  false
rawOntologyIDIRIInList iri (candidate ∷ candidates) with
  ontologyIDIRI candidate
... | absent =
  rawOntologyIDIRIInList iri candidates
... | present candidateIRI with sameRawIRI iri candidateIRI
... | true =
  true
... | false =
  rawOntologyIDIRIInList iri candidates

rawOntologyIDIRIMultipleInList : RawIRI → List RawOntologyID → Bool
rawOntologyIDIRIMultipleInList iri [] =
  false
rawOntologyIDIRIMultipleInList iri (candidate ∷ candidates) with
  ontologyIDIRI candidate
... | absent =
  rawOntologyIDIRIMultipleInList iri candidates
... | present candidateIRI with sameRawIRI iri candidateIRI
... | true =
  rawOntologyIDIRIInList iri candidates
... | false =
  rawOntologyIDIRIMultipleInList iri candidates

importOntologyID : RawIRI → RawOntologyID
importOntologyID iri =
  rawOntologyID (present iri) absent

ontologyIDInDocuments : RawOntologyID → List RawOntology → Bool
ontologyIDInDocuments id documents =
  rawOntologyIDInList id (documentOntologyIDs documents)

projectDocuments : RawImportProject → List RawOntology
projectDocuments project =
  projectRoot project ∷ projectImports project

projectDocumentsAxioms : List RawOntology → List (RawAnnotated RawAxiom)
projectDocumentsAxioms [] =
  []
projectDocumentsAxioms (document ∷ documents) =
  axioms document ++ projectDocumentsAxioms documents

projectAxioms : RawImportProject → List (RawAnnotated RawAxiom)
projectAxioms project =
  projectDocumentsAxioms (projectDocuments project)

projectOntologyIDs : RawImportProject → List RawOntologyID
projectOntologyIDs project =
  documentOntologyIDs (projectDocuments project)

eraseRawOntologyHeader : RawOntology → RawOntology
eraseRawOntologyHeader raw =
  rawOntology
    (provenance raw)
    absent
    absent
    []
    (annotations raw)
    (axioms raw)

sourceSymbolTable : RawOntology → SymbolTable
sourceSymbolTable raw =
  symbolTableFromRaw (eraseRawOntologyHeader raw)

appendProjectImportTables : List RawOntology → SymbolTable
appendProjectImportTables [] =
  emptySymbolTable
appendProjectImportTables (source ∷ sources) =
  appendSymbolTables
    K.noPunning
    (sourceSymbolTable source)
    (appendProjectImportTables sources)

projectRootSymbolTable : RawImportProject → SymbolTable
projectRootSymbolTable project =
  sourceSymbolTable (projectRoot project)

projectImportsSymbolTable : RawImportProject → SymbolTable
projectImportsSymbolTable project =
  appendProjectImportTables (projectImports project)

projectSymbolTable : RawImportProject → SymbolTable
projectSymbolTable project =
  appendSymbolTables
    K.noPunning
    (projectRootSymbolTable project)
    (projectImportsSymbolTable project)

record ProjectSymbolTables (project : RawImportProject) : Type₀ where
  constructor projectSymbolTables
  field
    rootTable :
      SymbolTable
    importTables :
      SymbolTable
    combinedTable :
      SymbolTable
    rootTableRecorded :
      rootTable ≡ projectRootSymbolTable project
    importTablesRecorded :
      importTables ≡ projectImportsSymbolTable project
    combinedTableRecorded :
      combinedTable ≡ projectSymbolTable project
    rootToProjectMorphism :
      K.SignatureMorphism
        (symbolTableSignature rootTable)
        (symbolTableSignature combinedTable)
    importsToProjectMorphism :
      K.SignatureMorphism
        (symbolTableSignature importTables)
        (symbolTableSignature combinedTable)

open ProjectSymbolTables public

projectSymbolTablesOf : (project : RawImportProject) → ProjectSymbolTables project
projectSymbolTablesOf project =
  projectSymbolTables
    rootProjectTable
    importProjectTables
    combinedProjectTable
    refl
    refl
    refl
    (leftSymbolTableMorphism K.noPunning rootProjectTable importProjectTables)
    (rightSymbolTableMorphism K.noPunning rootProjectTable importProjectTables)
  where
  rootProjectTable : SymbolTable
  rootProjectTable =
    projectRootSymbolTable project

  importProjectTables : SymbolTable
  importProjectTables =
    projectImportsSymbolTable project

  combinedProjectTable : SymbolTable
  combinedProjectTable =
    projectSymbolTable project

projectStructuralContext :
  (project : RawImportProject) →
  K.RegularityContext (symbolTableSignature (projectSymbolTable project))
projectStructuralContext project =
  structuralRegularityContext
    (projectSymbolTable project)
    (projectAxioms project)

data ProjectImportDocumentMorphisms
  (project : RawImportProject) : List RawOntology → Type₀ where
  projectImportDocumentMorphisms[] :
    ProjectImportDocumentMorphisms project []
  projectImportDocumentMorphisms∷ :
    ∀ {source sources} →
    K.SignatureMorphism
      (symbolTableSignature (sourceSymbolTable source))
      (symbolTableSignature (projectSymbolTable project)) →
    ProjectImportDocumentMorphisms project sources →
    ProjectImportDocumentMorphisms project (source ∷ sources)

projectImportDocumentHeadMorphism :
  ∀ {project source sources} →
  ProjectImportDocumentMorphisms project (source ∷ sources) →
  K.SignatureMorphism
    (symbolTableSignature (sourceSymbolTable source))
    (symbolTableSignature (projectSymbolTable project))
projectImportDocumentHeadMorphism
  (projectImportDocumentMorphisms∷ morphism morphisms) =
  morphism

projectImportDocumentTailMorphisms :
  ∀ {project source sources} →
  ProjectImportDocumentMorphisms project (source ∷ sources) →
  ProjectImportDocumentMorphisms project sources
projectImportDocumentTailMorphisms
  (projectImportDocumentMorphisms∷ morphism morphisms) =
  morphisms

projectImportDocumentMorphismsFrom :
  (project : RawImportProject) →
  (sources : List RawOntology) →
  K.SignatureMorphism
    (symbolTableSignature (appendProjectImportTables sources))
    (symbolTableSignature (projectSymbolTable project)) →
  ProjectImportDocumentMorphisms project sources
projectImportDocumentMorphismsFrom project [] aggregateToProject =
  projectImportDocumentMorphisms[]
projectImportDocumentMorphismsFrom
  project
  (source ∷ sources)
  aggregateToProject =
  projectImportDocumentMorphisms∷
    (K.composeSignatureMorphism
      aggregateToProject
      (leftSymbolTableMorphism
        K.noPunning
        (sourceSymbolTable source)
        (appendProjectImportTables sources)))
    (projectImportDocumentMorphismsFrom
      project
      sources
      (K.composeSignatureMorphism
        aggregateToProject
        (rightSymbolTableMorphism
          K.noPunning
          (sourceSymbolTable source)
          (appendProjectImportTables sources))))

projectImportDocumentMorphismsOf :
  (project : RawImportProject) →
  ProjectImportDocumentMorphisms project (projectImports project)
projectImportDocumentMorphismsOf project =
  projectImportDocumentMorphismsFrom
    project
    (projectImports project)
    (rightSymbolTableMorphism
      K.noPunning
      (projectRootSymbolTable project)
      (projectImportsSymbolTable project))

missingImportDiagnostic : RawIRI → Diagnostic
missingImportDiagnostic iri =
  diagnostic
    (elabCode "missing-import")
    severityError
    importsPath
    "The import project does not contain a document for one requested import IRI."

duplicateOntologyIRIDiagnostic : RawIRI → Diagnostic
duplicateOntologyIRIDiagnostic iri =
  diagnostic
    (elabCode "duplicate-ontology-iri")
    severityError
    documentsPath
    "The import project contains more than one document with the same ontology ID."

ambiguousImportDiagnostic : RawIRI → Diagnostic
ambiguousImportDiagnostic iri =
  diagnostic
    (elabCode "ambiguous-import-iri")
    severityError
    importsPath
    "The import project contains more than one document matching one requested import IRI."

rawIRIInList : RawIRI → List RawIRI → Bool
rawIRIInList iri [] =
  false
rawIRIInList iri (candidate ∷ candidates) with sameRawIRI iri candidate
... | true =
  true
... | false =
  rawIRIInList iri candidates

ontologyIRIInDocuments : RawIRI → List RawOntology → Bool
ontologyIRIInDocuments iri documents =
  rawOntologyIDIRIInList iri (documentOntologyIDs documents)

ontologyIRIAmbiguousInDocuments : RawIRI → List RawOntology → Bool
ontologyIRIAmbiguousInDocuments iri documents =
  rawOntologyIDIRIMultipleInList iri (documentOntologyIDs documents)

missingImportDiagnostics :
  List RawOntology → List RawIRI → Diagnostics
missingImportDiagnostics available [] =
  noDiagnostics
missingImportDiagnostics available (iri ∷ iris) with
  ontologyIRIInDocuments iri available
... | true =
  missingImportDiagnostics available iris
... | false =
  singleDiagnostic (missingImportDiagnostic iri) ++
  missingImportDiagnostics available iris

documentMissingImportDiagnostics :
  List RawOntology → RawOntology → Diagnostics
documentMissingImportDiagnostics available document =
  missingImportDiagnostics available (imports document)

documentsMissingImportDiagnostics :
  List RawOntology → List RawOntology → Diagnostics
documentsMissingImportDiagnostics available [] =
  noDiagnostics
documentsMissingImportDiagnostics available (document ∷ documents) =
  documentMissingImportDiagnostics available document ++
  documentsMissingImportDiagnostics available documents

ambiguousImportDiagnostics :
  List RawOntology → List RawIRI → Diagnostics
ambiguousImportDiagnostics available [] =
  noDiagnostics
ambiguousImportDiagnostics available (iri ∷ iris) with
  ontologyIRIAmbiguousInDocuments iri available
... | true =
  singleDiagnostic (ambiguousImportDiagnostic iri) ++
  ambiguousImportDiagnostics available iris
... | false =
  ambiguousImportDiagnostics available iris

documentAmbiguousImportDiagnostics :
  List RawOntology → RawOntology → Diagnostics
documentAmbiguousImportDiagnostics available document =
  ambiguousImportDiagnostics available (imports document)

documentsAmbiguousImportDiagnostics :
  List RawOntology → List RawOntology → Diagnostics
documentsAmbiguousImportDiagnostics available [] =
  noDiagnostics
documentsAmbiguousImportDiagnostics available (document ∷ documents) =
  documentAmbiguousImportDiagnostics available document ++
  documentsAmbiguousImportDiagnostics available documents

duplicateOntologyIRIDiagnosticsFrom :
  List RawOntologyID → List RawOntology → Diagnostics
duplicateOntologyIRIDiagnosticsFrom seen [] =
  noDiagnostics
duplicateOntologyIRIDiagnosticsFrom seen (document ∷ documents) with
  sourceOntologyID document
... | id with ontologyIDIRI id
... | absent =
  duplicateOntologyIRIDiagnosticsFrom seen documents
... | present iri with rawOntologyIDInList id seen
... | true =
  singleDiagnostic (duplicateOntologyIRIDiagnostic iri) ++
  duplicateOntologyIRIDiagnosticsFrom seen documents
... | false =
  duplicateOntologyIRIDiagnosticsFrom (id ∷ seen) documents

duplicateOntologyIRIDiagnostics : List RawOntology → Diagnostics
duplicateOntologyIRIDiagnostics =
  duplicateOntologyIRIDiagnosticsFrom []

projectDocumentResult : ImportPolicy → RawOntology → ElaborationResult
projectDocumentResult policy source =
  elaborateStructuralKernel policy (eraseRawOntologyHeader source)

projectDocumentDiagnostics : RawOntology → Diagnostics
projectDocumentDiagnostics source =
  structuralElaborationDiagnostics (eraseRawOntologyHeader source)

projectDocumentsDiagnostics : List RawOntology → Diagnostics
projectDocumentsDiagnostics [] =
  noDiagnostics
projectDocumentsDiagnostics (source ∷ sources) =
  projectDocumentDiagnostics source ++
  projectDocumentsDiagnostics sources

record CheckedProjectDocument
  (policy : ImportPolicy)
  (source : RawOntology)
  : Type₀ where
  constructor checkedProjectDocument
  field
    documentClean :
      Clean (projectDocumentResult policy source)

open CheckedProjectDocument public

data CheckedProjectDocuments
  (policy : ImportPolicy) : List RawOntology → Type₀ where
  checkedProjectDocuments[] :
    CheckedProjectDocuments policy []
  checkedProjectDocuments∷ :
    ∀ {source sources} →
    CheckedProjectDocument policy source →
    CheckedProjectDocuments policy sources →
    CheckedProjectDocuments policy (source ∷ sources)

projectDocumentChecked :
  ∀ {policy source} →
  CheckedProjectDocument policy source → CheckedImport
projectDocumentChecked {policy} {source} document =
  evidenceFromClean
    (projectDocumentResult policy source)
    (documentClean document)

projectDocumentSignatureFromSource :
  ∀ {policy source} →
  (document : CheckedProjectDocument policy source) →
  signature (projectDocumentChecked document) ≡
  symbolTableSignature (sourceSymbolTable source)
projectDocumentSignatureFromSource {policy} {source} document =
  cong signature
    (presentValueFromEvidenceFromCleanDiagnostics
      (projectDocumentDiagnostics source)
      (checkedImportFromCleanStructural
        policy
        (eraseRawOntologyHeader source))
      (cleanEvidence
        (projectDocumentResult policy source)
        (documentClean document)))

projectDocumentSound :
  ∀ {policy source} →
  (document : CheckedProjectDocument policy source) →
  ElaboratesToCheckedImport
    (eraseRawOntologyHeader source)
    (projectDocumentChecked document)
projectDocumentSound {policy} {source} document =
  soundFromClean
    (projectDocumentResult policy source)
    (documentClean document)

projectDocumentSourceImports :
  ∀ {policy source} →
  CheckedProjectDocument policy source → List RawIRI
projectDocumentSourceImports {source = source} document =
  imports source

projectDocumentNormalizedImportsClosed :
  ∀ {policy source} →
  (document : CheckedProjectDocument policy source) →
  imports (eraseRawOntologyHeader source) ≡ []
projectDocumentNormalizedImportsClosed document =
  refl

projectDocumentsChecked :
  ∀ {policy sources} →
  CheckedProjectDocuments policy sources → List CheckedImport
projectDocumentsChecked checkedProjectDocuments[] =
  []
projectDocumentsChecked (checkedProjectDocuments∷ document documents) =
  projectDocumentChecked document ∷ projectDocumentsChecked documents

data CheckedProjectDocumentMorphisms
  (policy : ImportPolicy)
  (project : RawImportProject) :
  (sources : List RawOntology) →
  CheckedProjectDocuments policy sources →
  Type₀ where
  checkedProjectDocumentMorphisms[] :
    CheckedProjectDocumentMorphisms
      policy
      project
      []
      checkedProjectDocuments[]
  checkedProjectDocumentMorphisms∷ :
    ∀ {source sources document documents} →
    K.SignatureMorphism
      (signature (projectDocumentChecked document))
      (symbolTableSignature (projectSymbolTable project)) →
    CheckedProjectDocumentMorphisms policy project sources documents →
    CheckedProjectDocumentMorphisms
      policy
      project
      (source ∷ sources)
      (checkedProjectDocuments∷ document documents)

checkedProjectDocumentHeadMorphism :
  ∀ {policy project source sources document documents} →
  CheckedProjectDocumentMorphisms
    policy
    project
    (source ∷ sources)
    (checkedProjectDocuments∷ document documents) →
  K.SignatureMorphism
    (signature (projectDocumentChecked document))
    (symbolTableSignature (projectSymbolTable project))
checkedProjectDocumentHeadMorphism
  (checkedProjectDocumentMorphisms∷ morphism morphisms) =
  morphism

checkedProjectDocumentTailMorphisms :
  ∀ {policy project source sources document documents} →
  CheckedProjectDocumentMorphisms
    policy
    project
    (source ∷ sources)
    (checkedProjectDocuments∷ document documents) →
  CheckedProjectDocumentMorphisms policy project sources documents
checkedProjectDocumentTailMorphisms
  (checkedProjectDocumentMorphisms∷ morphism morphisms) =
  morphisms

checkedProjectDocumentMorphismFromSource :
  ∀ {policy project source} →
  (document : CheckedProjectDocument policy source) →
  K.SignatureMorphism
    (symbolTableSignature (sourceSymbolTable source))
    (symbolTableSignature (projectSymbolTable project)) →
  K.SignatureMorphism
    (signature (projectDocumentChecked document))
    (symbolTableSignature (projectSymbolTable project))
checkedProjectDocumentMorphismFromSource {project = project} document sourceMorphism =
  subst
    (λ Sig →
      K.SignatureMorphism Sig
        (symbolTableSignature (projectSymbolTable project)))
    (sym (projectDocumentSignatureFromSource document))
    sourceMorphism

checkedProjectDocumentMorphismsFromSource :
  ∀ {policy project sources} →
  ProjectImportDocumentMorphisms project sources →
  (documents : CheckedProjectDocuments policy sources) →
  CheckedProjectDocumentMorphisms policy project sources documents
checkedProjectDocumentMorphismsFromSource
  projectImportDocumentMorphisms[]
  checkedProjectDocuments[] =
  checkedProjectDocumentMorphisms[]
checkedProjectDocumentMorphismsFromSource
  {project = project}
  (projectImportDocumentMorphisms∷ sourceMorphism sourceMorphisms)
  (checkedProjectDocuments∷ document documents) =
  checkedProjectDocumentMorphisms∷
    (checkedProjectDocumentMorphismFromSource
      {project = project}
      document
      sourceMorphism)
    (checkedProjectDocumentMorphismsFromSource
      {project = project}
      sourceMorphisms
      documents)

checkedProjectDocumentProjectOntology :
  ∀ {policy project source} →
  K.RegularityContext (symbolTableSignature (projectSymbolTable project)) →
  (document : CheckedProjectDocument policy source) →
  K.SignatureMorphism
    (signature (projectDocumentChecked document))
    (symbolTableSignature (projectSymbolTable project)) →
  K.Ontology (symbolTableSignature (projectSymbolTable project))
checkedProjectDocumentProjectOntology context document morphism =
  K.renameOntology morphism context (ontology (projectDocumentChecked document))

checkedProjectDocumentsProjectOntologies :
  ∀ {policy project sources} →
  K.RegularityContext (symbolTableSignature (projectSymbolTable project)) →
  (checkedDocuments : CheckedProjectDocuments policy sources) →
  CheckedProjectDocumentMorphisms policy project sources checkedDocuments →
  List (K.Ontology (symbolTableSignature (projectSymbolTable project)))
checkedProjectDocumentsProjectOntologies
  context
  checkedProjectDocuments[]
  checkedProjectDocumentMorphisms[] =
  []
checkedProjectDocumentsProjectOntologies
  {policy = policy}
  {project = project}
  {sources = source ∷ sources}
  context
  (checkedProjectDocuments∷ document documents)
  (checkedProjectDocumentMorphisms∷ morphism morphisms) =
  checkedProjectDocumentProjectOntology
    {project = project}
    context
    document
    morphism ∷
  checkedProjectDocumentsProjectOntologies
    {policy = policy}
    {project = project}
    {sources = sources}
    context
    documents
    morphisms

CheckedProjectDocumentsSound :
  ∀ {policy} →
  (sources : List RawOntology) →
  CheckedProjectDocuments policy sources →
  Type₀
CheckedProjectDocumentsSound [] checkedProjectDocuments[] =
  Unit
CheckedProjectDocumentsSound
  (source ∷ sources)
  (checkedProjectDocuments∷ document documents) =
  ElaboratesToCheckedImport
    (eraseRawOntologyHeader source)
    (projectDocumentChecked document)
  × CheckedProjectDocumentsSound sources documents

checkedProjectDocumentsSoundOf :
  ∀ {policy}
    (sources : List RawOntology)
    (documents : CheckedProjectDocuments policy sources) →
  CheckedProjectDocumentsSound sources documents
checkedProjectDocumentsSoundOf [] checkedProjectDocuments[] =
  tt
checkedProjectDocumentsSoundOf
  (source ∷ sources)
  (checkedProjectDocuments∷ document documents) =
  projectDocumentSound document ,
  checkedProjectDocumentsSoundOf sources documents

checkedProjectDocumentsFromClean :
  (policy : ImportPolicy) →
  (sources : List RawOntology) →
  CleanDiagnostics (projectDocumentsDiagnostics sources) →
  CheckedProjectDocuments policy sources
checkedProjectDocumentsFromClean policy [] clean =
  checkedProjectDocuments[]
checkedProjectDocumentsFromClean policy (source ∷ sources) clean =
  checkedProjectDocuments∷
    (checkedProjectDocument
      (cleanAppendLeft
        (projectDocumentDiagnostics source)
        (projectDocumentsDiagnostics sources)
        clean))
    (checkedProjectDocumentsFromClean
      policy
      sources
      (cleanAppendRight
        (projectDocumentDiagnostics source)
        (projectDocumentsDiagnostics sources)
        clean))

projectDuplicateDiagnostics : RawImportProject → Diagnostics
projectDuplicateDiagnostics project =
  duplicateOntologyIRIDiagnostics (projectDocuments project)

projectMissingDiagnostics : RawImportProject → Diagnostics
projectMissingDiagnostics project =
  documentsMissingImportDiagnostics
    (projectDocuments project)
    (projectDocuments project)

projectAmbiguousDiagnostics : RawImportProject → Diagnostics
projectAmbiguousDiagnostics project =
  documentsAmbiguousImportDiagnostics
    (projectDocuments project)
    (projectDocuments project)

checkedImportProjectStructuralDiagnostics : RawImportProject → Diagnostics
checkedImportProjectStructuralDiagnostics project =
  projectDocumentsDiagnostics (projectDocuments project)

projectDocumentScopedDiagnostics :
  (project : RawImportProject) →
  RawOntology →
  Diagnostics
projectDocumentScopedDiagnostics project source =
  annotationsDiagnostics table (annotations source) ++
  structuralAxiomsDiagnostics table context (axioms source)
  where
  table : SymbolTable
  table =
    projectSymbolTable project

  context : K.RegularityContext (symbolTableSignature table)
  context =
    projectStructuralContext project

projectDocumentsScopedDiagnostics :
  (project : RawImportProject) →
  List RawOntology →
  Diagnostics
projectDocumentsScopedDiagnostics project [] =
  noDiagnostics
projectDocumentsScopedDiagnostics project (source ∷ sources) =
  projectDocumentScopedDiagnostics project source ++
  projectDocumentsScopedDiagnostics project sources

projectScopedStructuralDiagnostics : RawImportProject → Diagnostics
projectScopedStructuralDiagnostics project =
  rawPunningDiagnosticsFromSymbolTable (projectSymbolTable project) ++
  projectDocumentScopedDiagnostics project (projectRoot project) ++
  projectDocumentsScopedDiagnostics project (projectImports project)

checkedImportProjectDiagnostics : RawImportProject → Diagnostics
checkedImportProjectDiagnostics project =
  projectDuplicateDiagnostics project ++
  projectMissingDiagnostics project ++
  projectAmbiguousDiagnostics project ++
  checkedImportProjectStructuralDiagnostics project

projectScopedImportDiagnostics : RawImportProject → Diagnostics
projectScopedImportDiagnostics project =
  projectDuplicateDiagnostics project ++
  projectMissingDiagnostics project ++
  projectAmbiguousDiagnostics project ++
  projectScopedStructuralDiagnostics project

importProjectDiagnostics : RawImportProject → Diagnostics
importProjectDiagnostics =
  projectScopedImportDiagnostics

checkedImportProjectDuplicateCleanFromClean :
  (project : RawImportProject) →
  CleanDiagnostics (checkedImportProjectDiagnostics project) →
  CleanDiagnostics (projectDuplicateDiagnostics project)
checkedImportProjectDuplicateCleanFromClean project clean =
  cleanAppendLeft
    (projectDuplicateDiagnostics project)
    (projectMissingDiagnostics project ++
     projectAmbiguousDiagnostics project ++
     checkedImportProjectStructuralDiagnostics project)
    clean

checkedImportProjectMissingCleanFromClean :
  (project : RawImportProject) →
  CleanDiagnostics (checkedImportProjectDiagnostics project) →
  CleanDiagnostics (projectMissingDiagnostics project)
checkedImportProjectMissingCleanFromClean project clean =
  cleanAppendLeft
    (projectMissingDiagnostics project)
    (projectAmbiguousDiagnostics project ++ checkedImportProjectStructuralDiagnostics project)
    (cleanAppendRight
      (projectDuplicateDiagnostics project)
      (projectMissingDiagnostics project ++
       projectAmbiguousDiagnostics project ++
       checkedImportProjectStructuralDiagnostics project)
      clean)

checkedImportProjectAmbiguousCleanFromClean :
  (project : RawImportProject) →
  CleanDiagnostics (checkedImportProjectDiagnostics project) →
  CleanDiagnostics (projectAmbiguousDiagnostics project)
checkedImportProjectAmbiguousCleanFromClean project clean =
  cleanAppendLeft
    (projectAmbiguousDiagnostics project)
    (checkedImportProjectStructuralDiagnostics project)
    (cleanAppendRight
      (projectMissingDiagnostics project)
      (projectAmbiguousDiagnostics project ++ checkedImportProjectStructuralDiagnostics project)
      (cleanAppendRight
        (projectDuplicateDiagnostics project)
        (projectMissingDiagnostics project ++
         projectAmbiguousDiagnostics project ++
         checkedImportProjectStructuralDiagnostics project)
        clean))

checkedImportProjectStructuralCleanFromClean :
  (project : RawImportProject) →
  CleanDiagnostics (checkedImportProjectDiagnostics project) →
  CleanDiagnostics (checkedImportProjectStructuralDiagnostics project)
checkedImportProjectStructuralCleanFromClean project clean =
  cleanAppendRight
    (projectAmbiguousDiagnostics project)
    (checkedImportProjectStructuralDiagnostics project)
    (cleanAppendRight
      (projectMissingDiagnostics project)
      (projectAmbiguousDiagnostics project ++ checkedImportProjectStructuralDiagnostics project)
      (cleanAppendRight
        (projectDuplicateDiagnostics project)
        (projectMissingDiagnostics project ++
         projectAmbiguousDiagnostics project ++
         checkedImportProjectStructuralDiagnostics project)
        clean))

checkedImportProjectRootDocumentCleanFromClean :
  (policy : ImportPolicy) →
  (project : RawImportProject) →
  CleanDiagnostics (checkedImportProjectDiagnostics project) →
  Clean (projectDocumentResult policy (projectRoot project))
checkedImportProjectRootDocumentCleanFromClean policy project clean =
  cleanAppendLeft
    (projectDocumentDiagnostics (projectRoot project))
    (projectDocumentsDiagnostics (projectImports project))
    (checkedImportProjectStructuralCleanFromClean project clean)

checkedImportProjectImportDocumentsCleanFromClean :
  (project : RawImportProject) →
  CleanDiagnostics (checkedImportProjectDiagnostics project) →
  CleanDiagnostics (projectDocumentsDiagnostics (projectImports project))
checkedImportProjectImportDocumentsCleanFromClean project clean =
  cleanAppendRight
    (projectDocumentDiagnostics (projectRoot project))
    (projectDocumentsDiagnostics (projectImports project))
    (checkedImportProjectStructuralCleanFromClean project clean)

record CheckedImportProject
  (policy : ImportPolicy)
  (project : RawImportProject)
  : Type₀ where
  constructor checkedImportProject
  field
    projectPolicyEvidence :
      ImportPolicyEvidence policy
    duplicateOntologyIDsClean :
      CleanDiagnostics (projectDuplicateDiagnostics project)
    missingImportsClean :
      CleanDiagnostics (projectMissingDiagnostics project)
    ambiguousImportsClean :
      CleanDiagnostics (projectAmbiguousDiagnostics project)
    checkedRootDocument :
      CheckedProjectDocument policy (projectRoot project)
    checkedImportDocuments :
      CheckedProjectDocuments policy (projectImports project)

open CheckedImportProject public

record CheckedImportProjectMorphisms
  {policy : ImportPolicy}
  {project : RawImportProject}
  (checked : CheckedImportProject policy project)
  : Type₀ where
  constructor checkedImportProjectMorphisms
  field
    checkedRootToProjectMorphism :
      K.SignatureMorphism
        (signature
          (projectDocumentChecked
            (checkedRootDocument checked)))
        (symbolTableSignature (projectSymbolTable project))
    checkedImportsToProjectMorphisms :
      CheckedProjectDocumentMorphisms
        policy
        project
        (projectImports project)
        (checkedImportDocuments checked)

open CheckedImportProjectMorphisms public

checkedImportProjectMorphismsOf :
  ∀ {policy project} →
  (checked : CheckedImportProject policy project) →
  CheckedImportProjectMorphisms checked
checkedImportProjectMorphismsOf {project = project} checked =
  checkedImportProjectMorphisms
    (checkedProjectDocumentMorphismFromSource
      {project = project}
      (checkedRootDocument checked)
      (leftSymbolTableMorphism
        K.noPunning
        (projectRootSymbolTable project)
        (projectImportsSymbolTable project)))
    (checkedProjectDocumentMorphismsFromSource
      (projectImportDocumentMorphismsOf project)
      (checkedImportDocuments checked))

record CheckedImportProjectProjection
  {policy : ImportPolicy}
  {project : RawImportProject}
  (checked : CheckedImportProject policy project)
  (context :
    K.RegularityContext (symbolTableSignature (projectSymbolTable project)))
  : Type₀ where
  constructor checkedImportProjectProjection
  field
    projectionMorphisms :
      CheckedImportProjectMorphisms checked
    projectedRootOntology :
      K.Ontology (symbolTableSignature (projectSymbolTable project))
    projectedImportOntologies :
      List (K.Ontology (symbolTableSignature (projectSymbolTable project)))

open CheckedImportProjectProjection public

checkedImportProjectProjectionOf :
  ∀ {policy project} →
  (checked : CheckedImportProject policy project) →
  (context :
    K.RegularityContext (symbolTableSignature (projectSymbolTable project))) →
  CheckedImportProjectProjection checked context
checkedImportProjectProjectionOf {policy = policy} {project = project} checked context =
  checkedImportProjectProjection
    morphisms
    (checkedProjectDocumentProjectOntology
      {project = project}
      context
      (checkedRootDocument checked)
      (checkedRootToProjectMorphism morphisms))
    (checkedProjectDocumentsProjectOntologies
      {policy = policy}
      {project = project}
      {sources = projectImports project}
      context
      (checkedImportDocuments checked)
      (checkedImportsToProjectMorphisms morphisms))
  where
  morphisms : CheckedImportProjectMorphisms checked
  morphisms =
    checkedImportProjectMorphismsOf checked

private
  uncheckedProjectDocumentScopedOntology :
    (project : RawImportProject) →
    RawOntology →
    K.Ontology (symbolTableSignature (projectSymbolTable project))
  uncheckedProjectDocumentScopedOntology project source =
    structuralOntologyFromTable
      (projectSymbolTable project)
      (projectStructuralContext project)
      source

  projectDocumentScopedOntologyFromClean :
    (project : RawImportProject) →
    (source : RawOntology) →
    CleanDiagnostics (projectDocumentScopedDiagnostics project source) →
    K.Ontology (symbolTableSignature (projectSymbolTable project))
  projectDocumentScopedOntologyFromClean project source clean =
    uncheckedProjectDocumentScopedOntology project source

  projectDocumentsScopedOntologiesFromClean :
    (project : RawImportProject) →
    (sources : List RawOntology) →
    CleanDiagnostics (projectDocumentsScopedDiagnostics project sources) →
    List (K.Ontology (symbolTableSignature (projectSymbolTable project)))
  projectDocumentsScopedOntologiesFromClean project [] clean =
    []
  projectDocumentsScopedOntologiesFromClean project (source ∷ sources) clean =
    projectDocumentScopedOntologyFromClean
      project
      source
      (cleanAppendLeft
        (projectDocumentScopedDiagnostics project source)
        (projectDocumentsScopedDiagnostics project sources)
        clean)
    ∷
    projectDocumentsScopedOntologiesFromClean
      project
      sources
      (cleanAppendRight
        (projectDocumentScopedDiagnostics project source)
        (projectDocumentsScopedDiagnostics project sources)
        clean)

projectScopedDuplicateCleanFromClean :
  (project : RawImportProject) →
  CleanDiagnostics (projectScopedImportDiagnostics project) →
  CleanDiagnostics (projectDuplicateDiagnostics project)
projectScopedDuplicateCleanFromClean project clean =
  cleanAppendLeft
    (projectDuplicateDiagnostics project)
    (projectMissingDiagnostics project ++
     projectAmbiguousDiagnostics project ++
     projectScopedStructuralDiagnostics project)
    clean

projectScopedMissingCleanFromClean :
  (project : RawImportProject) →
  CleanDiagnostics (projectScopedImportDiagnostics project) →
  CleanDiagnostics (projectMissingDiagnostics project)
projectScopedMissingCleanFromClean project clean =
  cleanAppendLeft
    (projectMissingDiagnostics project)
    (projectAmbiguousDiagnostics project ++
     projectScopedStructuralDiagnostics project)
    (cleanAppendRight
      (projectDuplicateDiagnostics project)
      (projectMissingDiagnostics project ++
       projectAmbiguousDiagnostics project ++
       projectScopedStructuralDiagnostics project)
      clean)

projectScopedAmbiguousCleanFromClean :
  (project : RawImportProject) →
  CleanDiagnostics (projectScopedImportDiagnostics project) →
  CleanDiagnostics (projectAmbiguousDiagnostics project)
projectScopedAmbiguousCleanFromClean project clean =
  cleanAppendLeft
    (projectAmbiguousDiagnostics project)
    (projectScopedStructuralDiagnostics project)
    (cleanAppendRight
      (projectMissingDiagnostics project)
      (projectAmbiguousDiagnostics project ++
       projectScopedStructuralDiagnostics project)
      (cleanAppendRight
        (projectDuplicateDiagnostics project)
        (projectMissingDiagnostics project ++
         projectAmbiguousDiagnostics project ++
         projectScopedStructuralDiagnostics project)
        clean))

projectScopedStructuralCleanFromClean :
  (project : RawImportProject) →
  CleanDiagnostics (projectScopedImportDiagnostics project) →
  CleanDiagnostics (projectScopedStructuralDiagnostics project)
projectScopedStructuralCleanFromClean project clean =
  cleanAppendRight
    (projectAmbiguousDiagnostics project)
    (projectScopedStructuralDiagnostics project)
    (cleanAppendRight
      (projectMissingDiagnostics project)
      (projectAmbiguousDiagnostics project ++
       projectScopedStructuralDiagnostics project)
      (cleanAppendRight
        (projectDuplicateDiagnostics project)
        (projectMissingDiagnostics project ++
         projectAmbiguousDiagnostics project ++
         projectScopedStructuralDiagnostics project)
        clean))

projectScopedDocumentCleanFromStructuralClean :
  (project : RawImportProject) →
  CleanDiagnostics (projectScopedStructuralDiagnostics project) →
  CleanDiagnostics (projectDocumentScopedDiagnostics project (projectRoot project))
projectScopedDocumentCleanFromStructuralClean project clean =
  cleanAppendLeft
    (projectDocumentScopedDiagnostics project (projectRoot project))
    (projectDocumentsScopedDiagnostics project (projectImports project))
    (cleanAppendRight
      (rawPunningDiagnosticsFromSymbolTable (projectSymbolTable project))
      (projectDocumentScopedDiagnostics project (projectRoot project) ++
       projectDocumentsScopedDiagnostics project (projectImports project))
      clean)

projectScopedImportsCleanFromStructuralClean :
  (project : RawImportProject) →
  CleanDiagnostics (projectScopedStructuralDiagnostics project) →
  CleanDiagnostics (projectDocumentsScopedDiagnostics project (projectImports project))
projectScopedImportsCleanFromStructuralClean project clean =
  cleanAppendRight
    (projectDocumentScopedDiagnostics project (projectRoot project))
    (projectDocumentsScopedDiagnostics project (projectImports project))
    (cleanAppendRight
      (rawPunningDiagnosticsFromSymbolTable (projectSymbolTable project))
      (projectDocumentScopedDiagnostics project (projectRoot project) ++
       projectDocumentsScopedDiagnostics project (projectImports project))
      clean)

projectScopedDocumentCleanFromClean :
  (project : RawImportProject) →
  CleanDiagnostics (projectScopedImportDiagnostics project) →
  CleanDiagnostics (projectDocumentScopedDiagnostics project (projectRoot project))
projectScopedDocumentCleanFromClean project clean =
  projectScopedDocumentCleanFromStructuralClean
    project
    (projectScopedStructuralCleanFromClean project clean)

projectScopedImportsCleanFromClean :
  (project : RawImportProject) →
  CleanDiagnostics (projectScopedImportDiagnostics project) →
  CleanDiagnostics (projectDocumentsScopedDiagnostics project (projectImports project))
projectScopedImportsCleanFromClean project clean =
  projectScopedImportsCleanFromStructuralClean
    project
    (projectScopedStructuralCleanFromClean project clean)

appendProjectedOntologies :
  ∀ {Sig} →
  K.RegularityContext Sig →
  K.Ontology Sig →
  List (K.Ontology Sig) →
  K.Ontology Sig
appendProjectedOntologies context root [] =
  root
appendProjectedOntologies context root (ont ∷ ontologies) =
  K.appendOntologies
    context
    root
    (appendProjectedOntologies context ont ontologies)

record ProjectScopedImportProject
  (policy : ImportPolicy)
  (project : RawImportProject)
  : Type₀ where
  constructor projectScopedImportProject
  field
    scopedProjectPolicyEvidence :
      ImportPolicyEvidence policy
    scopedDuplicateOntologyIDsClean :
      CleanDiagnostics (projectDuplicateDiagnostics project)
    scopedMissingImportsClean :
      CleanDiagnostics (projectMissingDiagnostics project)
    scopedAmbiguousImportsClean :
      CleanDiagnostics (projectAmbiguousDiagnostics project)
    scopedStructuralClean :
      CleanDiagnostics (projectScopedStructuralDiagnostics project)
    scopedCheckedImport :
      CheckedImport
    scopedProjectionContext :
      K.RegularityContext (signature scopedCheckedImport)
    scopedProjectedRootOntology :
      K.Ontology (signature scopedCheckedImport)
    scopedProjectedImportOntologies :
      List (K.Ontology (signature scopedCheckedImport))
    scopedProjectedOntologyIsMerged :
      appendProjectedOntologies
        scopedProjectionContext
        scopedProjectedRootOntology
        scopedProjectedImportOntologies ≡
      ontology scopedCheckedImport

open ProjectScopedImportProject public
  hiding
    ( scopedCheckedImport
    ; scopedProjectionContext
    ; scopedProjectedRootOntology
    ; scopedProjectedImportOntologies
    ; scopedProjectedOntologyIsMerged
    )

projectSourceTableTrace :
  (project : RawImportProject) →
  CheckedSourceTableTrace (symbolTableSignature (projectSymbolTable project))
projectSourceTableTrace project =
  checkedSourceTableTrace
    (projectSymbolTable project)
    refl
    absent

projectCheckedImportFromMergedOntology :
  (policy : ImportPolicy) →
  (project : RawImportProject) →
  ImportPolicyEvidence policy →
  K.Ontology (symbolTableSignature (projectSymbolTable project)) →
  CheckedImport
projectCheckedImportFromMergedOntology policy project policyEvidence merged =
  checkedImport
    policy
    (symbolTableSignature (projectSymbolTable project))
    merged
    (K.completeSourceOntologySemanticSupport (K.axioms merged))
    (completeDeclarationEvidence (projectSourceTableTrace project))
    (completePropertyRoleEvidence (projectSourceTableTrace project))
    policyEvidence
    noImportClosure

importProjectCheckedImport :
  ∀ {policy project} →
  ProjectScopedImportProject policy project →
  CheckedImport
importProjectCheckedImport scoped =
  ProjectScopedImportProject.scopedCheckedImport scoped

importProjectCheckedSourceEvidence :
  ∀ {policy project} →
  (scoped : ProjectScopedImportProject policy project) →
  CheckedSourceEvidence (importProjectCheckedImport scoped)
importProjectCheckedSourceEvidence scoped =
  checkedSourceEvidenceOf (importProjectCheckedImport scoped)

importProjectProjectionContext :
  ∀ {policy project} →
  (scoped : ProjectScopedImportProject policy project) →
  K.RegularityContext (signature (importProjectCheckedImport scoped))
importProjectProjectionContext scoped =
  ProjectScopedImportProject.scopedProjectionContext scoped

importProjectRootOntology :
  ∀ {policy project} →
  (scoped : ProjectScopedImportProject policy project) →
  K.Ontology (signature (importProjectCheckedImport scoped))
importProjectRootOntology scoped =
  ProjectScopedImportProject.scopedProjectedRootOntology scoped

importProjectImportOntologies :
  ∀ {policy project} →
  (scoped : ProjectScopedImportProject policy project) →
  List (K.Ontology (signature (importProjectCheckedImport scoped)))
importProjectImportOntologies scoped =
  ProjectScopedImportProject.scopedProjectedImportOntologies scoped

importProjectOntologies :
  ∀ {policy project} →
  (scoped : ProjectScopedImportProject policy project) →
  List (K.Ontology (signature (importProjectCheckedImport scoped)))
importProjectOntologies scoped =
  importProjectRootOntology scoped ∷
  importProjectImportOntologies scoped

importProjectMergedOntology :
  ∀ {policy project} →
  (scoped : ProjectScopedImportProject policy project) →
  K.Ontology (signature (importProjectCheckedImport scoped))
importProjectMergedOntology scoped =
  ontology (importProjectCheckedImport scoped)

importProjectProjectedOntologyIsMerged :
  ∀ {policy project} →
  (scoped : ProjectScopedImportProject policy project) →
  appendProjectedOntologies
    (importProjectProjectionContext scoped)
    (importProjectRootOntology scoped)
    (importProjectImportOntologies scoped) ≡
  importProjectMergedOntology scoped
importProjectProjectedOntologyIsMerged scoped =
  ProjectScopedImportProject.scopedProjectedOntologyIsMerged scoped

projectScopedImportProjectFromClean :
  (policy : ImportPolicy) →
  (project : RawImportProject) →
  CleanDiagnostics (projectScopedImportDiagnostics project) →
  ProjectScopedImportProject policy project
projectScopedImportProjectFromClean policy project clean =
  projectScopedImportProject
    scopedImportPolicyEvidence
    (projectScopedDuplicateCleanFromClean project clean)
    (projectScopedMissingCleanFromClean project clean)
    (projectScopedAmbiguousCleanFromClean project clean)
    structuralClean
    checked
    context
    root
    importedOntologies
    refl
  where
  scopedImportPolicyEvidence : ImportPolicyEvidence policy
  scopedImportPolicyEvidence =
    trivialPolicyEvidence policy

  structuralClean : CleanDiagnostics (projectScopedStructuralDiagnostics project)
  structuralClean =
    projectScopedStructuralCleanFromClean project clean

  context : K.RegularityContext (symbolTableSignature (projectSymbolTable project))
  context =
    projectStructuralContext project

  root : K.Ontology (symbolTableSignature (projectSymbolTable project))
  root =
    projectDocumentScopedOntologyFromClean
      project
      (projectRoot project)
      (projectScopedDocumentCleanFromClean project clean)

  importedOntologies : List (K.Ontology (symbolTableSignature (projectSymbolTable project)))
  importedOntologies =
    projectDocumentsScopedOntologiesFromClean
      project
      (projectImports project)
      (projectScopedImportsCleanFromClean project clean)

  merged : K.Ontology (symbolTableSignature (projectSymbolTable project))
  merged =
    appendProjectedOntologies context root importedOntologies

  checked : CheckedImport
  checked =
    projectCheckedImportFromMergedOntology
      policy
      project
      scopedImportPolicyEvidence
      merged

record ElaboratesToProjectScopedImportProject
  (policy : ImportPolicy)
  (project : RawImportProject)
  (scoped : ProjectScopedImportProject policy project)
  : Type₀ where
  constructor elaboratesToProjectScopedImportProject
  field
    scopedDuplicateOntologyIDsAccepted :
      CleanDiagnostics (projectDuplicateDiagnostics project)
    scopedMissingImportsAccepted :
      CleanDiagnostics (projectMissingDiagnostics project)
    scopedAmbiguousImportsAccepted :
      CleanDiagnostics (projectAmbiguousDiagnostics project)
    scopedStructuralAccepted :
      CleanDiagnostics (projectScopedStructuralDiagnostics project)

open ElaboratesToProjectScopedImportProject public

ProjectScopedImportProjectResult : ImportPolicy → Type₀
ProjectScopedImportProjectResult policy =
  CheckResult
    RawImportProject
    (ProjectScopedImportProject policy)
    (ElaboratesToProjectScopedImportProject policy)

projectScopedImportEvidence? :
  (policy : ImportPolicy) →
  (project : RawImportProject) →
  Optional (ProjectScopedImportProject policy project)
projectScopedImportEvidence? policy project =
  evidenceFromCleanDiagnostics
    (projectScopedImportDiagnostics project)
    (projectScopedImportProjectFromClean policy project)

projectScopedImportCleanEvidence :
  (policy : ImportPolicy) →
  (project : RawImportProject) →
  CleanDiagnostics (projectScopedImportDiagnostics project) →
  Present (projectScopedImportEvidence? policy project)
projectScopedImportCleanEvidence policy project clean =
  cleanEvidenceFromCleanDiagnostics
    (projectScopedImportDiagnostics project)
    (projectScopedImportProjectFromClean policy project)
    clean

projectScopedImportSound :
  (policy : ImportPolicy) →
  (project : RawImportProject) →
  (proof : Present (projectScopedImportEvidence? policy project)) →
  ElaboratesToProjectScopedImportProject policy project (presentValue proof)
projectScopedImportSound policy project proof =
  elaboratesToProjectScopedImportProject
    (scopedDuplicateOntologyIDsClean scoped)
    (scopedMissingImportsClean scoped)
    (scopedAmbiguousImportsClean scoped)
    (scopedStructuralClean scoped)
  where
  scoped : ProjectScopedImportProject policy project
  scoped =
    presentValue proof

elaborateProjectScopedImport :
  (policy : ImportPolicy) →
  RawImportProject →
  ProjectScopedImportProjectResult policy
elaborateProjectScopedImport policy project =
  let diagnostics = projectScopedImportDiagnostics project in
  record
    { input =
        project
    ; diagnostics =
        diagnostics
    ; clean? =
        diagnosticsClean? diagnostics
    ; evidence? =
        projectScopedImportEvidence? policy project
    ; cleanEvidence =
        projectScopedImportCleanEvidence policy project
    ; sound =
        projectScopedImportSound policy project
    }

elaborateProjectScopedImportStrict :
  RawImportProject →
  ProjectScopedImportProjectResult strictPolicy
elaborateProjectScopedImportStrict =
  elaborateProjectScopedImport strictPolicy

ImportProjectElaborationResult : ImportPolicy → Type₀
ImportProjectElaborationResult =
  ProjectScopedImportProjectResult

elaborateImportProject :
  (policy : ImportPolicy) →
  RawImportProject →
  ImportProjectElaborationResult policy
elaborateImportProject =
  elaborateProjectScopedImport

elaborateImportProjectStrict :
  RawImportProject →
  ImportProjectElaborationResult strictPolicy
elaborateImportProjectStrict =
  elaborateProjectScopedImportStrict

checkedImportProjectFromClean :
  (policy : ImportPolicy) →
  (project : RawImportProject) →
  CleanDiagnostics (checkedImportProjectDiagnostics project) →
  CheckedImportProject policy project
checkedImportProjectFromClean policy project clean =
  checkedImportProject
    (trivialPolicyEvidence policy)
    (checkedImportProjectDuplicateCleanFromClean project clean)
    (checkedImportProjectMissingCleanFromClean project clean)
    (checkedImportProjectAmbiguousCleanFromClean project clean)
    (checkedProjectDocument
      (checkedImportProjectRootDocumentCleanFromClean policy project clean))
    (checkedProjectDocumentsFromClean
      policy
      (projectImports project)
      (checkedImportProjectImportDocumentsCleanFromClean project clean))

record ElaboratesToCheckedImportProject
  (policy : ImportPolicy)
  (project : RawImportProject)
  (checked : CheckedImportProject policy project)
  : Type₀ where
  constructor elaboratesToCheckedImportProject
  field
    duplicateOntologyIDsAccepted :
      CleanDiagnostics (projectDuplicateDiagnostics project)
    missingImportsAccepted :
      CleanDiagnostics (projectMissingDiagnostics project)
    ambiguousImportsAccepted :
      CleanDiagnostics (projectAmbiguousDiagnostics project)
    checkedRootSound :
      ElaboratesToCheckedImport
        (eraseRawOntologyHeader (projectRoot project))
        (projectDocumentChecked (checkedRootDocument checked))
    checkedImportsSound :
      CheckedProjectDocumentsSound
        (projectImports project)
        (checkedImportDocuments checked)

open ElaboratesToCheckedImportProject public

CheckedImportProjectElaborationResult : ImportPolicy → Type₀
CheckedImportProjectElaborationResult policy =
  CheckResult
    RawImportProject
    (CheckedImportProject policy)
    (ElaboratesToCheckedImportProject policy)

checkedImportProjectEvidence? :
  (policy : ImportPolicy) →
  (project : RawImportProject) →
  Optional (CheckedImportProject policy project)
checkedImportProjectEvidence? policy project =
  evidenceFromCleanDiagnostics
    (checkedImportProjectDiagnostics project)
    (checkedImportProjectFromClean policy project)

checkedImportProjectCleanEvidence :
  (policy : ImportPolicy) →
  (project : RawImportProject) →
  CleanDiagnostics (checkedImportProjectDiagnostics project) →
  Present (checkedImportProjectEvidence? policy project)
checkedImportProjectCleanEvidence policy project clean =
  cleanEvidenceFromCleanDiagnostics
    (checkedImportProjectDiagnostics project)
    (checkedImportProjectFromClean policy project)
    clean

checkedImportProjectSound :
  (policy : ImportPolicy) →
  (project : RawImportProject) →
  (proof : Present (checkedImportProjectEvidence? policy project)) →
  ElaboratesToCheckedImportProject policy project (presentValue proof)
checkedImportProjectSound policy project proof =
  elaboratesToCheckedImportProject
    (duplicateOntologyIDsClean checked)
    (missingImportsClean checked)
    (ambiguousImportsClean checked)
    (projectDocumentSound (checkedRootDocument checked))
    (checkedProjectDocumentsSoundOf
      (projectImports project)
      (checkedImportDocuments checked))
  where
  checked : CheckedImportProject policy project
  checked =
    presentValue proof

elaborateCheckedImportProject :
  (policy : ImportPolicy) →
  RawImportProject →
  CheckedImportProjectElaborationResult policy
elaborateCheckedImportProject policy project =
  let diagnostics = checkedImportProjectDiagnostics project in
  record
    { input =
        project
    ; diagnostics =
        diagnostics
    ; clean? =
        diagnosticsClean? diagnostics
    ; evidence? =
        checkedImportProjectEvidence? policy project
    ; cleanEvidence =
        checkedImportProjectCleanEvidence policy project
    ; sound =
        checkedImportProjectSound policy project
    }

elaborateCheckedImportProjectStrict :
  RawImportProject →
  CheckedImportProjectElaborationResult strictPolicy
elaborateCheckedImportProjectStrict =
  elaborateCheckedImportProject strictPolicy