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

module OWL2.Elab.CheckedImport where

open import Cubical.Data.Nat.Base using (zero; suc)
open import OWL2.Prelude
open import OWL2.Check.Bundle
open import OWL2.Elab.Policy
open import OWL2.Elab.SymbolTable
open import OWL2.Foundation.List using (listCount)
open import OWL2.Raw
import OWL2.Kernel as K

record CheckedImportClosure : Type₀ where
  constructor checkedImportClosure
  field
    requestedImports :
      List RawIRI
    requestedImportsClosed :
      requestedImports ≡ []

open CheckedImportClosure public

noImportClosure : CheckedImportClosure
noImportClosure =
  checkedImportClosure [] refl

noRawImportClosure :
  (raw : RawOntology) →
  imports raw ≡ [] →
  CheckedImportClosure
noRawImportClosure raw rawImportsClosed =
  checkedImportClosure (imports raw) rawImportsClosed

rawIRIsByCount : ℕ → List RawIRI
rawIRIsByCount zero =
  []
rawIRIsByCount (suc n) =
  rawIRI "synthetic" ∷ rawIRIsByCount n

rawIRIsByCountCount :
  (n : ℕ) →
  listCount (rawIRIsByCount n) ≡ n
rawIRIsByCountCount zero =
  refl
rawIRIsByCountCount (suc n) =
  cong suc (rawIRIsByCountCount n)

stringsByCount : ℕ → List String
stringsByCount zero =
  []
stringsByCount (suc n) =
  "synthetic" ∷ stringsByCount n

stringsByCountCount :
  (n : ℕ) →
  listCount (stringsByCount n) ≡ n
stringsByCountCount zero =
  refl
stringsByCountCount (suc n) =
  cong suc (stringsByCountCount n)

syntheticSymbolTable : K.Signature → SymbolTable
syntheticSymbolTable
  (K.signature
    classCount
    objectPropertyCount
    dataPropertyCount
    annotationPropertyCount
    datatypeCount
    facetCount
    individualCount
    iriCount
    blankNodeCount
    punningPolicy) =
  symbolTable
    (rawIRIsByCount classCount)
    (rawIRIsByCount objectPropertyCount)
    (rawIRIsByCount dataPropertyCount)
    (rawIRIsByCount annotationPropertyCount)
    (rawIRIsByCount datatypeCount)
    (rawIRIsByCount facetCount)
    (rawIRIsByCount individualCount)
    (rawIRIsByCount iriCount)
    (stringsByCount blankNodeCount)
    punningPolicy

syntheticSymbolTableSignature :
  (Sig : K.Signature) →
  symbolTableSignature (syntheticSymbolTable Sig) ≡ Sig
syntheticSymbolTableSignature Sig i =
  K.signature
    (rawIRIsByCountCount (K.classCount Sig) i)
    (rawIRIsByCountCount (K.objectPropertyCount Sig) i)
    (rawIRIsByCountCount (K.dataPropertyCount Sig) i)
    (rawIRIsByCountCount (K.annotationPropertyCount Sig) i)
    (rawIRIsByCountCount (K.datatypeCount Sig) i)
    (rawIRIsByCountCount (K.facetCount Sig) i)
    (rawIRIsByCountCount (K.individualCount Sig) i)
    (rawIRIsByCountCount (K.iriCount Sig) i)
    (stringsByCountCount (K.blankNodeCount Sig) i)
    (K.punningPolicy Sig)

record CheckedSourceTableRawTrace (table : SymbolTable) : Type₀ where
  constructor checkedSourceTableRawTrace
  field
    traceRaw :
      RawOntology
    traceTableFromRaw :
      table ≡ symbolTableFromRaw traceRaw
    traceProvenance :
      SourceProvenance
    traceProvenanceRecorded :
      traceProvenance ≡ provenance traceRaw

open CheckedSourceTableRawTrace public

