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

module Spartan6.Examples.HierarchyProvenance where

open import Spartan6.Prelude

import Cubical.Data.Empty as Empty
import Cubical.Data.Nat.Properties as Nat
import Spartan6.Hierarchy.Provenance as Provenance
import Spartan6.Netlist.Provenance as Netlist

scopeModule wrongModule : Netlist.ModuleId
scopeModule = Netlist.moduleId 0
wrongModule = Netlist.moduleId 1

scopeOrigin wrongOrigin : Provenance.SourceOrigin
scopeOrigin =
  Provenance.sourceOrigin nothing (just scopeModule) []ᴸ "scope"
wrongOrigin =
  Provenance.sourceOrigin nothing (just wrongModule) []ᴸ "wrong"

wrongNode : Provenance.NodeOrigin
wrongNode = Provenance.nodeOrigin wrongOrigin 0

moduleOrdinalOrZero : Maybe Netlist.ModuleId -> ℕ
moduleOrdinalOrZero nothing = 0
moduleOrdinalOrZero (just module-id) = Netlist.moduleOrdinal module-id

-- A node from another module cannot be accounted for by a leaf merely by
-- choosing a convenient occurrence path.  The module-retention field forces
-- the contradiction 1 = 0.

unrelated-module-origin-is-impossible :
  Provenance.NodeAccountedFor
    (Provenance.leafProvenance scopeOrigin) wrongNode
  -> Empty.⊥
unrelated-module-origin-is-impossible
  (Provenance.accountedLeaf within) =
  Nat.snotz
    (cong moduleOrdinalOrZero
      (Provenance.moduleRetained within))