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

module Spartan6.Netlist.Provenance where

open import Spartan6.Prelude
import Spartan6.Netlist.Raw as Raw

record ArtifactId : Type₀ where
  constructor artifactId
  field artifactDigestId : String

record ModuleId : Type₀ where
  constructor moduleId
  field moduleOrdinal : ℕ

record OccurrenceId : Type₀ where
  constructor occurrenceId
  field occurrenceOrdinal : ℕ

record PortId : Type₀ where
  constructor portId
  field portOccurrence : OccurrenceId
        portOrdinal : ℕ

record LogicalNetId : Type₀ where
  constructor logicalNetId
  field logicalNetOrdinal : ℕ

open ArtifactId public
open ModuleId public
open OccurrenceId public
open PortId public
open LogicalNetId public

record DenseNetEntry : Type₀ where
  constructor denseNetEntry
  field
    denseNetId : LogicalNetId
    retainedRawNetId : Raw.NetId

open DenseNetEntry public

enumerateDenseFrom : ℕ → List Raw.NetId → List DenseNetEntry
enumerateDenseFrom next []ᴸ = []ᴸ
enumerateDenseFrom next (raw ∷ᴸ raws) =
  denseNetEntry (logicalNetId next) raw
  ∷ᴸ enumerateDenseFrom (suc next) raws