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

module OWL2.Portable.RegularityRank where

open import Cubical.Data.Nat.Base using (zero; suc)
open import OWL2.Prelude
import OWL2.Portable.Equality as Equality
import OWL2.Portable.Regularity as Reg
import OWL2.Portable.Syntax as P

private
  concatMap : ∀ {A B : Type₀} → (A → List B) → List A → List B
  concatMap f [] =
    []
  concatMap f (x ∷ xs) =
    f x ++ concatMap f xs

  listCount : ∀ {ℓ} {A : Type ℓ} → List A → ℕ
  listCount [] =
    zero
  listCount (x ∷ xs) =
    suc (listCount xs)

natLessThan : ℕ → ℕ → Bool
natLessThan zero zero =
  false
natLessThan zero (suc n) =
  true
natLessThan (suc m) zero =
  false
natLessThan (suc m) (suc n) =
  natLessThan m n

record PropertyRank : Type₀ where
  constructor propertyRank
  field
    propertyRankKey :
      String
    propertyRankValue :
      ℕ

open PropertyRank public

propertyRankForExpression :
  P.ObjectPropertyExpression → ℕ → PropertyRank
propertyRankForExpression property rank =
  propertyRank (Reg.objectPropertyBaseKey property) rank

rankForKey : String → List PropertyRank → Optional ℕ
rankForKey key [] =
  absent
rankForKey key (rank ∷ ranks)
  with primStringEquality key (propertyRankKey rank)
... | true =
  present (propertyRankValue rank)
... | false =
  rankForKey key ranks

rankForObjectPropertyExpression :
  List PropertyRank → P.ObjectPropertyExpression → Optional ℕ
rankForObjectPropertyExpression ranks property =
  rankForKey (Reg.objectPropertyBaseKey property) ranks

sameObjectPropertyBaseKey :
  P.ObjectPropertyExpression → P.ObjectPropertyExpression → Bool
sameObjectPropertyBaseKey left right =
  primStringEquality
    (Reg.objectPropertyBaseKey left)
    (Reg.objectPropertyBaseKey right)

boolAnd : Bool → Bool → Bool
boolAnd true true =
  true
boolAnd _ _ =
  false

sameObjectPropertyExpression :
  P.ObjectPropertyExpression → P.ObjectPropertyExpression → Bool
sameObjectPropertyExpression left right
  with Equality.objectPropertyExpressionEquality left right
... | present equalProperty =
  true
... | absent =
  false

objectPropertyChainElements :
  P.ObjectPropertyChain → List P.ObjectPropertyExpression
objectPropertyChainElements (P.objectPropertyChain properties) =
  P.first properties ∷ P.second properties ∷ P.rest properties

record PropertyChainAxiomFact : Type₀ where
  constructor propertyChainAxiomFact
  field
    propertyChainAxiomSource :
      P.Annotated P.Axiom
    propertyChainAxiomChain :
      P.ObjectPropertyChain
    propertyChainAxiomSuperProperty :
      P.ObjectPropertyExpression
    propertyChainAxiomSuperPropertyKey :
      String
    propertyChainAxiomElements :
      List P.ObjectPropertyExpression

open PropertyChainAxiomFact public

propertyChainAxiomFactForAnnotated :
  P.Annotated P.Axiom → Optional PropertyChainAxiomFact
propertyChainAxiomFactForAnnotated source with P.body source
... | P.subObjectPropertyOf (P.subObjectProperty property) super =
  absent
... | P.subObjectPropertyOf (P.subObjectPropertyChain chain) super =
  present
    (propertyChainAxiomFact
      source
      chain
      super
      (Reg.objectPropertyBaseKey super)
      (objectPropertyChainElements chain))
... | _ =
  absent

propertyChainAxiomFacts :
  List (P.Annotated P.Axiom) → List PropertyChainAxiomFact
propertyChainAxiomFacts axioms =
  filterMap propertyChainAxiomFactForAnnotated axioms

ontologyPropertyChainAxiomFacts :
  P.Ontology → List PropertyChainAxiomFact
ontologyPropertyChainAxiomFacts ont =
  propertyChainAxiomFacts (P.axioms ont)

ontologyDocumentPropertyChainAxiomFacts :
  P.OntologyDocument → List PropertyChainAxiomFact
ontologyDocumentPropertyChainAxiomFacts document =
  ontologyPropertyChainAxiomFacts (P.documentOntology document)

data ChainElementRankOrder : Type₀ where
  chainElementRankStrictlyBelowSuper :
    ChainElementRankOrder
  chainElementRankNotBelowSuper :
    ChainElementRankOrder
  chainElementRankMissing :
    ChainElementRankOrder
  chainSuperRankMissing :
    ChainElementRankOrder
  chainElementAndSuperRanksMissing :
    ChainElementRankOrder

