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

module SemanticExplanation.Translate where

open import SemanticExplanation.Base
open import SemanticExplanation.Domain
open import SemanticExplanation.IR
open import SemanticExplanation.Reflection.Reduce
open import SemanticExplanation.Reflection.View
import Agda.Builtin.Reflection as R

infixl  _>>=_

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

data Phase : Set where
  reduction classification interpretation : Phase

data FailureTag : Set where
  budgetExhausted : FailureTag
  unknownHead : FailureTag
  unsupportedTerm : FailureTag
  unsupportedExpression : FailureTag
  unboundVariable : FailureTag
  ambiguousBinderClassification : FailureTag
  unsupportedBinderVisibility : FailureTag
  unsupportedBinderModality : FailureTag
  nondependentEntityBinder : FailureTag
  proofDependentPremise : FailureTag
  dependentInfrastructureBinder : FailureTag
  predicateArityMismatch : FailureTag
  expressionArityMismatch : FailureTag

data FailureDetail : Set where
  noDetail : FailureDetail
  nameDetail : R.Name → FailureDetail
  termDetail : R.Term → FailureDetail
  visibilityDetail : R.Visibility → FailureDetail
  modalityDetail : R.Relevance → R.Quantity → FailureDetail

record TranslationFailure : Set where
  constructor translation-failure
  field
    phase : Phase
    tag : FailureTag
    path : List Nat
    detail : FailureDetail
    attemptedRules : List String

data Result {a} (A : Set a) : Set a where
  success : A → Result A
  failure : TranslationFailure → Result A

record ExprArguments (scope : Nat) : Set where
  constructor expr-arguments
  field
    expressions : List (ExprIR scope)
    provenance : List ProvenanceEntry

record ExprTranslation (scope : Nat) : Set where
  constructor translated-expr
  field
    expression : ExprIR scope
    provenance : List ProvenanceEntry

Env : Nat → Set
Env scope = List (Maybe (Fin scope))

liftMaybeFin : ∀ {n} → Maybe (Fin n) → Maybe (Fin (suc n))
liftMaybeFin nothing = nothing
liftMaybeFin (just index) = just (fsuc index)

extendEntity : ∀ {n} → Env n → Env (suc n)
extendEntity env = just fzero ∷ map liftMaybeFin env

extendNonsemantic : ∀ {n} → Env n → Env n
extendNonsemantic env = nothing ∷ env

mkFailure : Phase → FailureTag → FailureDetail → TranslationFailure
mkFailure phase tag detail = translation-failure phase tag [] detail []

resultMap : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → Result A → Result B
resultMap f (success value) = success (f value)
resultMap f (failure problem) = failure problem

normalModality : R.Relevance → R.Quantity → Bool
normalModality R.relevant R.quantity-ω = true
normalModality _ _ = false

surfaceArity : ExprSurface → Nat
surfaceArity (constantWord _) = zero
surfaceArity (unaryForm _ _) = suc zero
surfaceArity (binaryForm _ _ _) = suc (suc zero)

