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

module Spartan6.Hierarchy.Provenance where

open import Spartan6.Prelude
open import Spartan6.Hierarchy.Interface using (appendVec)

import Spartan6.Netlist.Provenance as Netlist

record ComponentIdentity : Type₀ where
  constructor componentIdentity
  field
    identityStableId : ℕ
    identityName : String

open ComponentIdentity public

record InstanceIdentity : Type₀ where
  constructor instanceIdentity
  field
    instanceOccurrence : Netlist.OccurrenceId
    instanceName : String

open InstanceIdentity public

record SourceOrigin : Type₀ where
  constructor sourceOrigin
  field
    originArtifact : Maybe Netlist.ArtifactId
    originModule : Maybe Netlist.ModuleId
    originInstancePath : List Netlist.OccurrenceId
    originLabel : String

open SourceOrigin public

prependInstance : Netlist.OccurrenceId -> SourceOrigin -> SourceOrigin
prependInstance occurrence
  (sourceOrigin artifact module-id path label) =
  sourceOrigin artifact module-id (occurrence ∷ᴸ path) label

record NodeOrigin : Type₀ where
  constructor nodeOrigin
  field
    nodeSource : SourceOrigin
    sourceLocalOrdinal : ℕ

open NodeOrigin public

data HierarchyProvenance : Type₀ where
  leafProvenance : SourceOrigin -> HierarchyProvenance
  instantiatedProvenance : Netlist.OccurrenceId -> String
    -> HierarchyProvenance -> HierarchyProvenance
  renamedProvenance : String
    -> HierarchyProvenance -> HierarchyProvenance
  serialProvenance : HierarchyProvenance -> HierarchyProvenance
    -> HierarchyProvenance
  parallelProvenance : HierarchyProvenance -> HierarchyProvenance
    -> HierarchyProvenance
  hiddenProvenance : String
    -> HierarchyProvenance -> HierarchyProvenance
  feedbackProvenance : String
    -> HierarchyProvenance -> HierarchyProvenance

mapNodeInstance : Netlist.OccurrenceId -> NodeOrigin -> NodeOrigin
mapNodeInstance occurrence (nodeOrigin source ordinal) =
  nodeOrigin (prependInstance occurrence source) ordinal

mapNodeOrigins : ∀ {count}
  -> Netlist.OccurrenceId -> Vec NodeOrigin count -> Vec NodeOrigin count
mapNodeOrigins occurrence [] = []
mapNodeOrigins occurrence (origin ∷ origins) =
  mapNodeInstance occurrence origin ∷ mapNodeOrigins occurrence origins

mapNodeOrigins-length-preserved : ∀ {count}
  (occurrence : Netlist.OccurrenceId)
  (origins : Vec NodeOrigin count)
  -> mapNodeOrigins occurrence origins
    ≡ map (mapNodeInstance occurrence) origins
mapNodeOrigins-length-preserved occurrence [] = refl
mapNodeOrigins-length-preserved occurrence (origin ∷ origins) =
  cong (mapNodeInstance occurrence origin ∷_)
    (mapNodeOrigins-length-preserved occurrence origins)

-- Certified hierarchy accounting -----------------------------------------

-- A hierarchy leaf may summarize a design containing several primitive
-- nodes.  A node is within that leaf when artifact and module identities are
-- retained and its instance path extends the leaf's path.  Labels remain
-- diagnostic descriptions rather than semantic identities.

record SourceWithin (scope source : SourceOrigin) : Type₀ where
  constructor sourceWithin
  field
    artifactRetained : originArtifact source ≡ originArtifact scope
    moduleRetained : originModule source ≡ originModule scope
    pathSuffix : List Netlist.OccurrenceId
    pathExtended :
      originInstancePath source
      ≡ originInstancePath scope ++ᴸ pathSuffix

open SourceWithin public

data NodeAccountedFor : HierarchyProvenance -> NodeOrigin -> Type₀ where
  accountedLeaf : ∀ {scope node}
    -> SourceWithin scope (nodeSource node)
    -> NodeAccountedFor (leafProvenance scope) node

  accountedInstantiated : ∀ {occurrence name hierarchy node}
    -> NodeAccountedFor hierarchy node
    -> NodeAccountedFor
        (instantiatedProvenance occurrence name hierarchy)
        (mapNodeInstance occurrence node)

  accountedRenamed : ∀ {name hierarchy node}
    -> NodeAccountedFor hierarchy node
    -> NodeAccountedFor (renamedProvenance name hierarchy) node

  accountedSerialLeft : ∀ {left right node}
    -> NodeAccountedFor left node
    -> NodeAccountedFor (serialProvenance left right) node

  accountedSerialRight : ∀ {left right node}
    -> NodeAccountedFor right node
    -> NodeAccountedFor (serialProvenance left right) node

  accountedParallelLeft : ∀ {left right node}
    -> NodeAccountedFor left node
    -> NodeAccountedFor (parallelProvenance left right) node

  accountedParallelRight : ∀ {left right node}
    -> NodeAccountedFor right node
    -> NodeAccountedFor (parallelProvenance left right) node

  accountedHidden : ∀ {name hierarchy node}
    -> NodeAccountedFor hierarchy node
    -> NodeAccountedFor (hiddenProvenance name hierarchy) node

  accountedFeedback : ∀ {name hierarchy node}
    -> NodeAccountedFor hierarchy node
    -> NodeAccountedFor (feedbackProvenance name hierarchy) node

