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

module Spartan6.Netlist.AdmissionCombinational where

open import Spartan6.Prelude

import Spartan6.Architecture.Profile as Profile
import Spartan6.Netlist.Candidate as Candidate
import Spartan6.Netlist.Checked as Checked
import Spartan6.Netlist.NormalizeScheduledCombinational as Normalize
import Spartan6.Netlist.NormalizeScheduledCombinationalSoundness as Soundness
import Spartan6.Netlist.Raw as Raw
import Spartan6.Semantics.Design as Semantics
import Spartan6.Semantics.Execution as Execution
import Spartan6.Validation.Diagnostic as Diagnostic
import Spartan6.Validation.Raw as Validation

open import Cubical.Foundations.Path using (inspect; [_]ᵢ)

-- Pure-combinational admission is exact-design evidence, not permission for
-- every occurrence of a primitive kind.  It retains the raw/structural
-- boundary, the successful translation equation, the accepted canonical mode
-- of every source instance, and the intrinsic zero-register invariant.

data CombinationalAdmissionScope : Type₀ where
  restrictedCombinationalCandidate : CombinationalAdmissionScope

record RestrictedCombinationalProfile
  (design : Raw.RawDesign) : Type₀ where
  constructor restrictedCombinationalProfile
  field
    admittedStructuralProof : Validation.StructurallyValid design
    admittedCandidate : Candidate.CheckedCombinationalCandidate
    translationAccepted :
      Normalize.normaliseScheduledCombinational
        (design , admittedStructuralProof)
      ≡ Diagnostic.accepted admittedCandidate
    translationWitness :
      Soundness.ScheduledCombinationalBuildWitness
        design admittedStructuralProof admittedCandidate
    admissionScope : CombinationalAdmissionScope

open RestrictedCombinationalProfile public

RestrictedCombinationalAdmission : Type₀
RestrictedCombinationalAdmission =
  Σ Raw.RawDesign RestrictedCombinationalProfile

admitRestrictedCombinational :
  Validation.StructurallyChecked
  → Diagnostic.CheckResult RestrictedCombinationalAdmission
admitRestrictedCombinational checked
  with Normalize.normaliseScheduledCombinational checked
     | inspect Normalize.normaliseScheduledCombinational checked
... | Diagnostic.rejected diagnostics | [ result-path ]ᵢ =
  Diagnostic.rejected diagnostics
... | Diagnostic.accepted candidate | [ result-path ]ᵢ =
  Diagnostic.accepted
    ( fst checked
    , restrictedCombinationalProfile
        (snd checked)
        candidate
        result-path
        (Soundness.normaliseScheduledCombinational-witness
          checked candidate result-path)
        restrictedCombinationalCandidate
    )

development-profile-remains-closed : ∀ kind
  → Profile.profileAdmits? Profile.developmentProfile kind ≡ false
development-profile-remains-closed =
  Profile.development-profile-is-closed

admitted-candidate-preserves-source :
  ∀ {design} (membership : RestrictedCombinationalProfile design)
  → Candidate.candidateSource (admittedCandidate membership) ≡ design
admitted-candidate-preserves-source {design} membership =
  Soundness.candidate-source-preserved
    (translationWitness membership)

-- The checked candidate compiles directly to the deterministic executable
-- semantics used by the rest of the library.  Its register index is
-- definitionally zero.

admittedSemantics :
  ∀ {design}
  → (membership : RestrictedCombinationalProfile design)
  → Semantics.Design
      (Candidate.candidateInputCount (admittedCandidate membership))
      (Candidate.candidateOutputCount (admittedCandidate membership))
      
admittedSemantics membership =
  Checked.compileNetlist
    (Candidate.candidateNetlist (admittedCandidate membership))

admitted-observation-deterministic :
  ∀ {design}
  → (membership : RestrictedCombinationalProfile design)
  → {external : Semantics.Inputs (admittedSemantics membership)}
  → {state : Semantics.State (admittedSemantics membership)}
  → {left right : Semantics.Observation (admittedSemantics membership)}
  → Semantics.ObservationOf
      (admittedSemantics membership) external state left
  → Semantics.ObservationOf
      (admittedSemantics membership) external state right
  → left ≡ right
admitted-observation-deterministic
  membership {external} {state} {left} {right} left-path right-path =
  Semantics.observation-deterministic
    {design = admittedSemantics membership}
    {external = external}
    {state = state}
    {left = left}
    {right = right}
    left-path right-path

admitted-execution-final-unique :
  ∀ {design}
  → (membership : RestrictedCombinationalProfile design)
  → {state left right : Semantics.State (admittedSemantics membership)}
  → {samples :
      List
        (Semantics.Stimulus
          (Candidate.candidateInputCount
            (admittedCandidate membership)))}
  → Execution.Executes
      (admittedSemantics membership) state samples left
  → Execution.Executes
      (admittedSemantics membership) state samples right
  → left ≡ right
admitted-execution-final-unique
  membership {state} {left} {right} {samples}
  left-execution right-execution =
  Execution.execution-final-unique
    {design = admittedSemantics membership}
    {state = state}
    {left = left}
    {right = right}
    {samples = samples}
    left-execution right-execution