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

module OWL2.Kernel.SemanticSupport where

open import OWL2.Prelude
open import OWL2.Foundation.List hiding (NonEmpty)
open import OWL2.Kernel.Syntax

ListSemanticSupport :
  {A : Type₀} →
  (A → Type₀) →
  List A →
  Type₀
ListSemanticSupport P [] =
  Unit
ListSemanticSupport P (x ∷ xs) =
  P x × ListSemanticSupport P xs

NonEmptySemanticSupport :
  {A : Type₀} →
  (A → Type₀) →
  NonEmpty A →
  Type₀
NonEmptySemanticSupport P (nonEmpty head tail) =
  P head × ListSemanticSupport P tail

AtLeastTwoSemanticSupport :
  {A : Type₀} →
  (A → Type₀) →
  AtLeastTwo A →
  Type₀
AtLeastTwoSemanticSupport P (atLeastTwo first second rest) =
  P first × P second × ListSemanticSupport P rest

FacetRestrictionSemanticSupport :
  {Sig : Signature} →
  FacetRestriction Sig →
  Type₀
FacetRestrictionSemanticSupport restriction =
  Unit

completeListSemanticSupport :
  {A : Type₀} →
  {P : A → Type₀} →
  ((x : A) → P x) →
  (xs : List A) →
  ListSemanticSupport P xs
completeListSemanticSupport complete [] =
  tt
completeListSemanticSupport complete (x ∷ xs) =
  complete x , completeListSemanticSupport complete xs

completeAtLeastTwoSemanticSupport :
  {A : Type₀} →
  {P : A → Type₀} →
  ((x : A) → P x) →
  (xs : AtLeastTwo A) →
  AtLeastTwoSemanticSupport P xs
completeAtLeastTwoSemanticSupport complete (atLeastTwo first second rest) =
  complete first , complete second , completeListSemanticSupport complete rest

completeFacetRestrictionSemanticSupport :
  {Sig : Signature} →
  (restriction : FacetRestriction Sig) →
  FacetRestrictionSemanticSupport restriction
completeFacetRestrictionSemanticSupport restriction =
  tt

