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

module Spartan6.Netlist.AdmissionCore where

open import Spartan6.Prelude

import Spartan6.Architecture.Primitive as Architecture
import Spartan6.Netlist.AdmissionCombinational as Combinational
import Spartan6.Netlist.AdmissionMixed as Mixed
import Spartan6.Netlist.Candidate as Candidate
import Spartan6.Netlist.NormalizeMixed as NormalizeMixed
import Spartan6.Netlist.Raw as Raw
import Spartan6.Semantics.Design as Semantics
import Spartan6.Validation.Diagnostic as Diagnostic
import Spartan6.Validation.Raw as Validation

-- The public restricted core dispatches by the presence of the two scalar
-- register kinds implemented by the mixed translator.  This avoids trying one
-- translator after another and accidentally replacing the most relevant
-- rejection diagnostics.  Other stateful kinds remain unsupported and are
-- rejected by the pure builder unless and until they receive their own
-- witnessed admission route.

scalarRegisterKind? : Architecture.PrimitiveKind → Bool
scalarRegisterKind? Architecture.FDRE = true
scalarRegisterKind? Architecture.FDSE = true
scalarRegisterKind? kind = false

scalarRegisterInstance? : Raw.RawInstance → Bool
scalarRegisterInstance? item with Raw.rawInstanceKind item
... | Raw.unknownPrimitive name = false
... | Raw.knownPrimitive kind = scalarRegisterKind? kind

someScalarRegister? : List Raw.RawInstance → Bool
someScalarRegister? []ᴸ = false
someScalarRegister? (item ∷ᴸ items) =
  scalarRegisterInstance? item or someScalarRegister? items

designHasScalarRegister? : Raw.RawDesign → Bool
designHasScalarRegister? design =
  someScalarRegister? (Raw.rawInstances design)

-- Both constructors carry the richer exact-design admission object from the
-- selected route.  Neither constructor opens ArchitectureProfile or claims a
-- selected device/silicon correspondence.

data RestrictedCoreAdmission : Type₀ where
  admittedCombinational :
    Combinational.RestrictedCombinationalAdmission
    → RestrictedCoreAdmission
  admittedMixed :
    Mixed.RestrictedMixedAdmission
    → RestrictedCoreAdmission

promoteCombinational :
  Combinational.RestrictedCombinationalAdmission
  → RestrictedCoreAdmission
promoteCombinational = admittedCombinational

promoteMixed :
  Mixed.RestrictedMixedAdmission
  → RestrictedCoreAdmission
promoteMixed = admittedMixed

admitRestrictedCore :
  Validation.StructurallyChecked
  → Diagnostic.CheckResult RestrictedCoreAdmission
admitRestrictedCore checked with designHasScalarRegister? (fst checked)
... | false =
  Diagnostic.mapResult promoteCombinational
    (Combinational.admitRestrictedCombinational checked)
... | true =
  Diagnostic.mapResult promoteMixed
    (Mixed.admitRestrictedMixed checked)

admittedRawSource : RestrictedCoreAdmission → Raw.RawDesign
admittedRawSource
  (admittedCombinational (design , membership)) = design
admittedRawSource (admittedMixed (design , membership)) = design

-- Existentially package the width-indexed executable semantics behind the
-- unified route.  Eliminating this record reveals the exact vector widths;
-- no dynamic casts or untyped signal arrays enter the semantic core.

record ExecutableCore : Type₀ where
  constructor executableCore
  field
    executableInputCount    : ℕ
    executableOutputCount   : ℕ
    executableRegisterCount : ℕ
    executableDesign :
      Semantics.Design
        executableInputCount
        executableOutputCount
        executableRegisterCount

open ExecutableCore public

admittedExecutable : RestrictedCoreAdmission → ExecutableCore
admittedExecutable
  (admittedCombinational (design , membership)) =
  executableCore
    (Candidate.candidateInputCount
      (Combinational.admittedCandidate membership))
    (Candidate.candidateOutputCount
      (Combinational.admittedCandidate membership))
    
    (Combinational.admittedSemantics membership)
admittedExecutable (admittedMixed (design , membership)) =
  executableCore
    (NormalizeMixed.candidateInputCount
      (Mixed.admittedCandidate membership))
    (NormalizeMixed.candidateOutputCount
      (Mixed.admittedCandidate membership))
    (NormalizeMixed.candidateRegisterCount
      (Mixed.admittedCandidate membership))
    (Mixed.admittedSemantics membership)

-- Reduction checks pin dispatch independently of the larger examples.

emptyRawDesign : Raw.RawDesign
emptyRawDesign = Raw.rawDesign nothing []ᴸ []ᴸ

empty-design-uses-combinational-route :
  designHasScalarRegister? emptyRawDesign ≡ false
empty-design-uses-combinational-route = refl

dummyFDRE : Raw.RawInstance
dummyFDRE =
  Raw.rawInstance
    "dispatch-only"
    (Raw.knownPrimitive Architecture.FDRE)
    []ᴸ []ᴸ nothing

fdre-design-uses-mixed-route :
  designHasScalarRegister?
    (Raw.rawDesign nothing []ᴸ (dummyFDRE ∷ᴸ []ᴸ))
  ≡ true
fdre-design-uses-mixed-route = refl