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

module Spartan6.Validation.Diagnostic where

open import Spartan6.Prelude

data DiagnosticCode : Type₀ where
  malformedImport        : DiagnosticCode
  unknownPrimitive       : DiagnosticCode
  unsupportedMode        : DiagnosticCode
  illegalParameter       : DiagnosticCode
  malformedInitialisation : DiagnosticCode
  missingPort            : DiagnosticCode
  unknownPort            : DiagnosticCode
  directionMismatch      : DiagnosticCode
  widthMismatch          : DiagnosticCode
  undrivenInput           : DiagnosticCode
  multipleDriver         : DiagnosticCode
  combinationalLoop      : DiagnosticCode
  unresolvedBlackBox     : DiagnosticCode
  unsupportedEvent       : DiagnosticCode
  contradictoryTarget    : DiagnosticCode

data Severity : Type₀ where
  reject     : Severity
  quarantine : Severity

record Diagnostic : Type₀ where
  constructor diagnostic
  field
    diagnosticCode     : DiagnosticCode
    diagnosticSeverity : Severity
    diagnosticSubject  : String
    diagnosticExpected : String
    diagnosticObserved : String
    diagnosticDetail   : String

open Diagnostic public

Diagnostics : Type₀
Diagnostics = List Diagnostic

data CheckResult (A : Type₀) : Type₀ where
  accepted : A → CheckResult A
  rejected : Diagnostics → CheckResult A

mapResult : ∀ {A B : Type₀} → (A → B) → CheckResult A → CheckResult B
mapResult function (accepted value) = accepted (function value)
mapResult function (rejected diagnostics) = rejected diagnostics

appendResult : ∀ {A B : Type₀}
             → CheckResult A → CheckResult B → CheckResult (A × B)
appendResult (accepted left) (accepted right) = accepted (left , right)
appendResult (rejected left) (accepted right) = rejected left
appendResult (accepted left) (rejected right) = rejected right
appendResult (rejected left) (rejected right) = rejected (left ++ᴸ right)

map-accepted : ∀ {A B : Type₀} (function : A → B) value
             → mapResult function (accepted value) ≡ accepted (function value)
map-accepted function value = refl

map-rejected : ∀ {A B : Type₀} (function : A → B) diagnostics
             → mapResult function (rejected diagnostics) ≡ rejected diagnostics
map-rejected function diagnostics = refl