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

module OWL2.Elab.Punning where

open import OWL2.Prelude
open import OWL2.Diagnostics
open import OWL2.Elab.SymbolTable
open import OWL2.Raw hiding (SourcePath; sourcePath; rootPath; fieldPath; indexPath)

private
  elabCode : String → DiagnosticCode
  elabCode name =
    mkDiagnosticCode "elab.punning" name

  entityPath : SourcePath
  entityPath =
    sourcePath (fieldSegment "entity" ∷ [])

punningDeclarationDiagnostic : RawIRI → Diagnostic
punningDeclarationDiagnostic iri =
  diagnostic
    (elabCode "punning-declaration")
    severityError
    entityPath
    (text iri)

rawIRIInList? : RawIRI → List RawIRI → Bool
rawIRIInList? iri [] =
  false
rawIRIInList? iri (candidate ∷ candidates) with sameRawIRI iri candidate
... | true =
  true
... | false =
  rawIRIInList? iri candidates

punningPairDiagnostics : List RawIRI → List RawIRI → Diagnostics
punningPairDiagnostics [] right =
  noDiagnostics
punningPairDiagnostics (iri ∷ left) right with rawIRIInList? iri right
... | true =
  singleDiagnostic (punningDeclarationDiagnostic iri) ++
  punningPairDiagnostics left right
... | false =
  punningPairDiagnostics left right

rawPunningDiagnosticsFromSymbolTable : SymbolTable → Diagnostics
rawPunningDiagnosticsFromSymbolTable table =
  punningPairDiagnostics (classIRIs table) (objectPropertyIRIs table) ++
  punningPairDiagnostics (classIRIs table) (dataPropertyIRIs table) ++
  punningPairDiagnostics (classIRIs table) (annotationPropertyIRIs table) ++
  punningPairDiagnostics (classIRIs table) (datatypeIRIs table) ++
  punningPairDiagnostics (classIRIs table) (individualIRIs table) ++
  punningPairDiagnostics (objectPropertyIRIs table) (dataPropertyIRIs table) ++
  punningPairDiagnostics
    (objectPropertyIRIs table)
    (annotationPropertyIRIs table) ++
  punningPairDiagnostics (objectPropertyIRIs table) (datatypeIRIs table) ++
  punningPairDiagnostics (objectPropertyIRIs table) (individualIRIs table) ++
  punningPairDiagnostics
    (dataPropertyIRIs table)
    (annotationPropertyIRIs table) ++
  punningPairDiagnostics (dataPropertyIRIs table) (datatypeIRIs table) ++
  punningPairDiagnostics (dataPropertyIRIs table) (individualIRIs table) ++
  punningPairDiagnostics (annotationPropertyIRIs table) (datatypeIRIs table) ++
  punningPairDiagnostics (annotationPropertyIRIs table) (individualIRIs table) ++
  punningPairDiagnostics (datatypeIRIs table) (individualIRIs table)