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

module OWL2.Examples.WebProtege.Countermodels where

open import OWL2.Prelude
import Cubical.Data.Prod.Base as Prod
open import OWL2.Syntax
open import OWL2.DirectSemantics
open import OWL2.DirectSemantics.Lemmas using (disjointClassesFirst)

import OWL2.Examples.WebProtege.Corpus as Corpus

ReverseTaxonomyTarget : Ontology Corpus.WebProtegeSignature
ReverseTaxonomyTarget =
  ontology
    []
    []
    ( subClassOf Corpus.DatasetC Corpus.CuratedDatasetC
    ∷ [] )

reverseTaxonomyTargetRejectedByCorpusModel :
  ¬ Model Corpus.webProtegeInterpretation ReverseTaxonomyTarget
reverseTaxonomyTargetRejectedByCorpusModel targetModel =
  Corpus.draftDatasetNotCurated
    (datasetSubCurated
      Corpus.draftDatasetObject
      Corpus.draftDatasetDataset)
  where
  datasetSubCurated :
    SatisfiesAxiom Corpus.webProtegeInterpretation
      (subClassOf Corpus.DatasetC Corpus.CuratedDatasetC)
  datasetSubCurated =
    Prod.proj₁ targetModel

reverseTaxonomyCountermodel :
  Model Corpus.webProtegeInterpretation Corpus.webProtegeOntology ×
  (¬ Model Corpus.webProtegeInterpretation ReverseTaxonomyTarget)
reverseTaxonomyCountermodel =
  Corpus.webProtegeModel ,
  reverseTaxonomyTargetRejectedByCorpusModel

webProtegeDoesNotEntailReverseTaxonomy :
  ¬ Entails {ℓObj = ℓ-zero} {ℓData = ℓ-zero} {ℓSem = ℓ-zero}
      Corpus.webProtegeOntology
      ReverseTaxonomyTarget
webProtegeDoesNotEntailReverseTaxonomy entails =
  reverseTaxonomyTargetRejectedByCorpusModel
    (entails Corpus.webProtegeInterpretation Corpus.webProtegeModel)

DraftCuratedTarget : Ontology Corpus.WebProtegeSignature
DraftCuratedTarget =
  ontology
    []
    []
    ( classAssertion Corpus.CuratedDatasetC Corpus.draftDataset
    ∷ [] )

draftCuratedTargetRejectedByCorpusModel :
  ¬ Model Corpus.webProtegeInterpretation DraftCuratedTarget
draftCuratedTargetRejectedByCorpusModel targetModel =
  Corpus.draftDatasetNotCurated (Prod.proj₁ targetModel)

draftCuratedCountermodel :
  Model Corpus.webProtegeInterpretation Corpus.webProtegeOntology ×
  (¬ Model Corpus.webProtegeInterpretation DraftCuratedTarget)
draftCuratedCountermodel =
  Corpus.webProtegeModel ,
  draftCuratedTargetRejectedByCorpusModel

webProtegeDoesNotEntailDraftCurated :
  ¬ Entails {ℓObj = ℓ-zero} {ℓData = ℓ-zero} {ℓSem = ℓ-zero}
      Corpus.webProtegeOntology
      DraftCuratedTarget
webProtegeDoesNotEntailDraftCurated entails =
  draftCuratedTargetRejectedByCorpusModel
    (entails Corpus.webProtegeInterpretation Corpus.webProtegeModel)

DatasetContributorDisjointConflict :
  Ontology Corpus.WebProtegeSignature
DatasetContributorDisjointConflict =
  ontology
    (Corpus.webProtegeDocument ∷ [])
    []
    ( disjointClasses (Corpus.DatasetC ∷ Corpus.ContributorC ∷ [])
    ∷ classAssertion Corpus.DatasetC Corpus.datasetOne
    ∷ classAssertion Corpus.ContributorC Corpus.datasetOne
    ∷ [] )

datasetContributorDisjointConflictNoModel :
  ∀ {ℓObj ℓData ℓSem}
  (I : Interpretation Corpus.WebProtegeSignature ℓObj ℓData ℓSem) →
  ¬ Model I DatasetContributorDisjointConflict
