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

module OWL2.Corpus.Accepted.Kernel where

open import OWL2.Prelude
import OWL2.Check.Bundle as Bundle
open import OWL2.Foundation.List using (all[]; all∷; listCount)
import OWL2.Elab.CheckedImport as CI
open import OWL2.Elab.Policy
open import OWL2.Kernel.Signature
open import OWL2.Kernel.Name
open import OWL2.Kernel.DatatypeMap
open import OWL2.Kernel.Regularity
open import OWL2.Kernel.Syntax
open import OWL2.Kernel.SemanticSupport
open import OWL2.Kernel.Semantics
open import OWL2.Semantics.Complete

kernelSemanticsSignature : Signature
kernelSemanticsSignature =
  signature          noPunning

mainClass : ClassName kernelSemanticsSignature
mainClass =
  className fzero

leftClass : ClassName kernelSemanticsSignature
leftClass =
  className (fsuc fzero)

rightClass : ClassName kernelSemanticsSignature
rightClass =
  className (fsuc (fsuc fzero))

keyDataPropertyName : DataPropertyName kernelSemanticsSignature
keyDataPropertyName =
  dataPropertyName fzero

unusedObjectPropertyName : ObjectPropertyName kernelSemanticsSignature
unusedObjectPropertyName =
  objectPropertyName fzero

kernelDatatypeName : DatatypeName kernelSemanticsSignature
kernelDatatypeName =
  datatypeName fzero

kernelIndividualName : IndividualName kernelSemanticsSignature
kernelIndividualName =
  individualName fzero

data KernelObject : Type₀ where
  leftObject :
    KernelObject
  rightObject :
    KernelObject

data KernelData : Type₀ where
  sharedKeyValue :
    KernelData

data MainMember : KernelObject → Type₀ where
  leftInMain :
    MainMember leftObject
  rightInMain :
    MainMember rightObject

data LeftMember : KernelObject → Type₀ where
  leftInLeft :
    LeftMember leftObject

data RightMember : KernelObject → Type₀ where
  rightInRight :
    RightMember rightObject

kernelClassDenotation :
  ClassName kernelSemanticsSignature →
  KernelObject →
  Type₀
kernelClassDenotation (scopedName fzero) =
  MainMember
kernelClassDenotation (scopedName (fsuc fzero)) =
  LeftMember
kernelClassDenotation (scopedName (fsuc (fsuc fzero))) =
  RightMember
kernelClassDenotation (scopedName (fsuc (fsuc (fsuc ()))))

kernelObjectPropertyDenotation :
  ObjectPropertyName kernelSemanticsSignature →
  KernelObject →
  KernelObject →
  Type₀
kernelObjectPropertyDenotation (scopedName fzero) x y =
  ⊥
kernelObjectPropertyDenotation (scopedName (fsuc ())) x y

data SharedIdentifier : KernelObject → KernelData → Type₀ where
  leftIdentifier :
    SharedIdentifier leftObject sharedKeyValue

kernelDataPropertyDenotation :
  DataPropertyName kernelSemanticsSignature →
  KernelObject →
  KernelData →
  Type₀
kernelDataPropertyDenotation (scopedName fzero) =
  SharedIdentifier
kernelDataPropertyDenotation (scopedName (fsuc ()))

kernelIndividualDenotation :
  IndividualName kernelSemanticsSignature →
  KernelObject
kernelIndividualDenotation (scopedName fzero) =
  leftObject
kernelIndividualDenotation (scopedName (fsuc ()))

kernelLiteralDenotation :
  Literal kernelSemanticsSignature →
  KernelData
kernelLiteralDenotation literal =
  sharedKeyValue

kernelDatatypeDenotation :
  DatatypeName kernelSemanticsSignature →
  KernelData →
  Type₀
kernelDatatypeDenotation (scopedName fzero) sharedKeyValue =
  Unit
kernelDatatypeDenotation (scopedName (fsuc ())) value

kernelFacetRestrictionDenotation :
  FacetRestriction kernelSemanticsSignature →
  KernelData →
  Type₀
kernelFacetRestrictionDenotation restriction value =
  Unit

kernelSemanticsInterpretation : Interpretation kernelSemanticsSignature
kernelSemanticsInterpretation =
  kernelInterpretation
    KernelObject
    KernelData
    kernelClassDenotation
    kernelObjectPropertyDenotation
    kernelDataPropertyDenotation
    kernelIndividualDenotation
    kernelLiteralDenotation
    kernelDatatypeDenotation
    kernelFacetRestrictionDenotation

leftRightDisjoint :
  DisjointClassExpressions
    kernelSemanticsInterpretation
    (namedClass leftClass)
    (namedClass rightClass)
leftRightDisjoint leftObject leftInLeft ()
leftRightDisjoint rightObject () rightInRight

