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

module OWL2.Kernel.Name where

open import OWL2.Prelude public
open import OWL2.Kernel.Signature public
  using (Signature)
open import Cubical.Data.FinData.Base public
  using (Fin)
  renaming (zero to fzero; suc to fsuc; toℕ to symbolIndex)

data NameKind : Type₀ where
  classKind :
    NameKind
  objectPropertyKind :
    NameKind
  dataPropertyKind :
    NameKind
  annotationPropertyKind :
    NameKind
  datatypeKind :
    NameKind
  facetKind :
    NameKind
  individualKind :
    NameKind
  iriKind :
    NameKind
  blankNodeKind :
    NameKind

symbolCount : Signature → NameKind → ℕ
symbolCount Sig classKind =
  Signature.classCount Sig
symbolCount Sig objectPropertyKind =
  Signature.objectPropertyCount Sig
symbolCount Sig dataPropertyKind =
  Signature.dataPropertyCount Sig
symbolCount Sig annotationPropertyKind =
  Signature.annotationPropertyCount Sig
symbolCount Sig datatypeKind =
  Signature.datatypeCount Sig
symbolCount Sig facetKind =
  Signature.facetCount Sig
symbolCount Sig individualKind =
  Signature.individualCount Sig
symbolCount Sig iriKind =
  Signature.iriCount Sig
symbolCount Sig blankNodeKind =
  Signature.blankNodeCount Sig

Symbol : Signature → NameKind → Type₀
Symbol Sig kind =
  Fin (symbolCount Sig kind)

record ScopedName (Sig : Signature) (kind : NameKind) : Type₀ where
  constructor scopedName
  field
    symbol : Symbol Sig kind

open ScopedName public

ClassName ObjectPropertyName DataPropertyName AnnotationPropertyName
  DatatypeName FacetName IndividualName IRIName BlankNodeName :
  Signature → Type₀
ClassName Sig =
  ScopedName Sig classKind
ObjectPropertyName Sig =
  ScopedName Sig objectPropertyKind
DataPropertyName Sig =
  ScopedName Sig dataPropertyKind
AnnotationPropertyName Sig =
  ScopedName Sig annotationPropertyKind
DatatypeName Sig =
  ScopedName Sig datatypeKind
FacetName Sig =
  ScopedName Sig facetKind
IndividualName Sig =
  ScopedName Sig individualKind
IRIName Sig =
  ScopedName Sig iriKind
BlankNodeName Sig =
  ScopedName Sig blankNodeKind

className : {Sig : Signature} → Symbol Sig classKind → ClassName Sig
className =
  scopedName

objectPropertyName :
  {Sig : Signature} → Symbol Sig objectPropertyKind → ObjectPropertyName Sig
objectPropertyName =
  scopedName

dataPropertyName :
  {Sig : Signature} → Symbol Sig dataPropertyKind → DataPropertyName Sig
dataPropertyName =
  scopedName

annotationPropertyName :
  {Sig : Signature} →
  Symbol Sig annotationPropertyKind →
  AnnotationPropertyName Sig
annotationPropertyName =
  scopedName

datatypeName : {Sig : Signature} → Symbol Sig datatypeKind → DatatypeName Sig
datatypeName =
  scopedName

facetName : {Sig : Signature} → Symbol Sig facetKind → FacetName Sig
facetName =
  scopedName

individualName :
  {Sig : Signature} → Symbol Sig individualKind → IndividualName Sig
individualName =
  scopedName

iriName :
  {Sig : Signature} → Symbol Sig iriKind → IRIName Sig
iriName =
  scopedName

blankNodeName :
  {Sig : Signature} → Symbol Sig blankNodeKind → BlankNodeName Sig
blankNodeName =
  scopedName