data NodesAccountedFor (hierarchy : HierarchyProvenance) :
  ∀ {count} -> Vec NodeOrigin count -> Type₀ where
  accountedNodesDone : NodesAccountedFor hierarchy []
  accountedNodesNext : ∀ {count node}
    {nodes : Vec NodeOrigin count}
    -> NodeAccountedFor hierarchy node
    -> NodesAccountedFor hierarchy nodes
    -> NodesAccountedFor hierarchy (node ∷ nodes)

mapNodeOrigins-accounted : ∀ {hierarchy count}
  (occurrence : Netlist.OccurrenceId) (name : String)
  {nodes : Vec NodeOrigin count}
  -> NodesAccountedFor hierarchy nodes
  -> NodesAccountedFor
      (instantiatedProvenance occurrence name hierarchy)
      (mapNodeOrigins occurrence nodes)
mapNodeOrigins-accounted occurrence name accountedNodesDone =
  accountedNodesDone
mapNodeOrigins-accounted occurrence name
  (accountedNodesNext node-accounted nodes-accounted) =
  accountedNodesNext
    (accountedInstantiated node-accounted)
    (mapNodeOrigins-accounted occurrence name nodes-accounted)

serial-left-accounted : ∀ {left right count}
  {nodes : Vec NodeOrigin count}
  -> NodesAccountedFor left nodes
  -> NodesAccountedFor (serialProvenance left right) nodes
serial-left-accounted accountedNodesDone = accountedNodesDone
serial-left-accounted
  (accountedNodesNext node-accounted nodes-accounted) =
  accountedNodesNext
    (accountedSerialLeft node-accounted)
    (serial-left-accounted nodes-accounted)

serial-right-accounted : ∀ {left right count}
  {nodes : Vec NodeOrigin count}
  -> NodesAccountedFor right nodes
  -> NodesAccountedFor (serialProvenance left right) nodes
serial-right-accounted accountedNodesDone = accountedNodesDone
serial-right-accounted
  (accountedNodesNext node-accounted nodes-accounted) =
  accountedNodesNext
    (accountedSerialRight node-accounted)
    (serial-right-accounted nodes-accounted)

parallel-left-accounted : ∀ {left right count}
  {nodes : Vec NodeOrigin count}
  -> NodesAccountedFor left nodes
  -> NodesAccountedFor (parallelProvenance left right) nodes
parallel-left-accounted accountedNodesDone = accountedNodesDone
parallel-left-accounted
  (accountedNodesNext node-accounted nodes-accounted) =
  accountedNodesNext
    (accountedParallelLeft node-accounted)
    (parallel-left-accounted nodes-accounted)

parallel-right-accounted : ∀ {left right count}
  {nodes : Vec NodeOrigin count}
  -> NodesAccountedFor right nodes
  -> NodesAccountedFor (parallelProvenance left right) nodes
parallel-right-accounted accountedNodesDone = accountedNodesDone
parallel-right-accounted
  (accountedNodesNext node-accounted nodes-accounted) =
  accountedNodesNext
    (accountedParallelRight node-accounted)
    (parallel-right-accounted nodes-accounted)

append-accounted : ∀ {hierarchy leftCount rightCount}
  {left : Vec NodeOrigin leftCount}
  {right : Vec NodeOrigin rightCount}
  -> NodesAccountedFor hierarchy left
  -> NodesAccountedFor hierarchy right
  -> NodesAccountedFor hierarchy (appendVec left right)
append-accounted accountedNodesDone right-accounted = right-accounted
append-accounted
  (accountedNodesNext node-accounted nodes-accounted) right-accounted =
  accountedNodesNext node-accounted
    (append-accounted nodes-accounted right-accounted)

serial-instances-accounted : ∀ {left right leftCount rightCount}
  (left-occurrence : Netlist.OccurrenceId) (left-name : String)
  (right-occurrence : Netlist.OccurrenceId) (right-name : String)
  {left-nodes : Vec NodeOrigin leftCount}
  {right-nodes : Vec NodeOrigin rightCount}
  -> NodesAccountedFor left left-nodes
  -> NodesAccountedFor right right-nodes
  -> NodesAccountedFor
      (serialProvenance
        (instantiatedProvenance left-occurrence left-name left)
        (instantiatedProvenance right-occurrence right-name right))
      (appendVec
        (mapNodeOrigins left-occurrence left-nodes)
        (mapNodeOrigins right-occurrence right-nodes))
serial-instances-accounted left-occurrence left-name
  right-occurrence right-name left-accounted right-accounted =
  append-accounted
    (serial-left-accounted
      (mapNodeOrigins-accounted
        left-occurrence left-name left-accounted))
    (serial-right-accounted
      (mapNodeOrigins-accounted
        right-occurrence right-name right-accounted))

parallel-instances-accounted : ∀ {left right leftCount rightCount}
  (left-occurrence : Netlist.OccurrenceId) (left-name : String)
  (right-occurrence : Netlist.OccurrenceId) (right-name : String)
  {left-nodes : Vec NodeOrigin leftCount}
  {right-nodes : Vec NodeOrigin rightCount}
  -> NodesAccountedFor left left-nodes
  -> NodesAccountedFor right right-nodes
  -> NodesAccountedFor
      (parallelProvenance
        (instantiatedProvenance left-occurrence left-name left)
        (instantiatedProvenance right-occurrence right-name right))
      (appendVec
        (mapNodeOrigins left-occurrence left-nodes)
        (mapNodeOrigins right-occurrence right-nodes))
parallel-instances-accounted left-occurrence left-name
  right-occurrence right-name left-accounted right-accounted =
  append-accounted
    (parallel-left-accounted
      (mapNodeOrigins-accounted
        left-occurrence left-name left-accounted))
    (parallel-right-accounted
      (mapNodeOrigins-accounted
        right-occurrence right-name right-accounted))