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

module OWL2.Portable.ProfileRestrictions where

open import Cubical.Data.Nat.Base using (suc)
open import OWL2.Prelude
import OWL2.Portable.Syntax as P
import OWL2.Profiles.EL as EL
import OWL2.Profiles.QL as QL
import OWL2.Profiles.RL as RL

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

record ProfileRestrictionsReport : Type₀ where
  constructor profileRestrictionsReport
  field
    profileRestrictionsReportDocument :
      P.OntologyDocument
    profileRestrictionsELReport :
      EL.ELReport
    profileRestrictionsQLReport :
      QL.QLReport
    profileRestrictionsRLReport :
      RL.RLReport
    profileRestrictionsNonELFeatures :
      List EL.NonELFeature
    profileRestrictionsNonQLFeatures :
      List QL.NonQLFeature
    profileRestrictionsNonRLFeatures :
      List RL.NonRLFeature
    profileRestrictionsNonELFeatureCount :
      ℕ
    profileRestrictionsNonQLFeatureCount :
      ℕ
    profileRestrictionsNonRLFeatureCount :
      ℕ

open ProfileRestrictionsReport public

reportProfileRestrictions :
  P.OntologyDocument → ProfileRestrictionsReport
reportProfileRestrictions document =
  profileRestrictionsReport
    document
    elReport
    qlReport
    rlReport
    (EL.nonELFeatures elReport)
    (QL.nonQLFeatures qlReport)
    (RL.nonRLFeatures rlReport)
    (listCount (EL.nonELFeatures elReport))
    (listCount (QL.nonQLFeatures qlReport))
    (listCount (RL.nonRLFeatures rlReport))
  where
  elReport : EL.ELReport
  elReport =
    EL.ontologyDocumentReport document

  qlReport : QL.QLReport
  qlReport =
    QL.ontologyDocumentReport document

  rlReport : RL.RLReport
  rlReport =
    RL.ontologyDocumentReport document

ELReportEmpty : EL.ELReport → Type₀
ELReportEmpty report =
  EL.NoNonELFeatures (EL.nonELFeatures report)

QLReportEmpty : QL.QLReport → Type₀
QLReportEmpty report =
  QL.NoNonQLFeatures (QL.nonQLFeatures report)

RLReportEmpty : RL.RLReport → Type₀
RLReportEmpty report =
  RL.NoNonRLFeatures (RL.nonRLFeatures report)

NoReportNonELFeatures :
  ProfileRestrictionsReport → Type₀
NoReportNonELFeatures report =
  EL.NoNonELFeatures (profileRestrictionsNonELFeatures report)

NoReportNonQLFeatures :
  ProfileRestrictionsReport → Type₀
NoReportNonQLFeatures report =
  QL.NoNonQLFeatures (profileRestrictionsNonQLFeatures report)

NoReportNonRLFeatures :
  ProfileRestrictionsReport → Type₀
NoReportNonRLFeatures report =
  RL.NoNonRLFeatures (profileRestrictionsNonRLFeatures report)

NoNonELProfileFeatures :
  P.OntologyDocument → Type₀
NoNonELProfileFeatures document =
  NoReportNonELFeatures (reportProfileRestrictions document)

NoNonQLProfileFeatures :
  P.OntologyDocument → Type₀
NoNonQLProfileFeatures document =
  NoReportNonQLFeatures (reportProfileRestrictions document)

NoNonRLProfileFeatures :
  P.OntologyDocument → Type₀
NoNonRLProfileFeatures document =
  NoReportNonRLFeatures (reportProfileRestrictions document)

record AllProfileRestrictions
  (report : ProfileRestrictionsReport) : Type₀ where
  constructor allProfileRestrictions
  field
    allProfileRestrictionsEL :
      NoReportNonELFeatures report
    allProfileRestrictionsQL :
      NoReportNonQLFeatures report
    allProfileRestrictionsRL :
      NoReportNonRLFeatures report

open AllProfileRestrictions public

AllProfileDocument : P.OntologyDocument → Type₀
AllProfileDocument document =
  AllProfileRestrictions (reportProfileRestrictions document)