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

module SemanticExplanation.Realise where

open import SemanticExplanation.Base
open import SemanticExplanation.Discourse
open import SemanticExplanation.Domain
open import SemanticExplanation.IR

record Explanation : Set where
  constructor explanation
  field
    text : String
    candidateId : String
    domainId : String
    provenance : List ProvenanceEntry

record CandidateSet : Set where
  constructor candidate-set
  field
    familyId : String
    candidates : List Explanation

renderExpr : ∀ {scope} → List String → ExprIR scope → String
renderExpr names (bound index) with lookupFin names index
... | just name = name
... | nothing = "<scope-error>"
renderExpr names (application rule (constantWord word) []) = word
renderExpr names (application rule (unaryForm before after) (x ∷ [])) =
  before ++ renderExpr names x ++ after
renderExpr names (application rule (binaryForm before between after) (x ∷ y ∷ [])) =
  before ++ renderExpr names x ++ between ++ renderExpr names y ++ after
renderExpr names (application rule surface args) = "<invalid-expression-realisation>"

renderAtom : ∀ {scope} → List String → AtomSurface → List (ExprIR scope) → String
renderAtom names (unarySuffix phrase) (x ∷ []) =
  renderExpr names x ++ " " ++ phrase
renderAtom names (binaryVerb phrase) (x ∷ y ∷ []) =
  renderExpr names x ++ " " ++ phrase ++ " " ++ renderExpr names y
renderAtom names (equalityPhrase phrase) (x ∷ y ∷ []) =
  renderExpr names x ++ " " ++ phrase ++ " " ++ renderExpr names y
renderAtom names surface args = "<invalid-atom-realisation>"

renderIndices : ∀ {scope} → List String → List (ExprIR scope) → String
renderIndices names [] = ""
renderIndices names (index ∷ []) = renderExpr names index
renderIndices names (index ∷ indices) =
  renderExpr names index ++ ", " ++ renderIndices names indices

snoc : ∀ {a} {A : Set a} → List A → A → List A
snoc [] y = y ∷ []
snoc (x ∷ xs) y = x ∷ snoc xs y

joinAnd : List String → String
joinAnd [] = ""
joinAnd (x ∷ []) = x
joinAnd (x ∷ y ∷ []) = x ++ " and " ++ y
joinAnd (x ∷ xs) = x ++ ", " ++ joinAndLast xs
  where
  joinAndLast : List String → String
  joinAndLast [] = ""
  joinAndLast (z ∷ []) = "and " ++ z
  joinAndLast (z ∷ zs) = z ++ ", " ++ joinAndLast zs

joinSemicolon : List String → String
joinSemicolon [] = ""
joinSemicolon (x ∷ []) = x
joinSemicolon (x ∷ y ∷ []) = x ++ "; and " ++ y
joinSemicolon (x ∷ xs) = x ++ "; " ++ joinSemicolonLast xs
  where
  joinSemicolonLast : List String → String
  joinSemicolonLast [] = ""
  joinSemicolonLast (z ∷ []) = "and " ++ z
  joinSemicolonLast (z ∷ zs) = z ++ "; " ++ joinSemicolonLast zs

propRuleId : ∀ {scope} → PropIR scope → Maybe String
propRuleId (atom rule _ _) = just rule
propRuleId (equal rule _ _ _) = just rule
propRuleId (imply _ _) = nothing
propRuleId (forallP _ _) = nothing

labelForProp
  : ∀ {scope} → DiscourseProfile → String → PropIR scope → String
labelForProp profile fallback proposition with propRuleId proposition
... | nothing = fallback
... | just ruleId
  with findStatementLabel ruleId (DiscourseProfile.statementLabels profile)
... | nothing = fallback
... | just label = label

binderRuleOccurs : ∀ {scope} → String → PropIR scope → Bool
binderRuleOccurs ruleId (atom _ _ _) = false
binderRuleOccurs ruleId (equal _ _ _ _) = false
binderRuleOccurs ruleId (imply premise conclusion)
  with binderRuleOccurs ruleId premise
