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

module OWL2.Elab.Regularity where

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

data RawObjectPropertyKey : Type₀ where
  keyObjectProperty :
    RawIRI → RawObjectPropertyKey
  keyInverseObjectProperty :
    RawIRI → RawObjectPropertyKey
  keyTopObjectProperty :
    RawObjectPropertyKey
  keyBottomObjectProperty :
    RawObjectPropertyKey

record RawObjectPropertyEdge : Type₀ where
  constructor rawObjectPropertyEdge
  field
    edgeSub :
      RawObjectPropertyKey
    edgeSuper :
      RawObjectPropertyKey

open RawObjectPropertyEdge public

invertRawObjectPropertyKey : RawObjectPropertyKey → RawObjectPropertyKey
invertRawObjectPropertyKey (keyObjectProperty iri) =
  keyInverseObjectProperty iri
invertRawObjectPropertyKey (keyInverseObjectProperty iri) =
  keyObjectProperty iri
invertRawObjectPropertyKey keyTopObjectProperty =
  keyTopObjectProperty
invertRawObjectPropertyKey keyBottomObjectProperty =
  keyBottomObjectProperty

sameRawObjectPropertyKey :
  RawObjectPropertyKey → RawObjectPropertyKey → Bool
sameRawObjectPropertyKey (keyObjectProperty left) (keyObjectProperty right) =
  sameRawIRI left right
sameRawObjectPropertyKey
  (keyInverseObjectProperty left)
  (keyInverseObjectProperty right) =
  sameRawIRI left right
sameRawObjectPropertyKey keyTopObjectProperty keyTopObjectProperty =
  true
sameRawObjectPropertyKey keyBottomObjectProperty keyBottomObjectProperty =
  true
sameRawObjectPropertyKey left right =
  false

rawObjectPropertyKey :
  RawObjectPropertyExpression → RawObjectPropertyKey
rawObjectPropertyKey (rawObjectProperty iri) =
  keyObjectProperty iri
rawObjectPropertyKey rawTopObjectProperty =
  keyTopObjectProperty
rawObjectPropertyKey rawBottomObjectProperty =
  keyBottomObjectProperty
rawObjectPropertyKey (rawObjectInverseOf property) =
  invertRawObjectPropertyKey (rawObjectPropertyKey property)

simpleUseKey : RawIRI → RawObjectPropertyKey
simpleUseKey iri =
  keyObjectProperty iri

compositeCarrierKey : RawObjectPropertyKey → RawObjectPropertyKey
compositeCarrierKey (keyInverseObjectProperty iri) =
  keyObjectProperty iri
compositeCarrierKey key =
  key

rawCompositeObjectPropertyKeysOfAxiom : RawAxiom → List RawObjectPropertyKey
rawCompositeObjectPropertyKeysOfAxiom
  (rawSubObjectPropertyOf (rawSubObjectPropertyChain properties) super) =
  compositeCarrierKey (rawObjectPropertyKey super) ∷ []
rawCompositeObjectPropertyKeysOfAxiom
  (rawTransitiveObjectProperty property) =
  compositeCarrierKey (rawObjectPropertyKey property) ∷ []
rawCompositeObjectPropertyKeysOfAxiom axiom =
  []

rawCompositeObjectPropertyKeysOfAnnotated :
  RawAnnotated RawAxiom → List RawObjectPropertyKey
rawCompositeObjectPropertyKeysOfAnnotated axiom =
  rawCompositeObjectPropertyKeysOfAxiom (body axiom)

rawCompositeObjectPropertyKeys :
  List (RawAnnotated RawAxiom) → List RawObjectPropertyKey
rawCompositeObjectPropertyKeys [] =
  keyTopObjectProperty ∷ keyBottomObjectProperty ∷ []
rawCompositeObjectPropertyKeys (axiom ∷ axioms) =
  rawCompositeObjectPropertyKeysOfAnnotated axiom ++
  rawCompositeObjectPropertyKeys axioms

rawObjectPropertyHierarchyEdgesFromKey :
  RawObjectPropertyKey →
  List RawObjectPropertyKey →
  List RawObjectPropertyEdge
rawObjectPropertyHierarchyEdgesFromKey key [] =
  []
rawObjectPropertyHierarchyEdgesFromKey key (target ∷ targets) =
  rawObjectPropertyEdge key target ∷
  rawObjectPropertyHierarchyEdgesFromKey key targets

rawObjectPropertyHierarchyEdgesFromKeys :
  List RawObjectPropertyKey →
  List RawObjectPropertyKey →
  List RawObjectPropertyEdge
rawObjectPropertyHierarchyEdgesFromKeys [] targets =
  []
rawObjectPropertyHierarchyEdgesFromKeys (key ∷ keys) targets =
  rawObjectPropertyHierarchyEdgesFromKey key targets ++
  rawObjectPropertyHierarchyEdgesFromKeys keys targets

rawObjectPropertyKeys :
  List RawObjectPropertyExpression → List RawObjectPropertyKey
rawObjectPropertyKeys [] =
  []
rawObjectPropertyKeys (property ∷ properties) =
  rawObjectPropertyKey property ∷ rawObjectPropertyKeys properties

invertRawObjectPropertyKeys :
  List RawObjectPropertyKey → List RawObjectPropertyKey
invertRawObjectPropertyKeys [] =
  []
invertRawObjectPropertyKeys (key ∷ keys) =
  invertRawObjectPropertyKey key ∷ invertRawObjectPropertyKeys keys

rawEquivalentObjectPropertyEdges :
  List RawObjectPropertyExpression → List RawObjectPropertyEdge
