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

module Spartan6.Architecture.Profile where

open import Spartan6.Prelude
open import Spartan6.Evidence
open import Spartan6.Architecture.Primitive

record ArchitectureProfile : Type₀ where
  constructor architectureProfile
  field
    profileName                : String
    primitiveSupport          : PrimitiveKind → SupportStatus
    primitiveSemantics        : PrimitiveKind → SemanticStatus
    profileClockDomains       : ℕ
    profileAllowsBidirectional : Bool

open ArchitectureProfile public

developmentProfile : ArchitectureProfile
developmentProfile =
  architectureProfile
    "spartan6-level1-development"
    kindSupport
    kindSemantics
    1
    false

profileAdmits? : ArchitectureProfile → PrimitiveKind → Bool
profileAdmits? profile kind =
  fullySupported? (primitiveSupport profile kind)

profileExecutes? : ArchitectureProfile → PrimitiveKind → Bool
profileExecutes? profile kind =
  executable? (primitiveSemantics profile kind)

-- Typed evaluators exist for several partial modes, but the untrusted raw
-- boundary remains closed until decoding and normalisation obligations are
-- complete.

development-profile-is-closed : ∀ kind
  → profileAdmits? developmentProfile kind ≡ false
development-profile-is-closed LUT1 = refl
development-profile-is-closed LUT2 = refl
development-profile-is-closed LUT3 = refl
development-profile-is-closed LUT4 = refl
development-profile-is-closed LUT5 = refl
development-profile-is-closed LUT6 = refl
development-profile-is-closed MUXF7 = refl
development-profile-is-closed MUXF8 = refl
development-profile-is-closed CARRY4 = refl
development-profile-is-closed FDRE = refl
development-profile-is-closed FDSE = refl
development-profile-is-closed SRL16E = refl
development-profile-is-closed RAM64X1S = refl
development-profile-is-closed IBUF = refl
development-profile-is-closed OBUF = refl
development-profile-is-closed OBUFDS = refl
development-profile-is-closed OBUFT = refl
development-profile-is-closed BUFG = refl
development-profile-is-closed BUFGCE = refl

record DeviceProfile : Type₀ where
  constructor deviceProfile
  field
    deviceArchitecture : ArchitectureProfile
    devicePart         : String
    devicePackage      : String
    deviceRevision     : String
    applicableErrata   : List PinnedSource

open DeviceProfile public

-- The charter deliberately does not select a part/package yet.

selectedDeviceProfile : Maybe DeviceProfile
selectedDeviceProfile = nothing