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

module OWL2.Kernel.DatatypeMap where

open import OWL2.Prelude public
open import OWL2.Kernel.Signature public
  using (Signature)
open import OWL2.Kernel.Name public
  using (DatatypeName)

record DatatypeMap (Sig : Signature) : Type₀ where
  constructor datatypeMap
  field
    canonicalDatatype :
      DatatypeName Sig → DatatypeName Sig
    canonicalDatatypeMatches :
      (d : DatatypeName Sig) → canonicalDatatype d ≡ d
    canonicalLiteralDatatype :
      DatatypeName Sig → DatatypeName Sig
    canonicalLiteralDatatypeMatches :
      (d : DatatypeName Sig) → canonicalLiteralDatatype d ≡ d

open DatatypeMap public

record DatatypeSupported
  (Sig : Signature) (d : DatatypeName Sig) : Type₀ where
  constructor datatypeSupported
  field
    supportedDatatypeName :
      DatatypeName Sig
    supportedDatatypeMatches :
      supportedDatatypeName ≡ d

open DatatypeSupported public

record LiteralSupported
  (Sig : Signature) (d : DatatypeName Sig) : Type₀ where
  constructor literalSupported
  field
    supportedLiteralDatatypeName :
      DatatypeName Sig
    supportedLiteralDatatypeMatches :
      supportedLiteralDatatypeName ≡ d

open LiteralSupported public

trivialDatatypeMap : {Sig : Signature} → DatatypeMap Sig
trivialDatatypeMap =
  datatypeMap (λ d → d) (λ d → refl) (λ d → d) (λ d → refl)

trivialDatatypeSupported :
  {Sig : Signature} →
  (d : DatatypeName Sig) →
  DatatypeSupported Sig d
trivialDatatypeSupported d =
  datatypeSupported d refl

trivialLiteralSupported :
  {Sig : Signature} →
  (d : DatatypeName Sig) →
  LiteralSupported Sig d
trivialLiteralSupported d =
  literalSupported d refl