mutual
  translateExpr : ∀ {scope} → Nat → DomainSpec → Env scope → R.Term → Result (ExprTranslation scope)
  translateExpr zero spec env term =
    failure (mkFailure interpretation budgetExhausted (termDetail term))
  translateExpr (suc fuel) spec env (R.var index []) with lookupNat env index
  ... | nothing = failure (mkFailure interpretation unboundVariable noDetail)
  ... | just nothing = failure (mkFailure interpretation unboundVariable noDetail)
  ... | just (just semanticIndex) =
    success (translated-expr (bound semanticIndex) [])
  translateExpr (suc fuel) spec env (R.def name args) =
    translateExpressionHead fuel spec env name args
  translateExpr (suc fuel) spec env (R.con name args) =
    translateExpressionHead fuel spec env name args
  translateExpr (suc fuel) spec env term =
    failure (mkFailure interpretation unsupportedExpression (termDetail term))

  translateExpressionHead
    : ∀ {scope} → Nat → DomainSpec → Env scope → R.Name
    → List (R.Arg R.Term) → Result (ExprTranslation scope)
  translateExpressionHead fuel spec env name args
    with findExpression name (DomainSpec.expressions spec)
  ... | nothing =
    failure (mkFailure interpretation unsupportedExpression (nameDetail name))
  ... | just rule
    with translateArguments fuel spec env (ExpressionRule.ruleId rule) zero
           (ExpressionRule.roles rule) args
  ... | failure problem = failure problem
  ... | success translatedArgs
    with length (ExprArguments.expressions translatedArgs) ==N
         surfaceArity (ExpressionRule.surface rule)
  ... | false =
    failure (mkFailure interpretation expressionArityMismatch (nameDetail name))
  ... | true =
    success
      (translated-expr
        (application (ExpressionRule.ruleId rule) (ExpressionRule.surface rule)
          (ExprArguments.expressions translatedArgs))
        (ruleUsed (ExpressionRule.ruleId rule)
         ∷ ExprArguments.provenance translatedArgs))

  translateArguments
    : ∀ {scope}
    → Nat
    → DomainSpec
    → Env scope
    → String
    → Nat
    → List ArgRole
    → List (R.Arg R.Term)
    → Result (ExprArguments scope)
  translateArguments zero spec env ruleId position roles args =
    failure (mkFailure interpretation budgetExhausted noDetail)
  translateArguments (suc fuel) spec env ruleId position [] [] =
    success (expr-arguments [] [])
  translateArguments (suc fuel) spec env ruleId position [] (_ ∷ _) =
    failure (mkFailure interpretation predicateArityMismatch noDetail)
  translateArguments (suc fuel) spec env ruleId position (_ ∷ _) [] =
    failure (mkFailure interpretation predicateArityMismatch noDetail)
  translateArguments (suc fuel) spec env ruleId position
    (semanticExpression ∷ roles) (R.arg _ term ∷ args)
    with translateExpr fuel spec env term
  ... | failure problem = failure problem
  ... | success translatedExpression
    with translateArguments fuel spec env ruleId (suc position) roles args
  ... | failure problem = failure problem
  ... | success rest =
    success
      (expr-arguments
        (ExprTranslation.expression translatedExpression
         ∷ ExprArguments.expressions rest)
        (ExprTranslation.provenance translatedExpression
         ++L ExprArguments.provenance rest))
  translateArguments (suc fuel) spec env ruleId position
    (infrastructureArgument ∷ roles) (_ ∷ args)
    with translateArguments fuel spec env ruleId (suc position) roles args
  ... | failure problem = failure problem
  ... | success rest =
    success
      (expr-arguments
        (ExprArguments.expressions rest)
        (argumentOmitted ruleId position ∷ ExprArguments.provenance rest))

headName : R.Term → Maybe R.Name
headName (R.def name _) = just name
headName (R.con name _) = just name
headName _ = nothing

headArgs : R.Term → List (R.Arg R.Term)
headArgs (R.def _ args) = args
headArgs (R.con _ args) = args
headArgs _ = []

data HeadClass : Set where
  entityClass : EntityRule → HeadClass
  predicateClass : PredicateRule → HeadClass
  infrastructureClass : InfrastructureRule → HeadClass
  ambiguousClass unknownClass : HeadClass

classifyHead : DomainSpec → R.Name → HeadClass
classifyHead spec name
  with findEntity name (DomainSpec.entities spec)
     | findPredicate name (DomainSpec.predicates spec)
     | findInfrastructure name (DomainSpec.infrastructure spec)
... | just entityRule | just predicateRule | infrastructureRule = ambiguousClass
... | just entityRule | predicateRule | just infrastructureRule = ambiguousClass
... | entityRule | just predicateRule | just infrastructureRule = ambiguousClass
... | just entityRule | nothing | nothing = entityClass entityRule
... | nothing | just predicateRule | nothing = predicateClass predicateRule
... | nothing | nothing | just infrastructureRule = infrastructureClass infrastructureRule
... | nothing | nothing | nothing = unknownClass

translateAtom
  : ∀ {scope}
  → Nat
  → DomainSpec
  → Env scope
  → R.Name
  → List (R.Arg R.Term)
  → Result (Translation scope)
translateAtom fuel spec env name args with findPredicate name (DomainSpec.predicates spec)
... | nothing = failure (mkFailure interpretation unknownHead (nameDetail name))
... | just rule
  with translateArguments fuel spec env (PredicateRule.ruleId rule) zero
         (PredicateRule.roles rule) args
