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

module Spartan6.Validation.CycleFuel where

open import Spartan6.Prelude
open import Spartan6.Validation.CycleSoundness
  using (_∈_; here; there;
         DependencyEdge; edgeHere; edgeThere;
         ReachableWithin; atTarget; followEdge;
         CycleWithin; someDependencyCycles-complete;
         combinationalCycle?-complete)

import Spartan6.Netlist.Raw as Raw
import Spartan6.Validation.Raw as Validation

private
  variable
    ℓ : Level

listToVec : ∀ {A : Type ℓ} (items : List A) → Vec A (lengthList items)
listToVec []ᴸ = []
listToVec (item ∷ᴸ items) = item ∷ listToVec items

removeAt : ∀ {A : Type ℓ} {size}
         → Fin (suc size)
         → Vec A (suc size)
         → Vec A size
removeAt fzero (item ∷ items) = items
removeAt {size = suc size} (fsuc index) (item ∷ items) =
  item ∷ removeAt index items

-- EdgeTrail has no search-fuel index.  Instead it carries the finite vector
-- of edge occurrences that remain available.  A step removes its selected
-- occurrence, so the same list position cannot be used twice.  Equal-valued
-- duplicate edges remain distinct occurrences, exactly as in Validation.Raw.

data EdgeTrail
  (all-edges : List Validation.Dependency)
  : ∀ {remaining}
    → Vec Validation.Dependency remaining
    → Raw.NetId
    → Raw.NetId
    → Type₀ where
  trailDone : ∀ {remaining}
    {available : Vec Validation.Dependency remaining}
    {current target}
    → current ≡ target
    → EdgeTrail all-edges available current target

  trailStep : ∀ {remaining}
    {available : Vec Validation.Dependency (suc remaining)}
    {current next target}
    (index : Fin (suc remaining))
    → current
      ≡ Validation.Dependency.dependencySource (lookup index available)
    → next
      ≡ Validation.Dependency.dependencyTarget (lookup index available)
    → lookup index available ∈ all-edges
    → EdgeTrail
        all-edges
        (removeAt index available)
        next
        target
    → EdgeTrail all-edges available current target

listed-edge : ∀ {edge edges source target}
  → edge ∈ edges
  → source ≡ Validation.Dependency.dependencySource edge
  → target ≡ Validation.Dependency.dependencyTarget edge
  → DependencyEdge source target edges
listed-edge here source-path target-path =
  edgeHere source-path target-path
listed-edge (there membership) source-path target-path =
  edgeThere (listed-edge membership source-path target-path)

-- The fuel bound is derived from the number of still-available occurrences.

trail-reachable : ∀ {all-edges remaining}
  {available : Vec Validation.Dependency remaining}
  {current target}
  → EdgeTrail all-edges available current target
  → ReachableWithin all-edges target remaining current
trail-reachable (trailDone equality) = atTarget equality
trail-reachable
  (trailStep index source-path target-path membership rest) =
  followEdge
    (listed-edge membership source-path target-path)
    (trail-reachable rest)

weaken-reachable : ∀ {edges target fuel current}
  → ReachableWithin edges target fuel current
  → ReachableWithin edges target (suc fuel) current
weaken-reachable (atTarget equality) = atTarget equality
weaken-reachable (followEdge edge path) =
  followEdge edge (weaken-reachable path)

-- A genuine finite listed-graph cycle consists of one listed closing edge and
-- an edge-occurrence-simple return trail.  There is deliberately no fuel in
-- this definition.  This is the usual finite closed-trail presentation of a
-- cycle; self-loops use trailDone as their return trail.

record GenuineCycle (edges : List Validation.Dependency) : Type₀ where
  constructor genuineCycle
  field
    closingEdge       : Validation.Dependency
    closingEdgeListed : closingEdge ∈ edges
    returnTrail       :
      EdgeTrail
        edges
        (listToVec edges)
        (Validation.Dependency.dependencyTarget closingEdge)
        (Validation.Dependency.dependencySource closingEdge)

open GenuineCycle public

genuine-cycle-within-detector-fuel : ∀ {edges}
  → GenuineCycle edges
  → CycleWithin (suc (lengthList edges)) edges edges
genuine-cycle-within-detector-fuel cycle =
  closingEdge cycle
  , closingEdgeListed cycle
  , weaken-reachable (trail-reachable (returnTrail cycle))

genuine-cycle-detected : ∀ {edges}
  → GenuineCycle edges
  → Validation.someDependencyCycles
      (suc (lengthList edges)) edges edges
    ≡ true
genuine-cycle-detected cycle =
  someDependencyCycles-complete
    (genuine-cycle-within-detector-fuel cycle)

DesignCycle : Raw.RawDesign → Type₀
DesignCycle design = GenuineCycle (Validation.designDependencies design)

design-cycle-detected : ∀ design
  → DesignCycle design
  → Validation.combinationalCycle? design ≡ true
design-cycle-detected design cycle =
  combinationalCycle?-complete
    design
    (genuine-cycle-within-detector-fuel cycle)