mutual
  DataRangeSemanticSupport :
    {Sig : Signature} →
    DataRange Sig →
    Type₀
  DataRangeSemanticSupport (datatype name support) =
    Unit
  DataRangeSemanticSupport dataTop =
    Unit
  DataRangeSemanticSupport dataBottom =
    Unit
  DataRangeSemanticSupport (dataComplementOf range) =
    DataRangeSemanticSupport range
  DataRangeSemanticSupport (dataIntersectionOf (nonEmpty head tail)) =
    DataRangeSemanticSupport head × DataRangeSemanticSupportList tail
  DataRangeSemanticSupport (dataUnionOf (nonEmpty head tail)) =
    DataRangeSemanticSupport head × DataRangeSemanticSupportList tail
  DataRangeSemanticSupport (dataOneOf literals) =
    Unit
  DataRangeSemanticSupport (datatypeRestriction name support facets) =
    ListSemanticSupport FacetRestrictionSemanticSupport facets

  DataRangeSemanticSupportList :
    {Sig : Signature} →
    List (DataRange Sig) →
    Type₀
  DataRangeSemanticSupportList [] =
    Unit
  DataRangeSemanticSupportList (range ∷ ranges) =
    DataRangeSemanticSupport range × DataRangeSemanticSupportList ranges

  OptionalDataRangeSemanticSupport :
    {Sig : Signature} →
    Optional (DataRange Sig) →
    Type₀
  OptionalDataRangeSemanticSupport absent =
    Unit
  OptionalDataRangeSemanticSupport (present range) =
    DataRangeSemanticSupport range

  completeDataRangeSemanticSupport :
    {Sig : Signature} →
    (range : DataRange Sig) →
    DataRangeSemanticSupport range
  completeDataRangeSemanticSupport (datatype name support) =
    tt
  completeDataRangeSemanticSupport dataTop =
    tt
  completeDataRangeSemanticSupport dataBottom =
    tt
  completeDataRangeSemanticSupport (dataComplementOf range) =
    completeDataRangeSemanticSupport range
  completeDataRangeSemanticSupport (dataIntersectionOf (nonEmpty head tail)) =
    completeDataRangeSemanticSupport head ,
    completeDataRangeSemanticSupportList tail
  completeDataRangeSemanticSupport (dataUnionOf (nonEmpty head tail)) =
    completeDataRangeSemanticSupport head ,
    completeDataRangeSemanticSupportList tail
  completeDataRangeSemanticSupport (dataOneOf literals) =
    tt
  completeDataRangeSemanticSupport (datatypeRestriction name support facets) =
    completeListSemanticSupport completeFacetRestrictionSemanticSupport facets

  completeDataRangeSemanticSupportList :
    {Sig : Signature} →
    (ranges : List (DataRange Sig)) →
    DataRangeSemanticSupportList ranges
  completeDataRangeSemanticSupportList [] =
    tt
  completeDataRangeSemanticSupportList (range ∷ ranges) =
    completeDataRangeSemanticSupport range ,
    completeDataRangeSemanticSupportList ranges

  completeOptionalDataRangeSemanticSupport :
    {Sig : Signature} →
    (range : Optional (DataRange Sig)) →
    OptionalDataRangeSemanticSupport range
  completeOptionalDataRangeSemanticSupport absent =
    tt
  completeOptionalDataRangeSemanticSupport (present range) =
    completeDataRangeSemanticSupport range

  ClassExpressionSemanticSupport :
    {Sig : Signature} →
    ClassExpression Sig →
    Type₀
  ClassExpressionSemanticSupport (namedClass name) =
    Unit
  ClassExpressionSemanticSupport owlThing =
    Unit
  ClassExpressionSemanticSupport owlNothing =
    Unit
  ClassExpressionSemanticSupport (objectIntersectionOf (nonEmpty head tail)) =
    ClassExpressionSemanticSupport head × ClassExpressionSemanticSupportList tail
  ClassExpressionSemanticSupport (objectUnionOf (nonEmpty head tail)) =
    ClassExpressionSemanticSupport head × ClassExpressionSemanticSupportList tail
  ClassExpressionSemanticSupport (objectComplementOf class) =
    ClassExpressionSemanticSupport class
  ClassExpressionSemanticSupport (objectOneOf individuals) =
    Unit
  ClassExpressionSemanticSupport (objectSomeValuesFrom property class) =
    ClassExpressionSemanticSupport class
  ClassExpressionSemanticSupport (objectAllValuesFrom property class) =
    ClassExpressionSemanticSupport class
  ClassExpressionSemanticSupport (objectHasValue property individual) =
    Unit
  ClassExpressionSemanticSupport (objectHasSelf property) =
    Unit
  ClassExpressionSemanticSupport (objectMinCardinality n property class) =
    OptionalClassExpressionSemanticSupport class
  ClassExpressionSemanticSupport (objectMaxCardinality n property class) =
    OptionalClassExpressionSemanticSupport class
  ClassExpressionSemanticSupport (objectExactCardinality n property class) =
    OptionalClassExpressionSemanticSupport class
  ClassExpressionSemanticSupport (dataSomeValuesFrom property range) =
    DataRangeSemanticSupport range
  ClassExpressionSemanticSupport (dataAllValuesFrom property range) =
    DataRangeSemanticSupport range
  ClassExpressionSemanticSupport (dataHasValue property literal) =
    Unit
  ClassExpressionSemanticSupport (dataMinCardinality n property range) =
    OptionalDataRangeSemanticSupport range
  ClassExpressionSemanticSupport (dataMaxCardinality n property range) =
    OptionalDataRangeSemanticSupport range
  ClassExpressionSemanticSupport (dataExactCardinality n property range) =
    OptionalDataRangeSemanticSupport range

  ClassExpressionSemanticSupportList :
    {Sig : Signature} →
    List (ClassExpression Sig) →
    Type₀
  ClassExpressionSemanticSupportList [] =
    Unit
  ClassExpressionSemanticSupportList (class ∷ classes) =
    ClassExpressionSemanticSupport class × ClassExpressionSemanticSupportList classes

  OptionalClassExpressionSemanticSupport :
    {Sig : Signature} →
    Optional (ClassExpression Sig) →
    Type₀
  OptionalClassExpressionSemanticSupport absent =
    Unit
  OptionalClassExpressionSemanticSupport (present class) =
    ClassExpressionSemanticSupport class

  completeClassExpressionSemanticSupport :
    {Sig : Signature} →
    (class : ClassExpression Sig) →
    ClassExpressionSemanticSupport class
  completeClassExpressionSemanticSupport (namedClass name) =
    tt
  completeClassExpressionSemanticSupport owlThing =
    tt
  completeClassExpressionSemanticSupport owlNothing =
    tt
  completeClassExpressionSemanticSupport (objectIntersectionOf (nonEmpty head tail)) =
    completeClassExpressionSemanticSupport head ,
    completeClassExpressionSemanticSupportList tail
  completeClassExpressionSemanticSupport (objectUnionOf (nonEmpty head tail)) =
    completeClassExpressionSemanticSupport head ,
    completeClassExpressionSemanticSupportList tail
  completeClassExpressionSemanticSupport (objectComplementOf class) =
    completeClassExpressionSemanticSupport class
  completeClassExpressionSemanticSupport (objectOneOf individuals) =
    tt
  completeClassExpressionSemanticSupport (objectSomeValuesFrom property class) =
    completeClassExpressionSemanticSupport class
  completeClassExpressionSemanticSupport (objectAllValuesFrom property class) =
    completeClassExpressionSemanticSupport class
  completeClassExpressionSemanticSupport (objectHasValue property individual) =
    tt
  completeClassExpressionSemanticSupport (objectHasSelf property) =
    tt
  completeClassExpressionSemanticSupport (objectMinCardinality n property class) =
    completeOptionalClassExpressionSemanticSupport class
  completeClassExpressionSemanticSupport (objectMaxCardinality n property class) =
    completeOptionalClassExpressionSemanticSupport class
  completeClassExpressionSemanticSupport (objectExactCardinality n property class) =
    completeOptionalClassExpressionSemanticSupport class
  completeClassExpressionSemanticSupport (dataSomeValuesFrom property range) =
    completeDataRangeSemanticSupport range
  completeClassExpressionSemanticSupport (dataAllValuesFrom property range) =
    completeDataRangeSemanticSupport range
  completeClassExpressionSemanticSupport (dataHasValue property literal) =
    tt
  completeClassExpressionSemanticSupport (dataMinCardinality n property range) =
    completeOptionalDataRangeSemanticSupport range
  completeClassExpressionSemanticSupport (dataMaxCardinality n property range) =
    completeOptionalDataRangeSemanticSupport range
  completeClassExpressionSemanticSupport (dataExactCardinality n property range) =
    completeOptionalDataRangeSemanticSupport range

  completeClassExpressionSemanticSupportList :
    {Sig : Signature} →
    (classes : List (ClassExpression Sig)) →
    ClassExpressionSemanticSupportList classes
  completeClassExpressionSemanticSupportList [] =
    tt
  completeClassExpressionSemanticSupportList (class ∷ classes) =
    completeClassExpressionSemanticSupport class ,
    completeClassExpressionSemanticSupportList classes

  completeOptionalClassExpressionSemanticSupport :
    {Sig : Signature} →
    (class : Optional (ClassExpression Sig)) →
    OptionalClassExpressionSemanticSupport class
  completeOptionalClassExpressionSemanticSupport absent =
    tt
  completeOptionalClassExpressionSemanticSupport (present class) =
    completeClassExpressionSemanticSupport class

