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

module Spartan6.Validation.DecodedDesign where

open import Spartan6.Prelude

import Spartan6.Architecture.Primitive as Architecture
import Spartan6.Import.Artifact as Artifact
import Spartan6.Netlist.Provenance as Provenance
import Spartan6.Netlist.Raw as Raw
import Spartan6.Validation.Diagnostic as Diagnostic
import Spartan6.Validation.Parameter as Parameter
import Spartan6.Validation.Raw as Validation

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

record DecodedOccurrence
  (identifier : Provenance.OccurrenceId)
  (source : Raw.RawInstance) : Type₀ where
  field
    decodedKind : Architecture.PrimitiveKind
    kindAccepted :
      Raw.rawInstanceKind source ≡ Raw.knownPrimitive decodedKind
    decodedMode : Parameter.CoreParameters decodedKind
    modeAccepted :
      Parameter.normaliseCoreParameters decodedKind
        (Raw.rawInstanceName source)
        (Raw.rawInstanceParameters source)
        (Raw.rawInstanceInitialBit source)
      ≡ Diagnostic.accepted decodedMode
    canonicalPortsAccepted :
      Validation.orderedPortDiagnostics
        (Architecture.inputPortSpecifications decodedKind)
        (Architecture.outputPortSpecifications decodedKind)
        (Raw.rawInstancePorts source)
      ≡ []ᴸ

open DecodedOccurrence public

unknownOccurrence : Raw.RawInstance → Diagnostic.Diagnostics
unknownOccurrence source = Validation.instanceStructuralDiagnostics source

decodeKnownOccurrence :
  (identifier : Provenance.OccurrenceId)
  → (source : Raw.RawInstance)
  → (kind : Architecture.PrimitiveKind)
  → Raw.rawInstanceKind source ≡ Raw.knownPrimitive kind
  → Diagnostic.CheckResult (DecodedOccurrence identifier source)
decodeKnownOccurrence identifier source kind kind-path with
  Validation.orderedPortDiagnostics
    (Architecture.inputPortSpecifications kind)
    (Architecture.outputPortSpecifications kind)
    (Raw.rawInstancePorts source)
  | inspect
      (Validation.orderedPortDiagnostics
        (Architecture.inputPortSpecifications kind)
        (Architecture.outputPortSpecifications kind))
      (Raw.rawInstancePorts source)
... | problem ∷ᴸ problems | [ port-path ]ᵢ =
  Diagnostic.rejected (problem ∷ᴸ problems)
... | []ᴸ | [ port-path ]ᵢ with
  Parameter.normaliseCoreParameters kind
    (Raw.rawInstanceName source)
    (Raw.rawInstanceParameters source)
    (Raw.rawInstanceInitialBit source)
  | inspect
      (Parameter.normaliseCoreParameters kind
        (Raw.rawInstanceName source)
        (Raw.rawInstanceParameters source))
      (Raw.rawInstanceInitialBit source)
...   | Diagnostic.rejected diagnostics | [ mode-path ]ᵢ =
  Diagnostic.rejected diagnostics
...   | Diagnostic.accepted mode | [ mode-path ]ᵢ =
  Diagnostic.accepted record
    { decodedKind = kind
    ; kindAccepted = kind-path
    ; decodedMode = mode
    ; modeAccepted = mode-path
    ; canonicalPortsAccepted = port-path
    }

decodeOccurrence :
  (identifier : Provenance.OccurrenceId)
  → (source : Raw.RawInstance)
  → Diagnostic.CheckResult (DecodedOccurrence identifier source)
decodeOccurrence identifier source with Raw.rawInstanceKind source
  | inspect Raw.rawInstanceKind source
... | Raw.unknownPrimitive name | [ kind-path ]ᵢ =
  Diagnostic.rejected (unknownOccurrence source)
... | Raw.knownPrimitive kind | [ kind-path ]ᵢ =
  decodeKnownOccurrence identifier source kind kind-path

data DecodedOccurrences
  (next : ℕ) : List Raw.RawInstance → Type₀ where
  decodedDone : DecodedOccurrences next []ᴸ
  decodedNext : ∀ {source sources}
    → DecodedOccurrence (Provenance.occurrenceId next) source
    → DecodedOccurrences (suc next) sources
    → DecodedOccurrences next (source ∷ᴸ sources)

decodeOccurrences : (next : ℕ) → (sources : List Raw.RawInstance)
  → Diagnostic.CheckResult (DecodedOccurrences next sources)
decodeOccurrences next []ᴸ = Diagnostic.accepted decodedDone
decodeOccurrences next (source ∷ᴸ sources) with
  decodeOccurrence (Provenance.occurrenceId next) source
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted decoded with
  decodeOccurrences (suc next) sources
...   | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...   | Diagnostic.accepted rest =
  Diagnostic.accepted (decodedNext decoded rest)

record DecodedDesign (artifact : Artifact.RawArtifact) : Type₀ where
  constructor decodedDesign
  field
    decodedOccurrences :
      DecodedOccurrences 
        (Raw.rawInstances (Artifact.decodedDesign artifact))

open DecodedDesign public

decodeDesign : (artifact : Artifact.RawArtifact)
  → Diagnostic.CheckResult (DecodedDesign artifact)
decodeDesign artifact = Diagnostic.mapResult decodedDesign
  (decodeOccurrences 
    (Raw.rawInstances (Artifact.decodedDesign artifact)))