... | failure problem = failure problem
... | success translatedArgs with PredicateRule.surface rule | ExprArguments.expressions translatedArgs
... | equalityPhrase phrase | left ∷ right ∷ [] =
  success
    (translated
      (equal (PredicateRule.ruleId rule) phrase left right)
      (ruleUsed (PredicateRule.ruleId rule)
       ∷ ExprArguments.provenance translatedArgs))
... | equalityPhrase phrase | expressions =
  failure (mkFailure interpretation predicateArityMismatch (nameDetail name))
... | surface | expressions =
  success
    (translated
      (atom
        (PredicateRule.ruleId rule)
        surface expressions)
      (ruleUsed (PredicateRule.ruleId rule)
       ∷ ExprArguments.provenance translatedArgs))

mutual
  translateProp
    : ∀ {scope}
    → Nat
    → DomainSpec
    → Env scope
    → R.Term
    → R.TC (Result (Translation scope))
  translateProp zero spec env term =
    R.returnTC (failure (mkFailure interpretation budgetExhausted (termDetail term)))
  translateProp (suc fuel) spec env
    (R.pi (R.arg (R.arg-info visibility (R.modality relevance quantity)) domain)
          (R.abs hint body)) =
    translatePi fuel spec env visibility relevance quantity domain hint body
  translateProp (suc fuel) spec env term@(R.def name args)
    with findPredicate name (DomainSpec.predicates spec)
  ... | just rule = R.returnTC (translateAtom fuel spec env name args)
  ... | nothing with memberName name (DomainSpec.transparentAliases spec)
  ... | false =
    R.returnTC (failure (mkFailure interpretation unknownHead (nameDetail name)))
  ... | true =
    reduceWhnfWith (DomainSpec.transparentAliases spec) term >>= λ reduced →
    translateProp fuel spec env reduced >>= λ where
      (failure problem) → R.returnTC (failure problem)
      (success result) →
        R.returnTC
          (success
            (translated
              (Translation.proposition result)
              (aliasUnfolded name ∷ Translation.provenance result)))
  translateProp (suc fuel) spec env (R.con name args) =
    R.returnTC (translateAtom fuel spec env name args)
  translateProp (suc fuel) spec env term =
    R.returnTC (failure (mkFailure interpretation unsupportedTerm (termDetail term)))

  translatePi
    : ∀ {scope}
    → Nat
    → DomainSpec
    → Env scope
    → R.Visibility
    → R.Relevance
    → R.Quantity
    → R.Term
    → String
    → R.Term
    → R.TC (Result (Translation scope))
  translatePi fuel spec env visibility relevance quantity domain hint body
    with headName domain
  ... | nothing =
    translatePremise fuel spec env visibility relevance quantity domain hint body
  ... | just name with classifyHead spec name
  ... | ambiguousClass =
    R.returnTC
      (failure
        (mkFailure classification ambiguousBinderClassification (nameDetail name)))
  ... | entityClass entityRule =
    translateEntity fuel spec env visibility relevance quantity
      domain hint body name entityRule
  ... | infrastructureClass infrastructureRule =
    translateInfrastructure fuel spec env visibility relevance quantity
      domain hint body name infrastructureRule
  ... | predicateClass predicateRule =
    translatePremise fuel spec env visibility relevance quantity domain hint body
  ... | unknownClass =
    translatePremise fuel spec env visibility relevance quantity domain hint body

  translateEntity
    : ∀ {scope}
    → Nat
    → DomainSpec
    → Env scope
    → R.Visibility
    → R.Relevance
    → R.Quantity
    → R.Term
    → String
    → R.Term
    → R.Name
    → EntityRule
    → R.TC (Result (Translation scope))
  translateEntity fuel spec env visibility relevance quantity
    domain hint body name entityRule
    with visibility | normalModality relevance quantity | occursAt fuel zero body
  ... | R.visible | true | true =
    translateEntitySupported fuel spec env visibility relevance quantity
      domain hint body entityRule
  ... | R.hidden | true | true =
    translateEntitySupported fuel spec env visibility relevance quantity
      domain hint body entityRule
  ... | R.visible | true | false =
    R.returnTC
      (failure (mkFailure classification nondependentEntityBinder (nameDetail name)))
  ... | R.hidden | true | false =
    R.returnTC
      (failure (mkFailure classification nondependentEntityBinder (nameDetail name)))
  ... | R.visible | false | dependency =
    R.returnTC
      (failure
        (mkFailure classification unsupportedBinderModality
          (modalityDetail relevance quantity)))
  ... | _ | modality | dependency =
    R.returnTC
      (failure
        (mkFailure classification unsupportedBinderVisibility
          (visibilityDetail visibility)))

  translateEntitySupported
    : ∀ {scope}
    → Nat
    → DomainSpec
    → Env scope
    → R.Visibility
    → R.Relevance
    → R.Quantity
    → R.Term
    → String
    → R.Term
    → EntityRule
    → R.TC (Result (Translation scope))
  translateEntitySupported fuel spec env visibility relevance quantity
    domain hint body entityRule
    with translateArguments fuel spec env (EntityRule.ruleId entityRule) zero
           (EntityRule.roles entityRule) (headArgs domain)
  ... | failure problem = R.returnTC (failure problem)
  ... | success domainArguments =
    R.extendContext hint
      (R.arg (R.arg-info visibility (R.modality relevance quantity)) domain)
      (translateProp fuel spec (extendEntity env) body) >>= λ where
      (failure problem) → R.returnTC (failure problem)
      (success bodyTranslation) →
        R.returnTC
          (success
            (translated
              (forallP
                (binder hint (EntityRule.word entityRule)
                  (ExprArguments.expressions domainArguments)
                  (EntityRule.ruleId entityRule) visibility relevance quantity)
                (Translation.proposition bodyTranslation))
              (ruleUsed (EntityRule.ruleId entityRule)
               ∷ (ExprArguments.provenance domainArguments
               ++L Translation.provenance bodyTranslation))))

  translateInfrastructure
    : ∀ {scope}
    → Nat
    → DomainSpec
    → Env scope
    → R.Visibility
    → R.Relevance
    → R.Quantity
    → R.Term
    → String
    → R.Term
    → R.Name
    → InfrastructureRule
    → R.TC (Result (Translation scope))
  translateInfrastructure fuel spec env visibility relevance quantity
    domain hint body name infrastructureRule =
    R.extendContext hint
      (R.arg (R.arg-info visibility (R.modality relevance quantity)) domain)
      (translateProp fuel spec (extendNonsemantic env) body) >>= λ where
      (failure problem) → R.returnTC (failure problem)
      (success bodyTranslation) →
        R.returnTC
          (success
            (translated
              (Translation.proposition bodyTranslation)
              (binderOmitted (InfrastructureRule.ruleId infrastructureRule)
               ∷ Translation.provenance bodyTranslation)))

  translatePremise
    : ∀ {scope}
    → Nat
    → DomainSpec
    → Env scope
    → R.Visibility
    → R.Relevance
    → R.Quantity
    → R.Term
    → String
    → R.Term
    → R.TC (Result (Translation scope))
  translatePremise fuel spec env visibility relevance quantity domain hint body
    with visibility | normalModality relevance quantity | occursAt fuel zero body
  ... | R.visible | true | true =
    R.returnTC (failure (mkFailure classification proofDependentPremise noDetail))
  ... | R.visible | true | false =
    translateProp fuel spec env domain >>= λ where
      (failure problem) → R.returnTC (failure problem)
      (success premiseTranslation) →
        R.extendContext hint
          (R.arg (R.arg-info visibility (R.modality relevance quantity)) domain)
          (translateProp fuel spec (extendNonsemantic env) body) >>= λ where
          (failure problem) → R.returnTC (failure problem)
          (success bodyTranslation) →
            R.returnTC
              (success
                (translated
                  (imply
                    (Translation.proposition premiseTranslation)
                    (Translation.proposition bodyTranslation))
                  (Translation.provenance premiseTranslation
                   ++L Translation.provenance bodyTranslation)))
  ... | R.visible | false | dependency =
    R.returnTC
      (failure
        (mkFailure classification unsupportedBinderModality
          (modalityDetail relevance quantity)))
  ... | _ | modality | dependency =
    R.returnTC
      (failure
        (mkFailure classification unsupportedBinderVisibility
          (visibilityDetail visibility)))

translateClosed : Nat → DomainSpec → R.Term → R.TC (Result (Translation zero))
translateClosed fuel spec term = translateProp fuel spec [] term