... | true = true
... | false = binderRuleOccurs ruleId conclusion
binderRuleOccurs ruleId (forallP boundEntity body)
  with ruleId ==S Binder.ruleId boundEntity
... | true = true
... | false = binderRuleOccurs ruleId body

record BinderRealisation : Set where
  constructor binder-realisation
  field
    introduction : String
    reference : String

realiseDomainBinder
  : ∀ {scope} → DiscourseProfile → List String → List String
  → PropIR (suc scope) → Binder scope → BinderRealisation
realiseDomainBinder profile names usedRuleIds body boundEntity
  with findEntityReferent (Binder.ruleId boundEntity)
         (DiscourseProfile.entityReferents profile)
     | memberString (Binder.ruleId boundEntity) usedRuleIds
     | binderRuleOccurs (Binder.ruleId boundEntity) body
... | just reference | false | false =
  binder-realisation (Binder.entityWord boundEntity) reference
... | referent | used | repeated =
  binder-realisation
    (Binder.entityWord boundEntity ++ " " ++ chosen)
    chosen
  where
  chosen : String
  chosen = freshHint (Binder.hint boundEntity) names

renderForallItems : List String → String
renderForallItems [] = ""
renderForallItems (x ∷ []) = "every " ++ x
renderForallItems (x ∷ y ∷ []) = "every " ++ x ++ " and every " ++ y
renderForallItems (x ∷ xs) = "every " ++ x ++ ", " ++ renderForallLast xs
  where
  renderForallLast : List String → String
  renderForallLast [] = ""
  renderForallLast (z ∷ []) = "and every " ++ z
  renderForallLast (z ∷ zs) = "every " ++ z ++ ", " ++ renderForallLast zs

renderProp : ∀ {scope} → List String → Bool → PropIR scope → String
renderProp names initial (atom rule surface args) = renderAtom names surface args
renderProp names initial (equal rule phrase left right) =
  renderExpr names left ++ " " ++ phrase ++ " " ++ renderExpr names right
renderProp names initial (imply premise conclusion) =
  (if initial then "If " else "if ")
  ++ renderProp names false premise
  ++ ", then "
  ++ renderProp names false conclusion
renderProp names initial (forallP boundEntity body) =
  (if initial then "For every " else "for every ")
  ++ Binder.entityWord boundEntity
  ++ " "
  ++ chosen
  ++ indexText
  ++ ", "
  ++ renderProp (chosen ∷ names) false body
  where
  chosen : String
  chosen = freshHint (Binder.hint boundEntity) names

  indexText : String
  indexText with Binder.indices boundEntity
  ... | [] = ""
  ... | indices = " indexed by " ++ renderIndices names indices

