Random calc ranges

Stream: std4

[Patrick Massot]

The following code is copy-pasted from Lean core calc tactic except that it tries to report Lsp ranges for individual calc steps. But the reported ranges seem completely off.

import Lean.Elab.Calc
import Lean.Elab.Tactic.ElabTerm

import Std.Lean.Position

namespace Lean.Elab.Term
open Meta

/-- A variation on elabCalcSteps from core. -/
def myElabCalcSteps (steps : TSyntax ``calcSteps) : TermElabM Expr := do
  let mut result? := none
  let mut prevRhs? := none
  for step in ← getCalcSteps steps do
    let `(calcStep| $pred := $proofTerm) := step | unreachable!

    -- The next two lines are new compared to core.
    let some stxRange := (← getFileMap).rangeOfStx? step | unreachable!
    dbg_trace toJson stxRange

    let type ← elabType <| ← do
      if let some prevRhs := prevRhs? then
        annotateFirstHoleWithType pred (← inferType prevRhs)
      else
        pure pred
    let some (_, lhs, rhs) ← getCalcRelation? type |
      throwErrorAt pred "invalid 'calc' step, relation expected{indentExpr type}"
    if let some prevRhs := prevRhs? then
      unless (← isDefEqGuarded lhs prevRhs) do
        throwErrorAt pred "invalid 'calc' step, left-hand-side is{indentD m!"{lhs} : {← inferType lhs}"}\nprevious right-hand-side is{indentD m!"{prevRhs} : {← inferType prevRhs}"}" -- "
    let proof ← withFreshMacroScope do elabTermEnsuringType proofTerm type
    result? := some <| ← do
      if let some (result, resultType) := result? then
        synthesizeSyntheticMVarsUsingDefault
        withRef pred do mkCalcTrans result resultType proof type
      else
        pure (proof, type)
    prevRhs? := rhs
  return result?.get!.1
end Lean.Elab.Term


namespace Lean.Elab.Tactic
open Meta

/-- Elaborator for the `calc` tactic mode variant. The only difference with the core version
from Lean/Elab/Tactic/Calc.lean is the call to `myElabCalcSteps` instead of `elabCalcSteps`. -/
elab_rules : tactic
| `(tactic|calc $stx) => withMainContext do
  let steps : TSyntax ``calcSteps := ⟨stx⟩
  let (val, mvarIds) ← withCollectingNewGoalsFrom (tagSuffix := `calc) do
    let target ← getMainTarget
    let tag ← getMainTag
    runTermElab do
    let mut val ← Term.myElabCalcSteps steps
    let mut valType ← inferType val
    unless (← isDefEq valType target) do
      let rec throwFailed :=
        throwError "'calc' tactic failed, has type{indentExpr valType}\nbut it is expected to have type{indentExpr target}"
      let some (_, _, rhs) ← Term.getCalcRelation? valType | throwFailed
      let some (r, _, rhs') ← Term.getCalcRelation? target | throwFailed
      let lastStep := mkApp2 r rhs rhs'
      let lastStepGoal ← mkFreshExprSyntheticOpaqueMVar lastStep (tag := tag ++ `calc.step)
      (val, valType) ← Term.mkCalcTrans val valType lastStepGoal lastStep
      unless (← isDefEq valType target) do throwFailed
    return val
  (← getMainGoal).assign val
  replaceMainGoal mvarIds


example (a b c d : Nat) (h₁ : a = b) (h₂ : b = c) (h₃ : c = d) : a = d := by
calc a
  = b := by exact h₁
_ = c := h₂
_ = d := h₃

[Wojciech Nawrocki]

Trying let some leanRange := step.raw.getRange? | throwError "no range", it would appear that the Lean ranges themselves are messed up. Possibly getCalcSteps results in this inconsistency because the range for steps appears correct.

[Patrick Massot]

How do you interpret leanRange? I get results like { start := { byteIdx := 2963 }, stop := { byteIdx := 3020 } }

[Gabriel Ebner]

Only the first step is off, and that's because getCalcSteps transforms the syntax of the first step (the first step has a different syntax than the rest!).

[Gabriel Ebner]

One way to fix this would be to add a withRef step0 do at the beginning of getCalcFirstStep.

[Wojciech Nawrocki]

Probably you ought to set (canonicalOnly := true) in the call to Syntax.getRange? so that the synthetic := injected by getCalcFirstStep does not get picked up.

[Patrick Massot]

Maybe I got extra confused because the line count starts at 0 and VSCode starts at 1.

[Patrick Massot]

The withRef step0 do suggestion seems to work! (combined with knowing lines starts at 0...)

[Patrick Massot]

Thanks Wojciech and Gabriel!

[Wojciech Nawrocki]

Patrick Massot said:

How do you interpret leanRange? I get results like { start := { byteIdx := 2963 }, stop := { byteIdx := 3020 } }

I didn't try to read them off literally (they are UTF-8 offsets), but you can see that they overlap in a way that doesn't make sense.

[Wojciech Nawrocki]

Wojciech Nawrocki said:

Probably you ought to set (canonicalOnly := true) in the call to Syntax.getRange? so that the synthetic := injected by getCalcFirstStep does not get picked up.

Ah, this doesn't work since canonicalOnly := true will not to find "the earliest canonical range" but rather expects the top-level one to be canonical and otherwise returns none.