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

module Spartan6.Evidence where

open import Spartan6.Prelude

-- How a claim about the architecture is justified.

data EvidenceClass : Type₀ where
  officialErratum       : EvidenceClass
  officialDocumentation : EvidenceClass
  vendorToolOutput      : EvidenceClass
  reverseEngineered     : EvidenceClass
  experimentBacked      : EvidenceClass
  inferred              : EvidenceClass
  assumed               : EvidenceClass
  unsupportedEvidence   : EvidenceClass

official? : EvidenceClass → Bool
official? officialErratum        = true
official? officialDocumentation  = true
official? vendorToolOutput       = false
official? reverseEngineered      = false
official? experimentBacked       = false
official? inferred               = false
official? assumed                = false
official? unsupportedEvidence    = false

-- Coverage of a primitive, mode, parameter set, or exceptional case.

data SupportStatus : Type₀ where
  fullySupported         : SupportStatus
  conditionallySupported : SupportStatus
  partiallySupported     : SupportStatus
  assumptionSupported    : SupportStatus
  unsupportedFeature     : SupportStatus
  planned                : SupportStatus

fullySupported? : SupportStatus → Bool
fullySupported? fullySupported          = true
fullySupported? conditionallySupported  = false
fullySupported? partiallySupported      = false
fullySupported? assumptionSupported     = false
fullySupported? unsupportedFeature      = false
fullySupported? planned                 = false

-- Whether a rule gives executable behaviour, requires a precondition, or
-- deliberately declines to assign behaviour.

data SemanticStatus : Type₀ where
  guaranteed              : SemanticStatus
  guaranteedConditionally : SemanticStatus
  documentedUnspecified   : SemanticStatus
  insufficientEvidence    : SemanticStatus
  unsupportedSemantics    : SemanticStatus

executable? : SemanticStatus → Bool
executable? guaranteed               = true
executable? guaranteedConditionally  = true
executable? documentedUnspecified    = false
executable? insufficientEvidence     = false
executable? unsupportedSemantics     = false

-- Public documents named by the project scope.  A SourceIdentifier is not a
-- citation on its own: PinnedSource additionally requires an explicit
-- revision label.

data SourceIdentifier : Type₀ where
  UG615     : SourceIdentifier
  UG384     : SourceIdentifier
  UG383     : SourceIdentifier
  XCN11014  : SourceIdentifier
  UG389     : SourceIdentifier
  UG380     : SourceIdentifier
  UG382     : SourceIdentifier
  EN148     : SourceIdentifier
  UG381     : SourceIdentifier
  DS160     : SourceIdentifier

sourceCode : SourceIdentifier → String
sourceCode UG615     = "UG615"
sourceCode UG384     = "UG384"
sourceCode UG383     = "UG383"
sourceCode XCN11014  = "XCN11014"
sourceCode UG389     = "UG389"
sourceCode UG380     = "UG380"
sourceCode UG382     = "UG382"
sourceCode EN148     = "EN148"
sourceCode UG381     = "UG381"
sourceCode DS160     = "DS160"

record SourceRevision : Type₀ where
  constructor revision
  field
    label         : String
    publicationDate : Maybe String

open SourceRevision public

record PinnedSource : Type₀ where
  constructor pinSource
  field
    identifier : SourceIdentifier
    pinnedRevision : SourceRevision

open PinnedSource public

record SourceLocator : Type₀ where
  constructor locate
  field
    source   : PinnedSource
    section  : String
    detail   : String

open SourceLocator public

-- sourceLocator is optional because assumptions, unsupported features, and
-- unresolved documentary gaps need traceability entries even when no source
-- can yet be cited.

record RuleTraceability : Type₀ where
  constructor traceRule
  field
    ruleId          : String
    evidenceClass   : EvidenceClass
    sourceLocator   : Maybe SourceLocator
    supportStatus   : SupportStatus
    semanticStatus  : SemanticStatus
    note            : String

open RuleTraceability public

traceOfficial? : RuleTraceability → Bool
traceOfficial? trace = official? (evidenceClass trace)

traceExecutable? : RuleTraceability → Bool
traceExecutable? trace = executable? (semanticStatus trace)

traceFullySupported? : RuleTraceability → Bool
traceFullySupported? trace = fullySupported? (supportStatus trace)

officialErratum-is-official : official? officialErratum ≡ true
officialErratum-is-official = refl

officialDocumentation-is-official :
  official? officialDocumentation ≡ true
officialDocumentation-is-official = refl

assumption-is-not-official : official? assumed ≡ false
assumption-is-not-official = refl

guaranteed-is-executable : executable? guaranteed ≡ true
guaranteed-is-executable = refl

unspecified-is-not-executable : executable? documentedUnspecified ≡ false
unspecified-is-not-executable = refl

fullySupported-is-full : fullySupported? fullySupported ≡ true
fullySupported-is-full = refl

UG615-source-code : sourceCode UG615 ≡ "UG615"
UG615-source-code = refl