mutual
  renderCompactProp : ∀ {scope} → List String → Bool → PropIR scope → String
  renderCompactProp names initial (forallP boundEntity body) =
    renderCompactForalls (chosen ∷ names) initial
      ((Binder.entityWord boundEntity ++ " " ++ chosen ++ indexText) ∷ []) body
    where
    chosen : String
    chosen = freshHint (Binder.hint boundEntity) names

    indexText : String
    indexText with Binder.indices boundEntity
    ... | [] = ""
    ... | indices = " indexed by " ++ renderIndices names indices
  renderCompactProp names initial (imply premise conclusion) =
    renderCompactImplications names initial
      (renderCompactProp names false premise ∷ []) conclusion
  renderCompactProp names initial (atom rule surface args) =
    renderAtom names surface args
  renderCompactProp names initial (equal rule phrase left right) =
    renderExpr names left ++ " " ++ phrase ++ " " ++ renderExpr names right

  renderCompactForalls
    : ∀ {scope} → List String → Bool → List String → PropIR scope → String
  renderCompactForalls names initial items (forallP boundEntity body) =
    renderCompactForalls (chosen ∷ names) initial
      (snoc items (Binder.entityWord boundEntity ++ " " ++ chosen ++ indexText)) body
    where
    chosen : String
    chosen = freshHint (Binder.hint boundEntity) names

    indexText : String
    indexText with Binder.indices boundEntity
    ... | [] = ""
    ... | indices = " indexed by " ++ renderIndices names indices
  renderCompactForalls names initial items (imply premise conclusion) =
    (if initial then "For " else "for ")
    ++ renderForallItems items
    ++ ", "
    ++ renderCompactImplications names false
         (renderCompactProp names false premise ∷ []) conclusion
  renderCompactForalls names initial items (atom rule surface args) =
    (if initial then "For " else "for ")
    ++ renderForallItems items
    ++ ", "
    ++ renderAtom names surface args
  renderCompactForalls names initial items (equal rule phrase left right) =
    (if initial then "For " else "for ")
    ++ renderForallItems items
    ++ ", "
    ++ renderExpr names left ++ " " ++ phrase ++ " " ++ renderExpr names right

  renderCompactImplications
    : ∀ {scope} → List String → Bool → List String → PropIR scope → String
  renderCompactImplications names initial premises (imply premise conclusion) =
    renderCompactImplications names initial
      (snoc premises (renderCompactProp names false premise)) conclusion
  renderCompactImplications names initial premises (forallP boundEntity body) =
    (if initial then "If " else "if ")
    ++ joinAnd premises
    ++ ", then "
    ++ renderCompactForalls (chosen ∷ names) false
         ((Binder.entityWord boundEntity ++ " " ++ chosen ++ indexText) ∷ []) body
    where
    chosen : String
    chosen = freshHint (Binder.hint boundEntity) names

    indexText : String
    indexText with Binder.indices boundEntity
    ... | [] = ""
    ... | indices = " indexed by " ++ renderIndices names indices
  renderCompactImplications names initial premises (atom rule surface args) =
    (if initial then "If " else "if ")
    ++ joinAnd premises
    ++ ", then "
    ++ renderAtom names surface args
  renderCompactImplications names initial premises (equal rule phrase left right) =
    (if initial then "If " else "if ")
    ++ joinAnd premises
    ++ ", then "
    ++ renderExpr names left ++ " " ++ phrase ++ " " ++ renderExpr names right

mutual
  renderEvidenceProp : ∀ {scope} → List String → Bool → PropIR scope → String
  renderEvidenceProp names initial (forallP boundEntity body) =
    renderEvidenceForalls (chosen ∷ names) initial
      ((Binder.entityWord boundEntity ++ " " ++ chosen ++ indexText) ∷ []) body
    where
    chosen : String
    chosen = freshHint (Binder.hint boundEntity) names

    indexText : String
    indexText with Binder.indices boundEntity
    ... | [] = ""
    ... | indices = " indexed by " ++ renderIndices names indices
  renderEvidenceProp names initial (imply premise conclusion) =
    renderEvidenceImplications names initial
      (renderCompactProp names false premise ∷ []) conclusion
  renderEvidenceProp names initial (atom rule surface args) =
    renderAtom names surface args
  renderEvidenceProp names initial (equal rule phrase left right) =
    renderExpr names left ++ " " ++ phrase ++ " " ++ renderExpr names right

  renderEvidenceForalls
    : ∀ {scope} → List String → Bool → List String → PropIR scope → String
  renderEvidenceForalls names initial items (forallP boundEntity body) =
    renderEvidenceForalls (chosen ∷ names) initial
      (snoc items (Binder.entityWord boundEntity ++ " " ++ chosen ++ indexText)) body
    where
    chosen : String
    chosen = freshHint (Binder.hint boundEntity) names

    indexText : String
    indexText with Binder.indices boundEntity
    ... | [] = ""
    ... | indices = " indexed by " ++ renderIndices names indices
  renderEvidenceForalls names initial items (imply premise conclusion) =
    (if initial then "For " else "for ")
    ++ renderForallItems items
    ++ ", "
    ++ renderEvidenceImplications names false
         (renderCompactProp names false premise ∷ []) conclusion
  renderEvidenceForalls names initial items (atom rule surface args) =
    (if initial then "For " else "for ")
    ++ renderForallItems items
    ++ ", "
    ++ renderAtom names surface args
  renderEvidenceForalls names initial items (equal rule phrase left right) =
    (if initial then "For " else "for ")
    ++ renderForallItems items
    ++ ", "
    ++ renderExpr names left ++ " " ++ phrase ++ " " ++ renderExpr names right

  renderEvidenceImplications
    : ∀ {scope} → List String → Bool → List String → PropIR scope → String
  renderEvidenceImplications names initial premises (imply premise conclusion) =
    renderEvidenceImplications names initial
      (snoc premises (renderCompactProp names false premise)) conclusion
  renderEvidenceImplications names initial premises (forallP boundEntity body) =
    (if initial then "Given " else "given ")
    ++ joinSemicolon premises
    ++ ", "
    ++ renderEvidenceForalls (chosen ∷ names) false
         ((Binder.entityWord boundEntity ++ " " ++ chosen ++ indexText) ∷ []) body
    where
    chosen : String
    chosen = freshHint (Binder.hint boundEntity) names

    indexText : String
    indexText with Binder.indices boundEntity
    ... | [] = ""
    ... | indices = " indexed by " ++ renderIndices names indices
  renderEvidenceImplications names initial premises (atom rule surface args) =
    (if initial then "Given " else "given ")
    ++ joinSemicolon premises
    ++ ", "
    ++ renderAtom names surface args
  renderEvidenceImplications names initial premises (equal rule phrase left right) =
    (if initial then "Given " else "given ")
    ++ joinSemicolon premises
    ++ ", "
    ++ renderExpr names left ++ " " ++ phrase ++ " " ++ renderExpr names right

