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

module OWL2.Diagnostics.Algebra where

open import OWL2.Prelude
open import OWL2.Foundation.List
open import OWL2.Diagnostics.Core

Diagnostics : Type₀
Diagnostics =
  List Diagnostic

CleanDiagnostics : Diagnostics → Type₀
CleanDiagnostics diagnostics =
  Empty diagnostics

diagnosticsClean? : Diagnostics → Bool
diagnosticsClean? diagnostics =
  isEmpty? diagnostics

noDiagnostics : Diagnostics
noDiagnostics =
  []

singleDiagnostic : Diagnostic → Diagnostics
singleDiagnostic d =
  d ∷ []

appendDiagnostics : Diagnostics → Diagnostics → Diagnostics
appendDiagnostics left right =
  left ++ right

cleanAppendLeft :
  (left right : Diagnostics) →
  CleanDiagnostics (left ++ right) →
  CleanDiagnostics left
cleanAppendLeft [] right clean =
  tt
cleanAppendLeft (d ∷ left) right clean =
  clean

cleanAppendRight :
  (left right : Diagnostics) →
  CleanDiagnostics (left ++ right) →
  CleanDiagnostics right
cleanAppendRight [] right clean =
  clean
cleanAppendRight (d ∷ left) right ()

emitIf : Bool → Diagnostic → Diagnostics
emitIf true d =
  singleDiagnostic d
emitIf false d =
  noDiagnostics