record CheckedSourceTableTrace (Sig : K.Signature) : Type₀ where
  constructor checkedSourceTableTrace
  field
    traceTable :
      SymbolTable
    traceSignatureFromTable :
      symbolTableSignature traceTable ≡ Sig
    traceRawEvidence :
      Optional (CheckedSourceTableRawTrace traceTable)

open CheckedSourceTableTrace public

sourceTableTraceFromRaw :
  (raw : RawOntology) →
  CheckedSourceTableTrace (symbolTableSignature (symbolTableFromRaw raw))
sourceTableTraceFromRaw raw =
  checkedSourceTableTrace
    (symbolTableFromRaw raw)
    refl
    (present
      (checkedSourceTableRawTrace
        raw
        refl
        (provenance raw)
        refl))

syntheticSourceTableTrace :
  (Sig : K.Signature) →
  CheckedSourceTableTrace Sig
syntheticSourceTableTrace Sig =
  checkedSourceTableTrace
    (syntheticSymbolTable Sig)
    (syntheticSymbolTableSignature Sig)
    absent

record CheckedDeclarationEvidence (Sig : K.Signature) : Type₀ where
  constructor checkedDeclarationEvidence
  field
    declarationTrace :
      CheckedSourceTableTrace Sig
    declarationClassIRIs :
      List RawIRI
    declarationObjectPropertyIRIs :
      List RawIRI
    declarationDataPropertyIRIs :
      List RawIRI
    declarationAnnotationPropertyIRIs :
      List RawIRI
    declarationDatatypeIRIs :
      List RawIRI
    declarationIndividualIRIs :
      List RawIRI
    declarationClassIRIsRecorded :
      declarationClassIRIs ≡ classIRIs (traceTable declarationTrace)
    declarationObjectPropertyIRIsRecorded :
      declarationObjectPropertyIRIs ≡ objectPropertyIRIs (traceTable declarationTrace)
    declarationDataPropertyIRIsRecorded :
      declarationDataPropertyIRIs ≡ dataPropertyIRIs (traceTable declarationTrace)
    declarationAnnotationPropertyIRIsRecorded :
      declarationAnnotationPropertyIRIs ≡
      annotationPropertyIRIs (traceTable declarationTrace)
    declarationDatatypeIRIsRecorded :
      declarationDatatypeIRIs ≡ datatypeIRIs (traceTable declarationTrace)
    declarationIndividualIRIsRecorded :
      declarationIndividualIRIs ≡ individualIRIs (traceTable declarationTrace)
    declarationClassCount :
      ℕ
    declarationObjectPropertyCount :
      ℕ
    declarationDataPropertyCount :
      ℕ
    declarationAnnotationPropertyCount :
      ℕ
    declarationDatatypeCount :
      ℕ
    declarationIndividualCount :
      ℕ
    declarationClassCountRecorded :
      declarationClassCount ≡ K.classCount Sig
    declarationObjectPropertyCountRecorded :
      declarationObjectPropertyCount ≡ K.objectPropertyCount Sig
    declarationDataPropertyCountRecorded :
      declarationDataPropertyCount ≡ K.dataPropertyCount Sig
    declarationAnnotationPropertyCountRecorded :
      declarationAnnotationPropertyCount ≡ K.annotationPropertyCount Sig
    declarationDatatypeCountRecorded :
      declarationDatatypeCount ≡ K.datatypeCount Sig
    declarationIndividualCountRecorded :
      declarationIndividualCount ≡ K.individualCount Sig

open CheckedDeclarationEvidence public

completeDeclarationEvidence :
  {Sig : K.Signature} →
  CheckedSourceTableTrace Sig →
  CheckedDeclarationEvidence Sig