mutual
  renderStructuredProp : ∀ {scope} → List String → Bool → PropIR scope → String
  renderStructuredProp names initial (forallP boundEntity body) =
    renderStructuredForalls (chosen ∷ names) initial
      ((Binder.entityWord boundEntity ++ " " ++ chosen ++ indexText) ∷ []) body
    where
    chosen : String
    chosen = freshHint (Binder.hint boundEntity) names

    indexText : String
    indexText with Binder.indices boundEntity
    ... | [] = ""
    ... | indices = " indexed by " ++ renderIndices names indices
  renderStructuredProp names initial (imply premise conclusion) =
    renderStructuredImplications names initial
      (renderCompactProp names false premise ∷ []) conclusion
  renderStructuredProp names initial (atom rule surface args) =
    renderAtom names surface args
  renderStructuredProp names initial (equal rule phrase left right) =
    renderExpr names left ++ " " ++ phrase ++ " " ++ renderExpr names right

  renderStructuredForalls
    : ∀ {scope} → List String → Bool → List String → PropIR scope → String
  renderStructuredForalls names initial items (forallP boundEntity body) =
    renderStructuredForalls (chosen ∷ names) initial
      (snoc items (Binder.entityWord boundEntity ++ " " ++ chosen ++ indexText)) body
    where
    chosen : String
    chosen = freshHint (Binder.hint boundEntity) names

    indexText : String
    indexText with Binder.indices boundEntity
    ... | [] = ""
    ... | indices = " indexed by " ++ renderIndices names indices
  renderStructuredForalls names initial items (imply premise conclusion) =
    (if initial then "For " else "for ")
    ++ renderForallItems items
    ++ ", the following conditions suffice: "
    ++ renderStructuredImplications names false
         (renderCompactProp names false premise ∷ []) conclusion
  renderStructuredForalls names initial items (atom rule surface args) =
    (if initial then "For " else "for ")
    ++ renderForallItems items
    ++ ", "
    ++ renderAtom names surface args
  renderStructuredForalls names initial items (equal rule phrase left right) =
    (if initial then "For " else "for ")
    ++ renderForallItems items
    ++ ", "
    ++ renderExpr names left ++ " " ++ phrase ++ " " ++ renderExpr names right

  renderStructuredImplications
    : ∀ {scope} → List String → Bool → List String → PropIR scope → String
  renderStructuredImplications names initial premises (imply premise conclusion) =
    renderStructuredImplications names initial
      (snoc premises (renderCompactProp names false premise)) conclusion
  renderStructuredImplications names initial premises (forallP boundEntity body) =
    joinSemicolon premises
    ++ ". Under those conditions, "
    ++ renderStructuredForalls (chosen ∷ names) false
         ((Binder.entityWord boundEntity ++ " " ++ chosen ++ indexText) ∷ []) body
    where
    chosen : String
    chosen = freshHint (Binder.hint boundEntity) names

    indexText : String
    indexText with Binder.indices boundEntity
    ... | [] = ""
    ... | indices = " indexed by " ++ renderIndices names indices
  renderStructuredImplications names initial premises (atom rule surface args) =
    (if initial then "The following conditions suffice: " else "")
    ++ joinSemicolon premises
    ++ ". Under those conditions, "
    ++ renderAtom names surface args
  renderStructuredImplications names initial premises (equal rule phrase left right) =
    (if initial then "The following conditions suffice: " else "")
    ++ joinSemicolon premises
    ++ ". Under those conditions, "
    ++ renderExpr names left ++ " " ++ phrase ++ " " ++ renderExpr names right

