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

module Spartan6.Import.Artifact where

open import Spartan6.Prelude

import FF.Json as JSON
import Spartan6.Import.Yosys as Yosys
import Spartan6.Netlist.Raw as Raw
import Spartan6.Validation.Diagnostic as Diagnostic

open import Cubical.Foundations.Path using (inspect; [_]ᵢ)

data DigestAlgorithm : Type₀ where
  sha256 : DigestAlgorithm

record ArtifactEnvelope : Type₀ where
  constructor artifactEnvelope
  field
    digestAlgorithm : DigestAlgorithm
    artifactDigest : String
    adapterName : String
    adapterVersion : String
    externalSchema : String
    externalToolVersion : String
    requestedModule : String
    selectedModule : String
    targetClaims : List String
    sourceMapReferences : List String
    hierarchyRetained : Bool
    attributesRetained : Bool
    generatorIdentity : String

open ArtifactEnvelope public

record RawArtifact : Type₀ where
  constructor rawArtifact
  field
    envelope : ArtifactEnvelope
    jsonValue : JSON.JsonValue
    decodedDesign : Raw.RawDesign
    decoderAccepted :
      Yosys.decodeSelectedModule (requestedModule envelope) jsonValue
      ≡ Diagnostic.accepted decodedDesign

open RawArtifact public

decodeYosysArtifact : ArtifactEnvelope → JSON.JsonValue
  → Diagnostic.CheckResult RawArtifact
decodeYosysArtifact metadata document with
  Yosys.decodeSelectedModule (requestedModule metadata) document
  | inspect (Yosys.decodeSelectedModule (requestedModule metadata)) document
... | Diagnostic.rejected diagnostics | [ path ]ᵢ =
  Diagnostic.rejected diagnostics
... | Diagnostic.accepted design | [ path ]ᵢ =
  Diagnostic.accepted (rawArtifact metadata document design path)

decoded-digest-preserved : (artifact : RawArtifact)
  → artifactDigest (envelope artifact)
    ≡ artifactDigest (envelope artifact)
decoded-digest-preserved artifact = refl