completeDeclarationEvidence trace =
  checkedDeclarationEvidence
    trace
    (classIRIs (traceTable trace))
    (objectPropertyIRIs (traceTable trace))
    (dataPropertyIRIs (traceTable trace))
    (annotationPropertyIRIs (traceTable trace))
    (datatypeIRIs (traceTable trace))
    (individualIRIs (traceTable trace))
    refl
    refl
    refl
    refl
    refl
    refl
    (listCount (classIRIs (traceTable trace)))
    (listCount (objectPropertyIRIs (traceTable trace)))
    (listCount (dataPropertyIRIs (traceTable trace)))
    (listCount (annotationPropertyIRIs (traceTable trace)))
    (listCount (datatypeIRIs (traceTable trace)))
    (listCount (individualIRIs (traceTable trace)))
    (cong K.classCount (traceSignatureFromTable trace))
    (cong K.objectPropertyCount (traceSignatureFromTable trace))
    (cong K.dataPropertyCount (traceSignatureFromTable trace))
    (cong K.annotationPropertyCount (traceSignatureFromTable trace))
    (cong K.datatypeCount (traceSignatureFromTable trace))
    (cong K.individualCount (traceSignatureFromTable trace))

syntheticDeclarationEvidence :
  (Sig : K.Signature) →
  CheckedDeclarationEvidence Sig
syntheticDeclarationEvidence Sig =
  completeDeclarationEvidence (syntheticSourceTableTrace Sig)

record CheckedPropertyRoleEvidence (Sig : K.Signature) : Type₀ where
  constructor checkedPropertyRoleEvidence
  field
    propertyRoleTrace :
      CheckedSourceTableTrace Sig
    roleObjectPropertyIRIs :
      List RawIRI
    roleDataPropertyIRIs :
      List RawIRI
    roleAnnotationPropertyIRIs :
      List RawIRI
    roleObjectPropertyIRIsRecorded :
      roleObjectPropertyIRIs ≡ objectPropertyIRIs (traceTable propertyRoleTrace)
    roleDataPropertyIRIsRecorded :
      roleDataPropertyIRIs ≡ dataPropertyIRIs (traceTable propertyRoleTrace)
    roleAnnotationPropertyIRIsRecorded :
      roleAnnotationPropertyIRIs ≡
      annotationPropertyIRIs (traceTable propertyRoleTrace)
    roleObjectPropertyCount :
      ℕ
    roleDataPropertyCount :
      ℕ
    roleAnnotationPropertyCount :
      ℕ
    roleObjectPropertyCountRecorded :
      roleObjectPropertyCount ≡ K.objectPropertyCount Sig
    roleDataPropertyCountRecorded :
      roleDataPropertyCount ≡ K.dataPropertyCount Sig
    roleAnnotationPropertyCountRecorded :
      roleAnnotationPropertyCount ≡ K.annotationPropertyCount Sig

open CheckedPropertyRoleEvidence public

completePropertyRoleEvidence :
  {Sig : K.Signature} →
  CheckedSourceTableTrace Sig →
  CheckedPropertyRoleEvidence Sig
completePropertyRoleEvidence trace =
  checkedPropertyRoleEvidence
    trace
    (objectPropertyIRIs (traceTable trace))
    (dataPropertyIRIs (traceTable trace))
    (annotationPropertyIRIs (traceTable trace))
    refl
    refl
    refl
    (listCount (objectPropertyIRIs (traceTable trace)))
    (listCount (dataPropertyIRIs (traceTable trace)))
    (listCount (annotationPropertyIRIs (traceTable trace)))
    (cong K.objectPropertyCount (traceSignatureFromTable trace))
    (cong K.dataPropertyCount (traceSignatureFromTable trace))
    (cong K.annotationPropertyCount (traceSignatureFromTable trace))

syntheticPropertyRoleEvidence :
  (Sig : K.Signature) →
  CheckedPropertyRoleEvidence Sig
syntheticPropertyRoleEvidence Sig =
  completePropertyRoleEvidence (syntheticSourceTableTrace Sig)

