{-# OPTIONS --safe --cubical-compatible --no-sized-types --no-guardedness #-}

module SemanticExplanation.Discourse where

open import SemanticExplanation.Base

-- Realisation metadata is keyed by the stable rule identifier already carried
-- by semantic IR.  Quoted Names remain the dispatch key when source terms are
-- translated; this layer only chooses audited wording after interpretation.
record StatementLabel : Set where
  constructor statement-label
  field
    ruleId : String
    label : String

record EntityReferent : Set where
  constructor entity-referent
  field
    entityRuleId : String
    reference : String

record DiscourseProfile : Set where
  constructor discourse-profile
  field
    profileId : String
    basisNoun : String
    fallbackPremiseLabel : String
    fallbackConclusionLabel : String
    statementLabels : List StatementLabel
    entityReferents : List EntityReferent

findStatementLabel : String → List StatementLabel → Maybe String
findStatementLabel ruleId [] = nothing
findStatementLabel ruleId (candidate ∷ candidates)
  with ruleId ==S StatementLabel.ruleId candidate
... | true = just (StatementLabel.label candidate)
... | false = findStatementLabel ruleId candidates

findEntityReferent : String → List EntityReferent → Maybe String
findEntityReferent ruleId [] = nothing
findEntityReferent ruleId (candidate ∷ candidates)
  with ruleId ==S EntityReferent.entityRuleId candidate
... | true = just (EntityReferent.reference candidate)
... | false = findEntityReferent ruleId candidates