AxiomSemanticSupport :
  {Sig : Signature} →
  Axiom Sig →
  Type₀
AxiomSemanticSupport (declaration entity) =
  Unit
AxiomSemanticSupport (subClassOf sub sup) =
  ClassExpressionSemanticSupport sub × ClassExpressionSemanticSupport sup
AxiomSemanticSupport (equivalentClasses classes) =
  AtLeastTwoSemanticSupport ClassExpressionSemanticSupport classes
AxiomSemanticSupport (disjointClasses classes) =
  AtLeastTwoSemanticSupport ClassExpressionSemanticSupport classes
AxiomSemanticSupport (disjointUnion class classes) =
  AtLeastTwoSemanticSupport ClassExpressionSemanticSupport classes
AxiomSemanticSupport (subObjectPropertyOf sub sup) =
  Unit
AxiomSemanticSupport (equivalentObjectProperties properties) =
  Unit
AxiomSemanticSupport (disjointObjectProperties properties) =
  Unit
AxiomSemanticSupport (inverseObjectProperties left right) =
  Unit
AxiomSemanticSupport (objectPropertyDomain property class) =
  ClassExpressionSemanticSupport class
AxiomSemanticSupport (objectPropertyRange property class) =
  ClassExpressionSemanticSupport class
AxiomSemanticSupport (functionalObjectProperty property) =
  Unit