renderLabeledPremise
  : ∀ {scope} → DiscourseProfile → List String → PropIR scope → String
renderLabeledPremise profile names premise =
  labelForProp profile (DiscourseProfile.fallbackPremiseLabel profile) premise
  ++ " — "
  ++ renderCompactProp names false premise

renderLabeledPremises
  : ∀ {scope} → DiscourseProfile → List String → List (PropIR scope) → List String
renderLabeledPremises profile names [] = []
renderLabeledPremises profile names (premise ∷ premises) =
  renderLabeledPremise profile names premise
  ∷ renderLabeledPremises profile names premises

mutual
  renderDomainEvidenceProp
    : ∀ {scope} → DiscourseProfile → List String → Bool → PropIR scope → String
  renderDomainEvidenceProp profile names initial (forallP boundEntity body) =
    renderDomainEvidenceForalls profile
      (BinderRealisation.reference words ∷ names)
      (Binder.ruleId boundEntity ∷ []) initial
      ((BinderRealisation.introduction words ++ indexText) ∷ []) body
    where
    words : BinderRealisation
    words = realiseDomainBinder profile names [] body boundEntity

    indexText : String
    indexText with Binder.indices boundEntity
    ... | [] = ""
    ... | indices = " indexed by " ++ renderIndices names indices
  renderDomainEvidenceProp profile names initial (imply premise conclusion) =
    renderDomainEvidenceImplications profile names initial
      (premise ∷ []) conclusion
  renderDomainEvidenceProp profile names initial proposition =
    labelForProp profile
      (DiscourseProfile.fallbackConclusionLabel profile) proposition
    ++ " — "
    ++ renderCompactProp names false proposition

  renderDomainEvidenceForalls
    : ∀ {scope} → DiscourseProfile → List String → List String → Bool
    → List String → PropIR scope → String
  renderDomainEvidenceForalls profile names usedRuleIds initial items
    (forallP boundEntity body) =
    renderDomainEvidenceForalls profile
      (BinderRealisation.reference words ∷ names)
      (Binder.ruleId boundEntity ∷ usedRuleIds) initial
      (snoc items (BinderRealisation.introduction words ++ indexText)) body
    where
    words : BinderRealisation
    words = realiseDomainBinder profile names usedRuleIds body boundEntity

    indexText : String
    indexText with Binder.indices boundEntity
    ... | [] = ""
    ... | indices = " indexed by " ++ renderIndices names indices
  renderDomainEvidenceForalls profile names usedRuleIds initial items body =
    (if initial then "For " else "for ")
    ++ renderForallItems items
    ++ ", "
    ++ renderDomainEvidenceBody profile names body

  renderDomainEvidenceBody
    : ∀ {scope} → DiscourseProfile → List String → PropIR scope → String
  renderDomainEvidenceBody profile names (imply premise conclusion) =
    renderDomainEvidenceImplications profile names false
      (premise ∷ []) conclusion
  renderDomainEvidenceBody profile names proposition =
    labelForProp profile
      (DiscourseProfile.fallbackConclusionLabel profile) proposition
    ++ " — "
    ++ renderCompactProp names false proposition

  renderDomainEvidenceImplications
    : ∀ {scope} → DiscourseProfile → List String → Bool
    → List (PropIR scope) → PropIR scope → String
  renderDomainEvidenceImplications profile names initial premises
    (imply premise conclusion) =
    renderDomainEvidenceImplications profile names initial
      (snoc premises premise) conclusion
  renderDomainEvidenceImplications profile names initial premises conclusion =
    (if initial then "The " else "the ")
    ++ DiscourseProfile.basisNoun profile
    ++ " in declaration order is: "
    ++ joinSemicolon (renderLabeledPremises profile names premises)
    ++ ". "
    ++ labelForProp profile
         (DiscourseProfile.fallbackConclusionLabel profile) conclusion
    ++ " — "
    ++ renderCompactProp names false conclusion

