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

module Spartan6.Validation.LocatedDiagnostic where

open import Spartan6.Prelude
import Spartan6.Import.Json as Json
import Spartan6.Netlist.Provenance as Provenance
import Spartan6.Validation.Diagnostic as Legacy

open import Cubical.Data.Bool.Properties using (false≢true)
import Cubical.Data.Empty as Empty

data DiagnosticLocation : Type₀ where
  artifactLocation : Provenance.ArtifactId → DiagnosticLocation
  jsonLocation : Json.JsonPath → DiagnosticLocation
  occurrenceLocation : Provenance.OccurrenceId → DiagnosticLocation
  portLocation : Provenance.PortId → DiagnosticLocation
  netLocation : Provenance.LogicalNetId → DiagnosticLocation

record LocatedDiagnostic : Type₀ where
  constructor locatedDiagnostic
  field
    diagnosticLocation : DiagnosticLocation
    legacyDiagnostic : Legacy.Diagnostic

open LocatedDiagnostic public

data NonEmpty (A : Type₀) : Type₀ where
  _∷⁺_ : A → List A → NonEmpty A

infixr  _∷⁺_

nonEmptyToList : ∀ {A} → NonEmpty A → List A
nonEmptyToList (item ∷⁺ items) = item ∷ᴸ items

mapNonEmpty : ∀ {A B} → (A → B) → NonEmpty A → NonEmpty B
mapNonEmpty function (item ∷⁺ items) =
  function item ∷⁺ mapList function items

data ValidationResult (A : Type₀) : Type₀ where
  valid : List LocatedDiagnostic → A → ValidationResult A
  invalid : List LocatedDiagnostic → NonEmpty LocatedDiagnostic
          → ValidationResult A

mapValidation : ∀ {A B} → (A → B) → ValidationResult A
  → ValidationResult B
mapValidation function (valid warnings value) =
  valid warnings (function value)
mapValidation function (invalid warnings errors) = invalid warnings errors

legacyDiagnostics : List LocatedDiagnostic → Legacy.Diagnostics
legacyDiagnostics []ᴸ = []ᴸ
legacyDiagnostics (problem ∷ᴸ problems) =
  legacyDiagnostic problem ∷ᴸ legacyDiagnostics problems

toCheckResult : ∀ {A} → ValidationResult A → Legacy.CheckResult A
toCheckResult (valid warnings value) = Legacy.accepted value
toCheckResult (invalid warnings errors) =
  Legacy.rejected (legacyDiagnostics (nonEmptyToList errors))

isValid : ∀ {A} → ValidationResult A → Bool
isValid (valid warnings value) = true
isValid (invalid warnings errors) = false

extractValid : ∀ {A} → (result : ValidationResult A)
  → isValid result ≡ true → A
extractValid (valid warnings value) proof = value
extractValid (invalid warnings errors) proof =
  Empty.rec (false≢true proof)