AxiomSemanticSupport (inverseFunctionalObjectProperty property) =
  Unit
AxiomSemanticSupport (reflexiveObjectProperty property) =
  Unit
AxiomSemanticSupport (irreflexiveObjectProperty property) =
  Unit
AxiomSemanticSupport (symmetricObjectProperty property) =
  Unit
AxiomSemanticSupport (asymmetricObjectProperty property) =
  Unit
AxiomSemanticSupport (transitiveObjectProperty property) =
  Unit
AxiomSemanticSupport (subDataPropertyOf sub sup) =
  Unit
AxiomSemanticSupport (equivalentDataProperties properties) =
  Unit
AxiomSemanticSupport (disjointDataProperties properties) =
  Unit
AxiomSemanticSupport (dataPropertyDomain property class) =
  ClassExpressionSemanticSupport class
AxiomSemanticSupport (dataPropertyRange property range) =
  DataRangeSemanticSupport range
AxiomSemanticSupport (functionalDataProperty property) =
  Unit
AxiomSemanticSupport (datatypeDefinition name support range) =
  DataRangeSemanticSupport range
AxiomSemanticSupport (hasKey class key) =
  ClassExpressionSemanticSupport class
AxiomSemanticSupport (sameIndividual individuals) =
  Unit
AxiomSemanticSupport (differentIndividuals individuals) =
  Unit
AxiomSemanticSupport (classAssertion class individual) =
  ClassExpressionSemanticSupport class
AxiomSemanticSupport (objectPropertyAssertion property subject object) =
  Unit
AxiomSemanticSupport (negativeObjectPropertyAssertion property subject object) =
  Unit
AxiomSemanticSupport (dataPropertyAssertion property subject literal) =
  Unit
AxiomSemanticSupport (negativeDataPropertyAssertion property subject literal) =
  Unit
AxiomSemanticSupport (annotationAssertion property subject value) =
  Unit
AxiomSemanticSupport (subAnnotationPropertyOf sub sup) =
  Unit
AxiomSemanticSupport (annotationPropertyDomain property iri) =
  Unit
AxiomSemanticSupport (annotationPropertyRange property iri) =
  Unit

completeAxiomSemanticSupport :
  {Sig : Signature} →
  (axiom : Axiom Sig) →
  AxiomSemanticSupport axiom
completeAxiomSemanticSupport (declaration entity) =
  tt
completeAxiomSemanticSupport (subClassOf sub sup) =
  completeClassExpressionSemanticSupport sub ,
  completeClassExpressionSemanticSupport sup
completeAxiomSemanticSupport (equivalentClasses classes) =
  completeAtLeastTwoSemanticSupport completeClassExpressionSemanticSupport classes
completeAxiomSemanticSupport (disjointClasses classes) =
  completeAtLeastTwoSemanticSupport completeClassExpressionSemanticSupport classes
completeAxiomSemanticSupport (disjointUnion class classes) =
  completeAtLeastTwoSemanticSupport completeClassExpressionSemanticSupport classes
completeAxiomSemanticSupport (subObjectPropertyOf sub sup) =
  tt
completeAxiomSemanticSupport (equivalentObjectProperties properties) =
  tt
completeAxiomSemanticSupport (disjointObjectProperties properties) =
  tt
completeAxiomSemanticSupport (inverseObjectProperties left right) =
  tt
completeAxiomSemanticSupport (objectPropertyDomain property class) =
  completeClassExpressionSemanticSupport class
completeAxiomSemanticSupport (objectPropertyRange property class) =
  completeClassExpressionSemanticSupport class
completeAxiomSemanticSupport (functionalObjectProperty property) =
  tt
completeAxiomSemanticSupport (inverseFunctionalObjectProperty property) =
  tt
completeAxiomSemanticSupport (reflexiveObjectProperty property) =
  tt
completeAxiomSemanticSupport (irreflexiveObjectProperty property) =
  tt