kernelDisjointUnionSatisfied :
  SatisfiesAxiom kernelSemanticsInterpretation
    (disjointUnion
      mainClass
      (atLeastTwo (namedClass leftClass) (namedClass rightClass) []))
kernelDisjointUnionSatisfied =
  equivalence , disjoint
  where
  mainToUnion :
    ClassSubsumes
      kernelSemanticsInterpretation
      (namedClass mainClass)
      (objectUnionOf
        (nonEmpty (namedClass leftClass) (namedClass rightClass ∷ [])))
  mainToUnion leftObject leftInMain =
    inl leftInLeft
  mainToUnion rightObject rightInMain =
    inr (inl rightInRight)

  unionToMain :
    ClassSubsumes
      kernelSemanticsInterpretation
      (objectUnionOf
        (nonEmpty (namedClass leftClass) (namedClass rightClass ∷ [])))
      (namedClass mainClass)
  unionToMain leftObject (inl leftInLeft) =
    leftInMain
  unionToMain leftObject (inr (inl ()))
  unionToMain leftObject (inr (inr ()))
  unionToMain rightObject (inl ())
  unionToMain rightObject (inr (inl rightInRight)) =
    rightInMain
  unionToMain rightObject (inr (inr ()))

  equivalence :
    EquivalentClassExpressions
      kernelSemanticsInterpretation
      (namedClass mainClass)
      (objectUnionOf
        (nonEmpty (namedClass leftClass) (namedClass rightClass ∷ [])))
  equivalence =
    mainToUnion , unionToMain

  disjoint :
    Pairwise
      (DisjointClassExpressions kernelSemanticsInterpretation)
      (namedClass leftClass ∷ namedClass rightClass ∷ [])
  disjoint =
    (leftRightDisjoint , tt) , (tt , tt)

kernelPropertyKey : PropertyKey kernelSemanticsSignature
kernelPropertyKey =
  propertyKey [] (dataProperty keyDataPropertyName ∷ [])

kernelHasKeySatisfied :
  SatisfiesAxiom kernelSemanticsInterpretation
    (hasKey (namedClass leftClass) kernelPropertyKey)
kernelHasKeySatisfied leftObject leftObject leftInLeft leftInLeft shared =
  refl
kernelHasKeySatisfied leftObject rightObject leftInLeft () shared
kernelHasKeySatisfied rightObject leftObject () leftInLeft shared
kernelHasKeySatisfied rightObject rightObject () () shared

kernelDatatypeDefinitionSatisfied :
  SatisfiesAxiom kernelSemanticsInterpretation
    (datatypeDefinition
      kernelDatatypeName
      (trivialDatatypeSupported kernelDatatypeName)
      (datatype
        kernelDatatypeName
        (trivialDatatypeSupported kernelDatatypeName)))
kernelDatatypeDefinitionSatisfied =
  (λ value member → member) , (λ value member → member)

kernelSemanticAxioms : List (Axiom kernelSemanticsSignature)
kernelSemanticAxioms =
  disjointUnion
    mainClass
    (atLeastTwo (namedClass leftClass) (namedClass rightClass) [])
  ∷ hasKey (namedClass leftClass) kernelPropertyKey
  ∷ datatypeDefinition
      kernelDatatypeName
      (trivialDatatypeSupported kernelDatatypeName)
      (datatype
        kernelDatatypeName
        (trivialDatatypeSupported kernelDatatypeName))
  ∷ []

kernelSemanticAxiomsSupported :
  OntologyAxiomsSemanticSupport kernelSemanticAxioms
kernelSemanticAxiomsSupported =
  (tt , (tt , tt)) , (tt , (tt , tt))

kernelSemanticSupport :
  SourceOntologySemanticSupport kernelSemanticsSignature kernelSemanticAxioms
kernelSemanticSupport =
  sourceOntologySemanticSupport
    kernelSemanticAxioms
    refl
    kernelSemanticAxiomsSupported

kernelSemanticAxiomsChainFree :
  AxiomsPropertyChainFree kernelSemanticAxioms
kernelSemanticAxiomsChainFree =
  tt , (tt , (tt , tt))

kernelSemanticAnnotatedBodiesAppend :
  annotatedBodies
    (plainAnnotatedAxioms kernelSemanticAxioms ++
     plainAnnotatedAxioms kernelSemanticAxioms) ≡
  kernelSemanticAxioms ++ kernelSemanticAxioms
kernelSemanticAnnotatedBodiesAppend =
  annotatedBodiesAppend
    (plainAnnotatedAxioms kernelSemanticAxioms)
    (plainAnnotatedAxioms kernelSemanticAxioms)

kernelSemanticAxiomsChainFreeAppend :
  AxiomsPropertyChainFree
    (kernelSemanticAxioms ++ kernelSemanticAxioms)