datasetContributorDisjointConflictNoModel I model =
  datasetDisjointContributor
    (individualDenotation I Corpus.datasetOne)
    datasetOneDataset
    datasetOneContributor
  where
  datasetContributorDisjoint :
    SatisfiesAxiom I
      (disjointClasses (Corpus.DatasetC ∷ Corpus.ContributorC ∷ []))
  datasetContributorDisjoint =
    Prod.proj₁ model

  datasetDisjointContributor :
    Disjoint
      (evalClass I Corpus.DatasetC)
      (evalClass I Corpus.ContributorC)
  datasetDisjointContributor =
    disjointClassesFirst
      {I = I}
      {c = Corpus.DatasetC}
      {d = Corpus.ContributorC}
      {cs = []}
      datasetContributorDisjoint

  afterDisjoint :
    AllList
      ( classAssertion Corpus.DatasetC Corpus.datasetOne
      ∷ classAssertion Corpus.ContributorC Corpus.datasetOne
      ∷ [] )
      (SatisfiesAxiom I)
  afterDisjoint =
    Prod.proj₂ model

  datasetOneDataset :
    evalClass I Corpus.DatasetC (individualDenotation I Corpus.datasetOne)
  datasetOneDataset =
    Prod.proj₁ afterDisjoint

  datasetOneContributor :
    evalClass I Corpus.ContributorC (individualDenotation I Corpus.datasetOne)
  datasetOneContributor =
    Prod.proj₁ (Prod.proj₂ afterDisjoint)

AtLeastOneContributorCurator MaxZeroContributorCurators :
  ClassExpression Corpus.WebProtegeSignature
AtLeastOneContributorCurator =
  objectMinCardinality
    
    Corpus.HasCurator
    (present Corpus.ContributorC)
MaxZeroContributorCurators =
  objectMaxCardinality
    
    Corpus.HasCurator
    (present Corpus.ContributorC)

CuratorCardinalityConflict : Ontology Corpus.WebProtegeSignature
CuratorCardinalityConflict =
  ontology
    (Corpus.webProtegeDocument ∷ [])
    []
    ( classAssertion AtLeastOneContributorCurator Corpus.datasetOne
    ∷ classAssertion MaxZeroContributorCurators Corpus.datasetOne
    ∷ [] )

curatorCardinalityConflictNoModel :
  ∀ {ℓObj ℓData ℓSem}
  (I : Interpretation Corpus.WebProtegeSignature ℓObj ℓData ℓSem) →
  ¬ Model I CuratorCardinalityConflict
curatorCardinalityConflictNoModel I model =
  maxZeroContributorCurators atLeastOneContributorCurator
  where
  atLeastOneContributorCurator :
    evalClass I AtLeastOneContributorCurator
      (individualDenotation I Corpus.datasetOne)
  atLeastOneContributorCurator =
    Prod.proj₁ model

  maxZeroContributorCurators :
    evalClass I MaxZeroContributorCurators
      (individualDenotation I Corpus.datasetOne)
  maxZeroContributorCurators =
    Prod.proj₁ (Prod.proj₂ model)

NoDataProperty : DataPropertyExpression Corpus.WebProtegeSignature
NoDataProperty =
  dataProperty Corpus.noDataProperty

NoDatatypeRange NoDatatypeSelfComplement :
  DataRange Corpus.WebProtegeSignature
NoDatatypeRange =
  datatype Corpus.noDatatype
NoDatatypeSelfComplement =
  dataIntersectionOf
    ( NoDatatypeRange
    ∷ dataComplementOf NoDatatypeRange
    ∷ [] )

DataRangeSelfComplementConflict : Ontology Corpus.WebProtegeSignature
DataRangeSelfComplementConflict =
  ontology
    (Corpus.webProtegeDocument ∷ [])
    []
    ( dataPropertyRange NoDataProperty NoDatatypeSelfComplement
    ∷ dataPropertyAssertion
        NoDataProperty
        Corpus.datasetOne
        Corpus.noLiteral
    ∷ [] )

dataRangeSelfComplementConflictNoModel :
  ∀ {ℓObj ℓData ℓSem}
  (I : Interpretation Corpus.WebProtegeSignature ℓObj ℓData ℓSem) →
  ¬ Model I DataRangeSelfComplementConflict
dataRangeSelfComplementConflictNoModel I model =
  notInNoDatatype inNoDatatype
  where
  rangeAxiom :
    SatisfiesAxiom I
      (dataPropertyRange NoDataProperty NoDatatypeSelfComplement)
  rangeAxiom =
    Prod.proj₁ model

  dataAssertion :
    evalDataProperty I
      NoDataProperty
      (individualDenotation I Corpus.datasetOne)
      (literalDenotation I Corpus.noLiteral)
  dataAssertion =
    Prod.proj₁ (Prod.proj₂ model)

  contradictoryRange :
    evalDataRange I
      NoDatatypeSelfComplement
      (literalDenotation I Corpus.noLiteral)
  contradictoryRange =
    rangeAxiom
      (individualDenotation I Corpus.datasetOne)
      (literalDenotation I Corpus.noLiteral)
      dataAssertion

  inNoDatatype :
    evalDataRange I NoDatatypeRange (literalDenotation I Corpus.noLiteral)
  inNoDatatype =
    fst contradictoryRange

  notInNoDatatype :
    ¬ evalDataRange I NoDatatypeRange (literalDenotation I Corpus.noLiteral)
  notInNoDatatype =
    fst (snd contradictoryRange)