rawEquivalentObjectPropertyEdges properties =
  rawObjectPropertyHierarchyEdgesFromKeys keys keys ++
  rawObjectPropertyHierarchyEdgesFromKeys
    (invertRawObjectPropertyKeys keys)
    (invertRawObjectPropertyKeys keys)
  where
  keys : List RawObjectPropertyKey
  keys =
    rawObjectPropertyKeys properties

rawObjectPropertyHierarchyEdgesOfAxiom : RawAxiom → List RawObjectPropertyEdge
rawObjectPropertyHierarchyEdgesOfAxiom
  (rawSubObjectPropertyOf (rawSubObjectProperty sub) super) =
  rawObjectPropertyEdge subKey superKey ∷
  rawObjectPropertyEdge
    (invertRawObjectPropertyKey subKey)
    (invertRawObjectPropertyKey superKey)
  ∷ []
  where
  subKey : RawObjectPropertyKey
  subKey =
    rawObjectPropertyKey sub

  superKey : RawObjectPropertyKey
  superKey =
    rawObjectPropertyKey super
rawObjectPropertyHierarchyEdgesOfAxiom
  (rawEquivalentObjectProperties properties) =
  rawEquivalentObjectPropertyEdges properties
rawObjectPropertyHierarchyEdgesOfAxiom (rawSymmetricObjectProperty property) =
  rawObjectPropertyEdge key (invertRawObjectPropertyKey key) ∷
  rawObjectPropertyEdge (invertRawObjectPropertyKey key) key ∷
  []
  where
  key : RawObjectPropertyKey
  key =
    rawObjectPropertyKey property
rawObjectPropertyHierarchyEdgesOfAxiom axiom =
  []

rawObjectPropertyHierarchyEdgesOfAnnotated :
  RawAnnotated RawAxiom → List RawObjectPropertyEdge
rawObjectPropertyHierarchyEdgesOfAnnotated axiom =
  rawObjectPropertyHierarchyEdgesOfAxiom (body axiom)

rawObjectPropertyHierarchyEdges :
  List (RawAnnotated RawAxiom) → List RawObjectPropertyEdge
rawObjectPropertyHierarchyEdges [] =
  []
rawObjectPropertyHierarchyEdges (axiom ∷ axioms) =
  rawObjectPropertyHierarchyEdgesOfAnnotated axiom ++
  rawObjectPropertyHierarchyEdges axioms

mutual
  rawObjectPropertyReachableWithin? :
    ℕ →
    List RawObjectPropertyEdge →
    RawObjectPropertyKey →
    RawObjectPropertyKey →
    Bool
  rawObjectPropertyReachableWithin? zero edges source target =
    sameRawObjectPropertyKey source target
  rawObjectPropertyReachableWithin? (suc fuel) edges source target with
    sameRawObjectPropertyKey source target
  ... | true =
    true
  ... | false =
    rawObjectPropertyReachableViaEdges? fuel edges source target edges

  rawObjectPropertyReachableViaEdges? :
    ℕ →
    List RawObjectPropertyEdge →
    RawObjectPropertyKey →
    RawObjectPropertyKey →
    List RawObjectPropertyEdge →
    Bool
  rawObjectPropertyReachableViaEdges? fuel edges source target [] =
    false
  rawObjectPropertyReachableViaEdges?
    fuel
    edges
    source
    target
    (edge ∷ candidates) with sameRawObjectPropertyKey source (edgeSub edge)
  ... | false =
    rawObjectPropertyReachableViaEdges?
      fuel
      edges
      source
      target
      candidates
  ... | true with
    rawObjectPropertyReachableWithin? fuel edges (edgeSuper edge) target
  ...   | true =
    true
  ...   | false =
    rawObjectPropertyReachableViaEdges?
      fuel
      edges
      source
      target
      candidates

rawAnyCompositeObjectPropertyReachable? :
  ℕ →
  List RawObjectPropertyEdge →
  List RawObjectPropertyKey →
  RawObjectPropertyKey →
  Bool
rawAnyCompositeObjectPropertyReachable? fuel edges [] target =
  false
rawAnyCompositeObjectPropertyReachable?
  fuel
  edges
  (composite ∷ composites)
  target with rawObjectPropertyReachableWithin? fuel edges composite target
... | true =
  true
... | false =
  rawAnyCompositeObjectPropertyReachable? fuel edges composites target

rawSimpleObjectProperty? :
  List RawObjectPropertyKey →
  List RawObjectPropertyEdge →
  RawObjectPropertyKey →
  Bool
rawSimpleObjectProperty? composites edges key with
  rawAnyCompositeObjectPropertyReachable? (listCount edges) edges composites key
... | true =
  false
... | false =
  true

objectPropertyNameIRI :
  (table : SymbolTable) →
  K.ObjectPropertyName (symbolTableSignature table) →
  RawIRI
objectPropertyNameIRI table name =
  lookupByFin (objectPropertyIRIs table) (K.symbol name)

structuralRegularityContext :
  (table : SymbolTable) →
  List (RawAnnotated RawAxiom) →
  K.RegularityContext (symbolTableSignature table)
structuralRegularityContext table axioms =
  K.regularityContext
    (λ property →
      rawSimpleObjectProperty?
        composites
        edges
        (simpleUseKey (objectPropertyNameIRI table property)))
  where
  composites : List RawObjectPropertyKey
  composites =
    rawCompositeObjectPropertyKeys axioms

  edges : List RawObjectPropertyEdge
  edges =
    rawObjectPropertyHierarchyEdges axioms