kernelSemanticAxiomsChainFreeAppend =
  axiomsPropertyChainFreeAppend
    kernelSemanticAxioms
    kernelSemanticAxioms
    kernelSemanticAxiomsChainFree
    kernelSemanticAxiomsChainFree

kernelSemanticOntology : Ontology kernelSemanticsSignature
kernelSemanticOntology =
  plainOntology
    kernelSemanticAxioms
    (completeOntologyDatatypeSupport kernelSemanticAxioms)
    (ontologyRegularity
      trivialRegularityContext
      kernelSemanticAxiomsChainFree)

kernelSemanticOntologyAppended : Ontology kernelSemanticsSignature
kernelSemanticOntologyAppended =
  appendOntologies
    trivialRegularityContext
    kernelSemanticOntology
    kernelSemanticOntology

kernelSemanticOntologyAppendedAxiomCount :
  listCount (axioms kernelSemanticOntologyAppended) ≡
  
kernelSemanticOntologyAppendedAxiomCount =
  refl

kernelSemanticOntologyAppendedAnnotationErasure :
  annotatedBodies (annotatedAxioms kernelSemanticOntologyAppended) ≡
  axioms kernelSemanticOntologyAppended
kernelSemanticOntologyAppendedAnnotationErasure =
  annotationErasure kernelSemanticOntologyAppended

kernelCheckedImport : CI.CheckedImport
kernelCheckedImport =
  CI.checkedImport
    strictPolicy
    kernelSemanticsSignature
    kernelSemanticOntology
    kernelSemanticSupport
    (CI.syntheticDeclarationEvidence kernelSemanticsSignature)
    (CI.syntheticPropertyRoleEvidence kernelSemanticsSignature)
    (trivialPolicyEvidence strictPolicy)
    CI.noImportClosure

kernelCheckedSourceEvidence : CI.CheckedSourceEvidence kernelCheckedImport
kernelCheckedSourceEvidence =
  CI.checkedSourceEvidenceOf kernelCheckedImport

kernelSemanticOntologySatisfied :
  SatisfiesOntology kernelSemanticsInterpretation kernelSemanticOntology
kernelSemanticOntologySatisfied =
  all∷
    kernelDisjointUnionSatisfied
    (all∷
      kernelHasKeySatisfied
      (all∷
        kernelDatatypeDefinitionSatisfied
        all[]))

kernelModelOfCheckedImport :
  ModelOfCheckedImport
    kernelCheckedImport
    (Bundle.storedEvidenceOf kernelSemanticSupport)
    kernelSemanticsInterpretation
kernelModelOfCheckedImport =
  kernelSemanticOntologySatisfied

kernelCheckedImportModel : CheckedImportModel kernelCheckedImport
kernelCheckedImportModel =
  checkedImportModel
    (Bundle.storedEvidenceOf kernelSemanticSupport)
    kernelSemanticsInterpretation
    kernelSemanticOntologySatisfied

kernelModelOfCompleteCheckedImport :
  ModelOfCompleteCheckedImport
    kernelCheckedImport
    kernelCheckedSourceEvidence
    kernelSemanticsInterpretation
kernelModelOfCompleteCheckedImport =
  kernelSemanticOntologySatisfied

kernelCompleteCheckedImportModel :
  CompleteCheckedImportModel kernelCheckedImport
kernelCompleteCheckedImportModel =
  completeCheckedImportModel
    kernelCheckedSourceEvidence
    kernelSemanticsInterpretation
    kernelSemanticOntologySatisfied

punningAllowedSignature : Signature
punningAllowedSignature =
  signature          allowDeclaredPunning

punningAllowedOntology : Ontology punningAllowedSignature
punningAllowedOntology =
  emptyOntology
    (completeOntologyDatatypeSupport [])
    (ontologyRegularity trivialRegularityContext tt)

punningAllowedCheckedImport : CI.CheckedImport
punningAllowedCheckedImport =
  CI.checkedImport
    strictPolicy
    punningAllowedSignature
    punningAllowedOntology
    (completeSourceOntologySemanticSupport [])
    (CI.syntheticDeclarationEvidence punningAllowedSignature)
    (CI.syntheticPropertyRoleEvidence punningAllowedSignature)
    (trivialPolicyEvidence strictPolicy)
    CI.noImportClosure

punningAllowedEvidenceBundle :
  Bundle.EvidenceBundle CI.CheckedImport CI.CheckedEvidence
punningAllowedEvidenceBundle =
  CI.checkedEvidenceBundle punningAllowedCheckedImport

punningAllowedBundlePunningAbsent :
  Bundle.punning punningAllowedEvidenceBundle ≡ absent
punningAllowedBundlePunningAbsent =
  refl