classifyChainElementRankOrder :
  Optional ℕ → Optional ℕ → ChainElementRankOrder
classifyChainElementRankOrder absent absent =
  chainElementAndSuperRanksMissing
classifyChainElementRankOrder absent (present superRank) =
  chainElementRankMissing
classifyChainElementRankOrder (present elementRank) absent =
  chainSuperRankMissing
classifyChainElementRankOrder
  (present elementRank)
  (present superRank)
  with natLessThan elementRank superRank
... | true =
  chainElementRankStrictlyBelowSuper
... | false =
  chainElementRankNotBelowSuper

chainElementRankOrderHasEvidence : ChainElementRankOrder → Bool
chainElementRankOrderHasEvidence chainElementRankStrictlyBelowSuper =
  true
chainElementRankOrderHasEvidence chainElementRankNotBelowSuper =
  true
chainElementRankOrderHasEvidence chainElementRankMissing =
  false
chainElementRankOrderHasEvidence chainSuperRankMissing =
  false
chainElementRankOrderHasEvidence chainElementAndSuperRanksMissing =
  false

chainElementRankOrderStrictlyBelow : ChainElementRankOrder → Bool
chainElementRankOrderStrictlyBelow chainElementRankStrictlyBelowSuper =
  true
chainElementRankOrderStrictlyBelow chainElementRankNotBelowSuper =
  false
chainElementRankOrderStrictlyBelow chainElementRankMissing =
  false
chainElementRankOrderStrictlyBelow chainSuperRankMissing =
  false
chainElementRankOrderStrictlyBelow chainElementAndSuperRanksMissing =
  false

record PropertyChainElementRankCheck : Type₀ where
  constructor propertyChainElementRankCheck
  field
    propertyChainElementProperty :
      P.ObjectPropertyExpression
    propertyChainElementKey :
      String
    propertyChainElementRank :
      Optional ℕ
    propertyChainElementSuperRank :
      Optional ℕ
    propertyChainElementRankOrder :
      ChainElementRankOrder

open PropertyChainElementRankCheck public

propertyChainElementRankCheckFor :
  List PropertyRank →
  Optional ℕ →
  P.ObjectPropertyExpression →
  PropertyChainElementRankCheck
propertyChainElementRankCheckFor ranks superRank property =
  propertyChainElementRankCheck
    property
    key
    elementRank
    superRank
    (classifyChainElementRankOrder elementRank superRank)
  where
  key : String
  key =
    Reg.objectPropertyBaseKey property

  elementRank : Optional ℕ
  elementRank =
    rankForKey key ranks

propertyChainElementRankChecks :
  List PropertyRank →
  Optional ℕ →
  List P.ObjectPropertyExpression →
  List PropertyChainElementRankCheck
propertyChainElementRankChecks ranks superRank [] =
  []
propertyChainElementRankChecks ranks superRank (property ∷ properties) =
  propertyChainElementRankCheckFor ranks superRank property
  ∷ propertyChainElementRankChecks ranks superRank properties

allElementRankChecksHaveEvidence :
  List PropertyChainElementRankCheck → Bool
allElementRankChecksHaveEvidence [] =
  true
allElementRankChecksHaveEvidence (check ∷ checks)
  with chainElementRankOrderHasEvidence (propertyChainElementRankOrder check)
... | true =
  allElementRankChecksHaveEvidence checks
... | false =
  false

allElementRankChecksStrictlyBelow :
  List PropertyChainElementRankCheck → Bool
allElementRankChecksStrictlyBelow [] =
  true
allElementRankChecksStrictlyBelow (check ∷ checks)
  with chainElementRankOrderStrictlyBelow
        (propertyChainElementRankOrder check)
... | true =
  allElementRankChecksStrictlyBelow checks
... | false =
  false

chainIsTransitiveSelfShape :
  P.ObjectPropertyChain → P.ObjectPropertyExpression → Bool
chainIsTransitiveSelfShape (P.objectPropertyChain properties) super
  with P.rest properties
... | [] =
  boolAnd
    (sameObjectPropertyExpression (P.first properties) super)
    (sameObjectPropertyExpression (P.second properties) super)
... | _ ∷ _ =
  false

objectPropertyExpressionIsTop : P.ObjectPropertyExpression → Bool
objectPropertyExpressionIsTop P.topObjectProperty =
  true
objectPropertyExpressionIsTop _ =
  false

