Improve calc user experience

[leodemoura]

This is a placeholder for a few issues reported by @digama0 and Heather MacBeth.
TODO: list all issues here.

[digama0]

cc: @hrmacbeth

[digama0]

• Editing a calc block is syntactically fiddly. Initially, you have

  calc a <= b := prf

  but adding a line to this means moving the <= b := down, but keeping the prf on the first line, and adding a ... (now _) on the newly created line:

  calc a <= c := prf
    _ <= b := prf'

  A code action to add a new line to an existing calc block would help a lot.
• The syntax shown just above doesn't actually work, because the withPosition is in the wrong place. In fact, the more common indentation pattern is

  calc   a
      <= c := prf
    _ <= b := prf'

  and this also doesn't work. The version that works is

  calc
      a <= c := prf
      _ <= b := prf'

  which is difficult to make look good if a is more than one character. The suggestion to fix this is to parse calc as (approximately, untested):

  syntax "calc" withPosition(term ":=" term) withPosition((colGe term ":=" term)*)

• Heather suggested changing the calc tactic (not the term) such that if the final RHS does not defeq match the goal RHS, it returns a final inequality as a subgoal, as if the block had an extra _ <= _ : ?_ line at the end. This would make it easier to write calc blocks by working from the left end rather than having to write lines 1, n, then 2, ..., n-1 in that order.
• The elaboration order seems to work from the bottom up, most likely due to the trans applications that calc macro expands to, which means that errors in later lines can sometimes hide errors textually earlier, which is confusing for users. This can be fixed by having calc be an elab that takes control of the elaboration order.

[leodemoura]

The elaboration order seems to work from the bottom up, most likely due to the trans applications that calc macro expands to, which means that errors in later lines can sometimes hide errors textually earlier, which is confusing for users. This can be fixed by having calc be an elab that takes control of the elaboration order.

Do you have a #mwe for this one? We already had an elaborate for calc that controls the elaboration order.

[leodemoura]

Heather suggested changing the calc tactic (not the term) such that if the final RHS does not defeq match the goal RHS, it returns a final inequality as a subgoal, as if the block had an extra _ <= _ : ?_ line at the end. This would make it easier to write calc blocks by working from the left end rather than having to write lines 1, n, then 2, ..., n-1 in that order.

The commit above does not fix this one.

[digama0]

I haven't managed to replicate the elaboration order bug (cc: @hrmacbeth?), and I think this was a lean 3 behavior in the first place so it probably wasn't inherited, but I did notice some issues with errors not being reported in independent calc lines which are regressions relative to the lean 3 behavior:

-- lean 3
example (a b : nat) : 1 ≤ 2 :=
calc
  1 ≤ a + b : by refl -- error
  ... ≤ b : by refl -- error
  ... ≤ 2 : by refl -- error

-- lean 4
example (a b : Nat) : 1 ≤ 2 :=
calc
  1 ≤ a + b := by rfl -- error
  _ ≤ b := by rfl -- error not reported
  _ ≤ 2 := by rfl -- error not reported

[leodemoura]

@digama0 The commit above should address this issue.