canonicalRealise : DomainSpec → Translation zero → Explanation
canonicalRealise spec result =
  explanation
    (renderProp [] true (Translation.proposition result) ++ ".")
    "canonical/v1"
    (DomainSpec.domainId spec)
    (Translation.provenance result)

compactRealise : DomainSpec → Translation zero → Explanation
compactRealise spec result =
  explanation
    (renderCompactProp [] true (Translation.proposition result) ++ ".")
    "compact/v1"
    (DomainSpec.domainId spec)
    (Translation.provenance result)

evidenceRealise : DomainSpec → Translation zero → Explanation
evidenceRealise spec result =
  explanation
    (renderEvidenceProp [] true (Translation.proposition result) ++ ".")
    "evidence/v1"
    (DomainSpec.domainId spec)
    (Translation.provenance result)

structuredRealise : DomainSpec → Translation zero → Explanation
structuredRealise spec result =
  explanation
    (renderStructuredProp [] true (Translation.proposition result) ++ ".")
    "structured/v1"
    (DomainSpec.domainId spec)
    (Translation.provenance result)

domainEvidenceRealise
  : DiscourseProfile → DomainSpec → Translation zero → Explanation
domainEvidenceRealise profile spec result =
  explanation
    (renderDomainEvidenceProp profile [] true
      (Translation.proposition result) ++ ".")
    "domain-evidence/v1"
    (DomainSpec.domainId spec)
    (Translation.provenance result)

realisationFamily : DomainSpec → Translation zero → List Explanation
realisationFamily spec result =
  canonicalRealise spec result
  ∷ compactRealise spec result
  ∷ evidenceRealise spec result
  ∷ structuredRealise spec result
  ∷ []

realisationSet : DomainSpec → Translation zero → CandidateSet
realisationSet spec result =
  candidate-set "core-proposition/v2" (realisationFamily spec result)

domainRealisationFamily
  : DiscourseProfile → DomainSpec → Translation zero → List Explanation
domainRealisationFamily profile spec result =
  canonicalRealise spec result
  ∷ compactRealise spec result
  ∷ evidenceRealise spec result
  ∷ structuredRealise spec result
  ∷ domainEvidenceRealise profile spec result
  ∷ []

domainRealisationSet
  : DiscourseProfile → DomainSpec → Translation zero → CandidateSet
domainRealisationSet profile spec result =
  candidate-set
    ("domain-proposition/" ++ DiscourseProfile.profileId profile ++ "/v1")
    (domainRealisationFamily profile spec result)

candidateIds : List Explanation → List String
candidateIds [] = []
candidateIds (candidate ∷ candidates) =
  Explanation.candidateId candidate ∷ candidateIds candidates

selectCandidateById : String → List Explanation → Maybe Explanation
selectCandidateById candidateId [] = nothing
selectCandidateById candidateId (candidate ∷ candidates)
  with candidateId ==S Explanation.candidateId candidate
... | true = just candidate
... | false = selectCandidateById candidateId candidates