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

module Spartan6.Netlist.Candidate where

open import Spartan6.Prelude

import Spartan6.Netlist.BuilderCore as Builder
import Spartan6.Netlist.Checked as Checked
import Spartan6.Netlist.Raw as Raw
import Spartan6.Netlist.TopInterface as Top
import Spartan6.Validation.Raw as Validation

-- Representation-independent boundary retained by every pure-combinational
-- compatibility normalizer.

record CheckedCombinationalCandidate : Type₀ where
  constructor checkedCombinationalCandidate
  field
    candidateSource          : Raw.RawDesign
    candidateStructuralProof : Validation.StructurallyValid candidateSource
    candidateInputCount      : ℕ
    candidateOutputCount     : ℕ
    candidateLocalCount      : ℕ
    candidateNetlist         :
      Checked.CheckedNetlist
        candidateInputCount candidateOutputCount 0 candidateLocalCount

open CheckedCombinationalCandidate public

finishCandidate :
  (design : Raw.RawDesign)
  → Validation.StructurallyValid design
  → (input-net-ids : List Raw.NetId)
  → (current : Builder.Builder (lengthList input-net-ids) 0)
  → List
      (Checked.Wire
        (lengthList input-net-ids) 0 (Builder.builderLocalCount current))
  → CheckedCombinationalCandidate
finishCandidate design structural-proof input-net-ids current outputs =
  checkedCombinationalCandidate
    design
    structural-proof
    (lengthList input-net-ids)
    (lengthList outputs)
    (Builder.builderLocalCount current)
    (Checked.checkedNetlist
      []
      (Builder.builderNodes current)
      (Top.listToVec outputs)
      [])

candidate-has-no-registers : (candidate : CheckedCombinationalCandidate)
  → Checked.checkedInitial (candidateNetlist candidate) ≡ []
candidate-has-no-registers candidate
  with Checked.checkedInitial (candidateNetlist candidate)
... | [] = refl

candidate-next-is-empty : (candidate : CheckedCombinationalCandidate)
  → Checked.checkedNext (candidateNetlist candidate) ≡ []
candidate-next-is-empty candidate
  with Checked.checkedNext (candidateNetlist candidate)
... | [] = refl