SemanticExplanation.Macro

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

module SemanticExplanation.Macro where

open import SemanticExplanation.Base
open import SemanticExplanation.Discourse
open import SemanticExplanation.Domain
open import SemanticExplanation.Realise
open import SemanticExplanation.Translate hiding (_>>=_)
open import Agda.Builtin.Reflection

infixl 1 _>>=_

_>>=_ : ∀ {a b} {A : Set a} {B : Set b} → TC A → (A → TC B) → TC B
_>>=_ = bindTC

defaultFuel : Nat
defaultFuel = 256

failureParts : Name → TranslationFailure → List ErrorPart
failureParts declaration problem =
  strErr "semantic explanation failed for "
  ∷ nameErr declaration
  ∷ strErr "; structured failure tag is available through failureTagForName"
  ∷ []

explainNameWithFuelTC : Nat → DomainSpec → Name → Term → TC ⊤
explainNameWithFuelTC fuel spec declaration hole =
  withReconstructed true (getType declaration) >>= λ declaredType →
  noConstraints (translateClosed fuel spec declaredType) >>= λ where
    (failure problem) → typeError (failureParts declaration problem)
    (success result) → quoteTC (canonicalRealise spec result) >>= unify hole

explainNameTC : DomainSpec → Name → Term → TC ⊤
explainNameTC spec declaration hole =
  explainNameWithFuelTC (DomainSpec.reductionFuel spec) spec declaration hole

explainNameCompactTC : DomainSpec → Name → Term → TC ⊤
explainNameCompactTC spec declaration hole =
  withReconstructed true (getType declaration) >>= λ declaredType →
  noConstraints (translateClosed (DomainSpec.reductionFuel spec) spec declaredType) >>= λ where
    (failure problem) → typeError (failureParts declaration problem)
    (success result) → quoteTC (compactRealise spec result) >>= unify hole

explainNameFamilyTC : DomainSpec → Name → Term → TC ⊤
explainNameFamilyTC spec declaration hole =
  withReconstructed true (getType declaration) >>= λ declaredType →
  noConstraints (translateClosed (DomainSpec.reductionFuel spec) spec declaredType) >>= λ where
    (failure problem) → typeError (failureParts declaration problem)
    (success result) → quoteTC (realisationFamily spec result) >>= unify hole

unknownCandidateParts : String → Name → List ErrorPart
unknownCandidateParts candidateId declaration =
  strErr "semantic explanation candidate ID "
  ∷ strErr candidateId
  ∷ strErr " is not available for "
  ∷ nameErr declaration
  ∷ strErr "; allowed IDs are canonical/v1, compact/v1, evidence/v1, structured/v1"
  ∷ []

emitSelected : String → Name → Term → Maybe Explanation → TC ⊤
emitSelected candidateId declaration hole nothing =
  typeError (unknownCandidateParts candidateId declaration)
emitSelected candidateId declaration hole (just candidate) =
  quoteTC candidate >>= unify hole

explainNameSelectedTC : DomainSpec → String → Name → Term → TC ⊤
explainNameSelectedTC spec candidateId declaration hole =
  withReconstructed true (getType declaration) >>= λ declaredType →
  noConstraints (translateClosed (DomainSpec.reductionFuel spec) spec declaredType) >>= λ where
    (failure problem) → typeError (failureParts declaration problem)
    (success result) → emitSelected candidateId declaration hole
      (selectCandidateById candidateId (realisationFamily spec result))

unknownDomainCandidateParts : String → Name → List ErrorPart
unknownDomainCandidateParts candidateId declaration =
  strErr "semantic explanation candidate ID "
  ∷ strErr candidateId
  ∷ strErr " is not available for "
  ∷ nameErr declaration
  ∷ strErr "; allowed IDs are canonical/v1, compact/v1, evidence/v1, structured/v1, domain-evidence/v1"
  ∷ []