data PropertyChainRankClassification : Type₀ where
  propertyChainToTopAllowed :
    PropertyChainRankClassification
  propertyChainStrictlyRanked :
    PropertyChainRankClassification
  propertyChainTransitiveSelfAllowed :
    PropertyChainRankClassification
  propertyChainMissingRankEvidence :
    PropertyChainRankClassification
  propertyChainInsufficientSubpropertyRank :
    PropertyChainRankClassification

classifyPropertyChainRanks :
  Bool →
  Bool →
  Bool →
  Bool →
  PropertyChainRankClassification
classifyPropertyChainRanks true transitiveSelf evidence below =
  propertyChainToTopAllowed
classifyPropertyChainRanks false true evidence below =
  propertyChainTransitiveSelfAllowed
classifyPropertyChainRanks false false true true =
  propertyChainStrictlyRanked
classifyPropertyChainRanks false false false below =
  propertyChainMissingRankEvidence
classifyPropertyChainRanks false false true false =
  propertyChainInsufficientSubpropertyRank

data PropertyChainRankIssueKind : Type₀ where
  missingSuperPropertyRank :
    PropertyChainRankIssueKind
  missingSubpropertyRank :
    PropertyChainRankIssueKind
  insufficientSubpropertyRank :
    PropertyChainRankIssueKind

record PropertyChainRankIssue : Type₀ where
  constructor propertyChainRankIssue
  field
    propertyChainRankIssueSource :
      P.Annotated P.Axiom
    propertyChainRankIssueSuperProperty :
      P.ObjectPropertyExpression
    propertyChainRankIssueSuperPropertyKey :
      String
    propertyChainRankIssueSubproperty :
      Optional P.ObjectPropertyExpression
    propertyChainRankIssueSubpropertyKey :
      Optional String
    propertyChainRankIssueSubpropertyRank :
      Optional ℕ
    propertyChainRankIssueSuperRank :
      Optional ℕ
    propertyChainRankIssueKind :
      PropertyChainRankIssueKind

open PropertyChainRankIssue public

missingSuperRankIssues :
  PropertyChainAxiomFact → Optional ℕ → List PropertyChainRankIssue
missingSuperRankIssues fact absent =
  propertyChainRankIssue
    (propertyChainAxiomSource fact)
    (propertyChainAxiomSuperProperty fact)
    (propertyChainAxiomSuperPropertyKey fact)
    absent
    absent
    absent
    absent
    missingSuperPropertyRank
  ∷ []
missingSuperRankIssues fact (present superRank) =
  []

propertyChainElementRankIssues :
  PropertyChainAxiomFact →
  PropertyChainElementRankCheck →
  List PropertyChainRankIssue
propertyChainElementRankIssues fact check
  with propertyChainElementRankOrder check
... | chainElementRankStrictlyBelowSuper =
  []
... | chainElementRankNotBelowSuper =
  propertyChainRankIssue
    (propertyChainAxiomSource fact)
    (propertyChainAxiomSuperProperty fact)
    (propertyChainAxiomSuperPropertyKey fact)
    (present (propertyChainElementProperty check))
    (present (propertyChainElementKey check))
    (propertyChainElementRank check)
    (propertyChainElementSuperRank check)
    insufficientSubpropertyRank
  ∷ []
... | chainElementRankMissing =
  propertyChainRankIssue
    (propertyChainAxiomSource fact)
    (propertyChainAxiomSuperProperty fact)
    (propertyChainAxiomSuperPropertyKey fact)
    (present (propertyChainElementProperty check))
    (present (propertyChainElementKey check))
    absent
    (propertyChainElementSuperRank check)
    missingSubpropertyRank
  ∷ []
... | chainSuperRankMissing =
  []
... | chainElementAndSuperRanksMissing =
  propertyChainRankIssue
    (propertyChainAxiomSource fact)
    (propertyChainAxiomSuperProperty fact)
    (propertyChainAxiomSuperPropertyKey fact)
    (present (propertyChainElementProperty check))
    (present (propertyChainElementKey check))
    absent
    absent
    missingSubpropertyRank
  ∷ []

propertyChainElementsRankIssues :
  PropertyChainAxiomFact →
  List PropertyChainElementRankCheck →
  List PropertyChainRankIssue
propertyChainElementsRankIssues fact =
  concatMap (propertyChainElementRankIssues fact)

record PropertyChainRankDiagnostic : Type₀ where
  constructor propertyChainRankDiagnostic
  field
    propertyChainRankFact :
      PropertyChainAxiomFact
    propertyChainRankSuperRank :
      Optional ℕ
    propertyChainRankElementChecks :
      List PropertyChainElementRankCheck
    propertyChainRankToTop :
      Bool
    propertyChainRankTransitiveSelfShape :
      Bool
    propertyChainRankHasEnoughEvidence :
      Bool
    propertyChainRankAllElementsStrictlyBelowSuper :
      Bool
    propertyChainRankClassification :
      PropertyChainRankClassification
    propertyChainRankIssues :
      List PropertyChainRankIssue
    propertyChainRankIssueCount :
      ℕ

