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

module Spartan6.Validation.Design where

open import Spartan6.Prelude

import Spartan6.Import.Artifact as Artifact
import Spartan6.Netlist.Provenance as Provenance
import Spartan6.Netlist.Raw as Raw
import Spartan6.Validation.DecodedDesign as Decoded
import Spartan6.Validation.Diagnostic as Diagnostic
import Spartan6.Validation.LocatedDiagnostic as Located
import Spartan6.Validation.Raw as Legacy

open import Agda.Builtin.String using (primShowNat)
open import Cubical.Foundations.Path using (inspect; [_]ᵢ)

deduplicate : List Raw.NetId → List Raw.NetId
deduplicate []ᴸ = []ᴸ
deduplicate (net ∷ᴸ nets) =
  if Legacy.containsNet net nets
  then deduplicate nets
  else net ∷ᴸ deduplicate nets

denseRawNets : Raw.RawDesign → List Raw.NetId
denseRawNets design =
  deduplicate (Legacy.designDrivers design ++ᴸ Legacy.designSinks design)

record ValidatedDesign (artifact : Artifact.RawArtifact) : Type₀ where
  constructor validatedDesign
  field
    decoded : Decoded.DecodedDesign artifact
    structuralEvidence :
      Legacy.StructurallyValid (Artifact.decodedDesign artifact)
    denseNetCorrespondence : List Provenance.DenseNetEntry
    denseNetCorrespondence-is-canonical :
      denseNetCorrespondence
      ≡ Provenance.enumerateDenseFrom 
          (denseRawNets (Artifact.decodedDesign artifact))
    validatedDrivers : List Raw.NetId
    validatedDrivers-are-source :
      validatedDrivers
      ≡ Legacy.designDrivers (Artifact.decodedDesign artifact)
    validatedSinks : List Raw.NetId
    validatedSinks-are-source :
      validatedSinks
      ≡ Legacy.designSinks (Artifact.decodedDesign artifact)
    validatedDependencies : List Legacy.Dependency
    validatedDependencies-are-source :
      validatedDependencies
      ≡ Legacy.designDependencies (Artifact.decodedDesign artifact)

open ValidatedDesign public

buildValidated : (artifact : Artifact.RawArtifact)
  → Decoded.DecodedDesign artifact
  → Legacy.StructurallyValid (Artifact.decodedDesign artifact)
  → ValidatedDesign artifact
buildValidated artifact decoded-design structural =
  validatedDesign decoded-design structural
    (Provenance.enumerateDenseFrom 
      (denseRawNets (Artifact.decodedDesign artifact))) refl
    (Legacy.designDrivers (Artifact.decodedDesign artifact)) refl
    (Legacy.designSinks (Artifact.decodedDesign artifact)) refl
    (Legacy.designDependencies (Artifact.decodedDesign artifact)) refl

artifactRoot : Artifact.RawArtifact → Located.DiagnosticLocation
artifactRoot artifact =
  Located.artifactLocation
    (Provenance.artifactId
      (Artifact.artifactDigest (Artifact.envelope artifact)))

internalEmptyRejection : Diagnostic.Diagnostic
internalEmptyRejection =
  Diagnostic.diagnostic Diagnostic.malformedImport Diagnostic.reject
    "validation result" "a nonempty rejection" "an empty rejection list"
    "The compatibility diagnostic type permits an empty rejection; the staged validator makes that state nonempty explicitly."

locateAll : Located.DiagnosticLocation → Diagnostic.Diagnostics
  → Located.NonEmpty Located.LocatedDiagnostic
locateAll location []ᴸ =
  Located.locatedDiagnostic location internalEmptyRejection Located.∷⁺ []ᴸ
locateAll location (problem ∷ᴸ problems) =
  Located.locatedDiagnostic location problem Located.∷⁺
    mapList (Located.locatedDiagnostic location) problems

validateConnected : (artifact : Artifact.RawArtifact)
  → Decoded.DecodedDesign artifact
  → Located.ValidationResult (ValidatedDesign artifact)
validateConnected artifact decoded-design with
  Legacy.structureDiagnostics (Artifact.decodedDesign artifact)
  | inspect Legacy.structureDiagnostics (Artifact.decodedDesign artifact)
... | problem ∷ᴸ problems | [ structural ]ᵢ =
  Located.invalid []ᴸ
    (locateAll (artifactRoot artifact) (problem ∷ᴸ problems))
... | []ᴸ | [ structural ]ᵢ =
  Located.valid []ᴸ (buildValidated artifact decoded-design structural)

validateArtifact : (artifact : Artifact.RawArtifact)
  → Located.ValidationResult (ValidatedDesign artifact)
validateArtifact artifact with Decoded.decodeDesign artifact
... | Diagnostic.rejected diagnostics =
  Located.invalid []ᴸ (locateAll (artifactRoot artifact) diagnostics)
... | Diagnostic.accepted decoded-design =
  validateConnected artifact decoded-design

validateArtifactLegacy : (artifact : Artifact.RawArtifact)
  → Diagnostic.CheckResult (ValidatedDesign artifact)
validateArtifactLegacy artifact =
  Located.toCheckResult (validateArtifact artifact)

validated-digest-preserved : (artifact : Artifact.RawArtifact)
  → ValidatedDesign artifact
  → Artifact.artifactDigest (Artifact.envelope artifact)
    ≡ Artifact.artifactDigest (Artifact.envelope artifact)
validated-digest-preserved artifact validated = refl