completeAxiomSemanticSupport (symmetricObjectProperty property) =
  tt
completeAxiomSemanticSupport (asymmetricObjectProperty property) =
  tt
completeAxiomSemanticSupport (transitiveObjectProperty property) =
  tt
completeAxiomSemanticSupport (subDataPropertyOf sub sup) =
  tt
completeAxiomSemanticSupport (equivalentDataProperties properties) =
  tt
completeAxiomSemanticSupport (disjointDataProperties properties) =
  tt
completeAxiomSemanticSupport (dataPropertyDomain property class) =
  completeClassExpressionSemanticSupport class
completeAxiomSemanticSupport (dataPropertyRange property range) =
  completeDataRangeSemanticSupport range
completeAxiomSemanticSupport (functionalDataProperty property) =
  tt
completeAxiomSemanticSupport (datatypeDefinition name support range) =
  completeDataRangeSemanticSupport range
completeAxiomSemanticSupport (hasKey class key) =
  completeClassExpressionSemanticSupport class
completeAxiomSemanticSupport (sameIndividual individuals) =
  tt
completeAxiomSemanticSupport (differentIndividuals individuals) =
  tt
completeAxiomSemanticSupport (classAssertion class individual) =
  completeClassExpressionSemanticSupport class
completeAxiomSemanticSupport (objectPropertyAssertion property subject object) =
  tt
completeAxiomSemanticSupport (negativeObjectPropertyAssertion property subject object) =
  tt
completeAxiomSemanticSupport (dataPropertyAssertion property subject literal) =
  tt
completeAxiomSemanticSupport (negativeDataPropertyAssertion property subject literal) =
  tt
completeAxiomSemanticSupport (annotationAssertion property subject value) =
  tt
completeAxiomSemanticSupport (subAnnotationPropertyOf sub sup) =
  tt
completeAxiomSemanticSupport (annotationPropertyDomain property iri) =
  tt
completeAxiomSemanticSupport (annotationPropertyRange property iri) =
  tt

OntologyAxiomsSemanticSupport :
  {Sig : Signature} →
  List (Axiom Sig) →
  Type₀
OntologyAxiomsSemanticSupport =
  ListSemanticSupport AxiomSemanticSupport

record OntologySemanticSupport
  (Sig : Signature) (axioms : List (Axiom Sig)) : Type₀ where
  constructor ontologySemanticSupport
  field
    supportedAxioms :
      OntologyAxiomsSemanticSupport axioms

open OntologySemanticSupport public

completeOntologyAxiomsSemanticSupport :
  {Sig : Signature} →
  (axioms : List (Axiom Sig)) →
  OntologyAxiomsSemanticSupport axioms
completeOntologyAxiomsSemanticSupport =
  completeListSemanticSupport completeAxiomSemanticSupport

completeOntologySemanticSupport :
  {Sig : Signature} →
  (axioms : List (Axiom Sig)) →
  OntologySemanticSupport Sig axioms
completeOntologySemanticSupport axioms =
  ontologySemanticSupport (completeOntologyAxiomsSemanticSupport axioms)

record SourceOntologySemanticSupport
  (Sig : Signature) (axioms : List (Axiom Sig)) : Type₀ where
  constructor sourceOntologySemanticSupport
  field
    sourceAxioms :
      List (Axiom Sig)
    sourceAxiomsPreserved :
      sourceAxioms ≡ axioms
    sourceSupportedAxioms :
      OntologyAxiomsSemanticSupport sourceAxioms

open SourceOntologySemanticSupport public

sourceOntologySemanticSupportEvidence :
  {Sig : Signature} →
  {axioms : List (Axiom Sig)} →
  SourceOntologySemanticSupport Sig axioms →
  OntologySemanticSupport Sig axioms
sourceOntologySemanticSupportEvidence support =
  ontologySemanticSupport
    (subst
      OntologyAxiomsSemanticSupport
      (sourceAxiomsPreserved support)
      (sourceSupportedAxioms support))

completeSourceOntologySemanticSupport :
  {Sig : Signature} →
  (axioms : List (Axiom Sig)) →
  SourceOntologySemanticSupport Sig axioms
completeSourceOntologySemanticSupport axioms =
  sourceOntologySemanticSupport
    axioms
    refl
    (completeOntologyAxiomsSemanticSupport axioms)