open PropertyChainRankDiagnostic public

propertyChainRankDiagnosticFor :
  List PropertyRank → PropertyChainAxiomFact → PropertyChainRankDiagnostic
propertyChainRankDiagnosticFor ranks fact =
  propertyChainRankDiagnostic
    fact
    superRank
    checks
    toTop
    transitiveSelfShape
    hasEvidence
    allBelow
    (classifyPropertyChainRanks
      toTop
      transitiveSelfShape
      hasEvidence
      allBelow)
    issues
    (listCount issues)
  where
  superRank : Optional ℕ
  superRank =
    rankForKey (propertyChainAxiomSuperPropertyKey fact) ranks

  checks : List PropertyChainElementRankCheck
  checks =
    propertyChainElementRankChecks
      ranks
      superRank
      (propertyChainAxiomElements fact)

  toTop : Bool
  toTop =
    objectPropertyExpressionIsTop
      (propertyChainAxiomSuperProperty fact)

  transitiveSelfShape : Bool
  transitiveSelfShape =
    chainIsTransitiveSelfShape
      (propertyChainAxiomChain fact)
      (propertyChainAxiomSuperProperty fact)

  hasEvidence : Bool
  hasEvidence =
    allElementRankChecksHaveEvidence checks

  allBelow : Bool
  allBelow =
    allElementRankChecksStrictlyBelow checks

  issues : List PropertyChainRankIssue
  issues with toTop | transitiveSelfShape
  ... | true | _ =
    []
  ... | false | true =
    []
  ... | false | false =
    missingSuperRankIssues fact superRank
    ++ propertyChainElementsRankIssues fact checks

propertyChainRankDiagnostics :
  List PropertyRank →
  List PropertyChainAxiomFact →
  List PropertyChainRankDiagnostic
propertyChainRankDiagnostics ranks [] =
  []
propertyChainRankDiagnostics ranks (fact ∷ facts) =
  propertyChainRankDiagnosticFor ranks fact
  ∷ propertyChainRankDiagnostics ranks facts

propertyChainRankIssuesForDiagnostics :
  List PropertyChainRankDiagnostic → List PropertyChainRankIssue
propertyChainRankIssuesForDiagnostics =
  concatMap propertyChainRankIssues

record RegularityRankReport : Type₀ where
  constructor regularityRankReport
  field
    regularityRankReportDocument :
      P.OntologyDocument
    regularityRankReportPropertyRanks :
      List PropertyRank
    regularityRankReportBaseRegularityReport :
      Reg.RegularityReport
    regularityRankReportPropertyChainAxioms :
      List PropertyChainAxiomFact
    regularityRankReportPropertyChainDiagnostics :
      List PropertyChainRankDiagnostic
    regularityRankReportPropertyChainIssues :
      List PropertyChainRankIssue
    regularityRankReportPropertyRankCount :
      ℕ
    regularityRankReportPropertyChainAxiomCount :
      ℕ
    regularityRankReportPropertyChainDiagnosticCount :
      ℕ
    regularityRankReportPropertyChainIssueCount :
      ℕ

open RegularityRankReport public

reportRegularityRank :
  List PropertyRank → P.OntologyDocument → RegularityRankReport
reportRegularityRank ranks document =
  regularityRankReport
    document
    ranks
    (Reg.reportRegularity document)
    chainFacts
    diagnostics
    issues
    (listCount ranks)
    (listCount chainFacts)
    (listCount diagnostics)
    (listCount issues)
  where
  chainFacts : List PropertyChainAxiomFact
  chainFacts =
    ontologyDocumentPropertyChainAxiomFacts document

  diagnostics : List PropertyChainRankDiagnostic
  diagnostics =
    propertyChainRankDiagnostics ranks chainFacts

  issues : List PropertyChainRankIssue
  issues =
    propertyChainRankIssuesForDiagnostics diagnostics

NoPropertyChainRankIssues :
  List PropertyChainRankIssue → Type₀
NoPropertyChainRankIssues [] =
  Unit*
NoPropertyChainRankIssues (_ ∷ _) =
  ⊥

NoReportPropertyChainRankIssues :
  RegularityRankReport → Type₀
NoReportPropertyChainRankIssues report =
  NoPropertyChainRankIssues
    (regularityRankReportPropertyChainIssues report)

PortableRegularityRankRestrictions :
  List PropertyRank → P.OntologyDocument → Type₀
PortableRegularityRankRestrictions ranks document =
  NoReportPropertyChainRankIssues
    (reportRegularityRank ranks document)