emitDomainSelected : String → Name → Term → Maybe Explanation → TC ⊤
emitDomainSelected candidateId declaration hole nothing =
  typeError (unknownDomainCandidateParts candidateId declaration)
emitDomainSelected candidateId declaration hole (just candidate) =
  quoteTC candidate >>= unify hole

explainNameDomainEvidenceTC
  : DiscourseProfile → DomainSpec → Name → Term → TC ⊤
explainNameDomainEvidenceTC profile spec declaration hole =
  withReconstructed true (getType declaration) >>= λ declaredType →
  noConstraints (translateClosed (DomainSpec.reductionFuel spec) spec declaredType) >>= λ where
    (failure problem) → typeError (failureParts declaration problem)
    (success result) →
      quoteTC (domainEvidenceRealise profile spec result) >>= unify hole

explainNameDomainFamilyTC
  : DiscourseProfile → DomainSpec → Name → Term → TC ⊤
explainNameDomainFamilyTC profile spec declaration hole =
  withReconstructed true (getType declaration) >>= λ declaredType →
  noConstraints (translateClosed (DomainSpec.reductionFuel spec) spec declaredType) >>= λ where
    (failure problem) → typeError (failureParts declaration problem)
    (success result) →
      quoteTC (domainRealisationFamily profile spec result) >>= unify hole

explainNameDomainSelectedTC
  : DiscourseProfile → DomainSpec → String → Name → Term → TC ⊤
explainNameDomainSelectedTC profile spec candidateId declaration hole =
  withReconstructed true (getType declaration) >>= λ declaredType →
  noConstraints (translateClosed (DomainSpec.reductionFuel spec) spec declaredType) >>= λ where
    (failure problem) → typeError (failureParts declaration problem)
    (success result) → emitDomainSelected candidateId declaration hole
      (selectCandidateById candidateId
        (domainRealisationFamily profile spec result))

failureTagForNameWithFuelTC : Nat → DomainSpec → Name → Term → TC ⊤
failureTagForNameWithFuelTC fuel spec declaration hole =
  withReconstructed true (getType declaration) >>= λ declaredType →
  noConstraints (translateClosed fuel spec declaredType) >>= λ where
    (success result) →
      typeError (strErr "expected structured translation failure, but translation succeeded" ∷ [])
    (failure problem) → quoteTC (TranslationFailure.tag problem) >>= unify hole

failureTagForNameTC : DomainSpec → Name → Term → TC ⊤
failureTagForNameTC spec declaration hole =
  failureTagForNameWithFuelTC
    (DomainSpec.reductionFuel spec) spec declaration hole

macro
  explainNameWithFuel : Nat → DomainSpec → Name → Term → TC ⊤
  explainNameWithFuel = explainNameWithFuelTC

  explainName : DomainSpec → Name → Term → TC ⊤
  explainName = explainNameTC

  explainNameCompact : DomainSpec → Name → Term → TC ⊤
  explainNameCompact = explainNameCompactTC

  explainNameFamily : DomainSpec → Name → Term → TC ⊤
  explainNameFamily = explainNameFamilyTC

  explainNameSelected : DomainSpec → String → Name → Term → TC ⊤
  explainNameSelected = explainNameSelectedTC

  explainNameDomainEvidence
    : DiscourseProfile → DomainSpec → Name → Term → TC ⊤
  explainNameDomainEvidence = explainNameDomainEvidenceTC

  explainNameDomainFamily
    : DiscourseProfile → DomainSpec → Name → Term → TC ⊤
  explainNameDomainFamily = explainNameDomainFamilyTC

  explainNameDomainSelected
    : DiscourseProfile → DomainSpec → String → Name → Term → TC ⊤
  explainNameDomainSelected = explainNameDomainSelectedTC

  failureTagForNameWithFuel : Nat → DomainSpec → Name → Term → TC ⊤
  failureTagForNameWithFuel = failureTagForNameWithFuelTC

  failureTagForName : DomainSpec → Name → Term → TC ⊤
  failureTagForName = failureTagForNameTC