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

module OWL2.Diagnostics.Core where

open import OWL2.Prelude

record DiagnosticCode : Type₀ where
  constructor mkDiagnosticCode
  field
    diagnosticCodeNamespace :
      String
    diagnosticCodeName :
      String

open DiagnosticCode public

data Severity : Type₀ where
  severityInfo :
    Severity
  severityWarning :
    Severity
  severityError :
    Severity
  severityFatal :
    Severity

data SourcePathSegment : Type₀ where
  fieldSegment :
    String → SourcePathSegment
  indexSegment :
    ℕ → SourcePathSegment
  opaqueSegment :
    String → SourcePathSegment

record SourcePath : Type₀ where
  constructor sourcePath
  field
    sourcePathSegments :
      List SourcePathSegment

open SourcePath public

rootSourcePath : SourcePath
rootSourcePath =
  sourcePath []

record Diagnostic : Type₀ where
  constructor diagnostic
  field
    diagnosticCode :
      DiagnosticCode
    diagnosticSeverity :
      Severity
    diagnosticSourcePath :
      SourcePath
    diagnosticMessage :
      String

open Diagnostic public