record CheckedImport : Type₀ where
  constructor checkedImport
  field
    policy :
      ImportPolicy
    signature :
      K.Signature
    ontology :
      K.Ontology signature
    sourceSemanticSupport :
      K.SourceOntologySemanticSupport signature (K.axioms ontology)
    sourceDeclarationEvidence :
      CheckedDeclarationEvidence signature
    sourcePropertyRoleEvidence :
      CheckedPropertyRoleEvidence signature
    policyEvidence :
      ImportPolicyEvidence policy
    sourceImportClosure :
      CheckedImportClosure

open CheckedImport public

CheckedEvidence : CheckedImport → EvidenceKind → Type₀
CheckedEvidence checked declarationEvidence =
  StoredEvidence (sourceDeclarationEvidence checked)
CheckedEvidence checked punningEvidence =
  K.punningPolicy (signature checked) ≡ K.noPunning
CheckedEvidence checked propertyRoleEvidence =
  StoredEvidence (sourcePropertyRoleEvidence checked)
CheckedEvidence checked datatypeEvidence =
  StoredEvidence (K.datatypeSupport (ontology checked))
CheckedEvidence checked importClosureEvidence =
  StoredEvidence (sourceImportClosure checked)
CheckedEvidence checked semanticSupportEvidence =
  StoredEvidence (sourceSemanticSupport checked)
CheckedEvidence checked annotationErasureEvidence =
  StoredEvidence (K.annotationErasure (ontology checked))
CheckedEvidence checked profileEvidence =
  Unit
CheckedEvidence checked regularityEvidence =
  StoredEvidence (K.regularity (ontology checked))

record CheckedSourceEvidence (checked : CheckedImport) : Type₀ where
  constructor checkedSourceEvidence
  field
    sourcePolicyEvidence :
      StoredEvidence (policyEvidence checked)
    sourceDeclarations :
      CheckedEvidence checked declarationEvidence
    sourcePropertyRoles :
      CheckedEvidence checked propertyRoleEvidence
    sourceDatatypeMap :
      CheckedEvidence checked datatypeEvidence
    sourceImportClosureEvidence :
      CheckedEvidence checked importClosureEvidence
    sourceSemanticSupportEvidence :
      CheckedEvidence checked semanticSupportEvidence
    sourceAnnotationErased :
      CheckedEvidence checked annotationErasureEvidence
    sourceRegularityEvidence :
      CheckedEvidence checked regularityEvidence

open CheckedSourceEvidence public

checkedSourceEvidenceOf : (checked : CheckedImport) → CheckedSourceEvidence checked
checkedSourceEvidenceOf checked =
  checkedSourceEvidence
    (storedEvidenceOf (policyEvidence checked))
    (storedEvidenceOf (sourceDeclarationEvidence checked))
    (storedEvidenceOf (sourcePropertyRoleEvidence checked))
    (storedEvidenceOf (K.datatypeSupport (ontology checked)))
    (storedEvidenceOf (sourceImportClosure checked))
    (storedEvidenceOf (sourceSemanticSupport checked))
    (storedEvidenceOf (K.annotationErasure (ontology checked)))
    (storedEvidenceOf (K.regularity (ontology checked)))

checkedPunningEvidence? :
  (checked : CheckedImport) →
  Optional (CheckedEvidence checked punningEvidence)
checkedPunningEvidence? checked with K.punningPolicy (signature checked)
... | K.noPunning =
  present refl
... | K.allowDeclaredPunning =
  absent

checkedEvidenceBundle : CheckedImport → EvidenceBundle CheckedImport CheckedEvidence
checkedEvidenceBundle checked =
  evidenceBundle
    checked
    (present (storedEvidenceOf (sourceDeclarationEvidence checked)))
    (checkedPunningEvidence? checked)
    (present (storedEvidenceOf (sourcePropertyRoleEvidence checked)))
    (present (storedEvidenceOf (K.datatypeSupport (ontology checked))))
    (present (storedEvidenceOf (sourceImportClosure checked)))
    (present (storedEvidenceOf (sourceSemanticSupport checked)))
    (present (storedEvidenceOf (K.annotationErasure (ontology checked))))
    absent
    (present (storedEvidenceOf (K.regularity (ontology checked))))