Normalizing binder parses

Stream: metaprogramming / tactics

[Robert Maxton]

I'm writing an extension to set to allow it to handle functions the way let does. Is there a better way of turning a TSyntax `binder into a TSyntax `funBinder than this?

/--Turns a ```TSyntax ``binder``` into a```TSyntax ``funBinder```.-/
def binderShim {m} [Monad m] [MonadQuotation m] (b : TSyntax ``binder) :
    m (TSyntax ``funBinder) := do
  match b with
  | `(binder| _)                   => pure ⟨←`(_)⟩
  | `(binder| $id:ident)           => pure ⟨id⟩
  | `(binder| {$ibs* $[: $ty]?})   =>
              let ty ← ty.getDM `(_); pure ⟨←`(funBinder | {$ibs* : $ty})⟩
  | `(binder| ⦃$stibs* $[: $ty]?⦄) =>
              let ty ← ty.getDM `(_); pure ⟨←`(funBinder | ⦃$stibs* : $ty⦄)⟩
  | `(binder| [$[$inst :]? $ty])   => pure ⟨←`(funBinder | [$[$inst :]? $ty])⟩
  | `(binder| ($id $ids* $[: $ty]?)) =>
              let ids ← ids.mapM (`(⟨·⟩))
              let ty ← ty.getDM `(_); pure ⟨←`(funBinder | ($(⟨id⟩) $ids* : $ty))⟩
  | _ => unreachable!

[Robert Maxton]

Note that almost all the cases are no-ops and can be individually replaced by lines that look like

| `(binder| $ibs:implicitBinder) => pure ⟨←`(funBinder | $ibs:implicitBinder)⟩

I just thought the above was somewhat more aesthetic; but what I can't seem to do is just handle the one distinct case, the case of explicit binders/type ascriptions, and then have all the rest just be

| `(binder| $b) => pure ⟨←`(funBinder | $b)⟩

... at least, not without breaking the thin veneer of type safety with a raw cast, which I'd still rather not do.

[Robert Maxton]

Oh, I should say that a TSyntax binder` is

syntax binder := ppSpace (binderIdent <|> bracketedBinder)

[Kyle Miller]

I would avoid redoing any of this processing if possible. The best way to emulate let is to use let itself:

import Lean

open Lean Meta Elab Tactic Term

syntax "set'" letDecl (" with " "← "? ident)? : tactic

elab_rules : tactic
  | `(tactic| set'%$tk $d:letDecl $[with $[←%$rev]? $h?]?) => withRef tk do
    let rev := rev matches some (some _)
    let oldHyps ← withMainContext getLocalHyps
    let letTac ← `(tactic| let $d:letDecl)
    evalTactic letTac
    withMainContext do
      let newHyps ← getLocalHyps
      unless oldHyps.size + 1 = newHyps.size do
        throwError "\
          Invalid 'set', expecting a single single new local variable. \
          Got {newHyps[oldHyps.size:]}."
      let new := newHyps[oldHyps.size]!
      let some newVal ← new.fvarId!.getValue?
        | throwError "\
            Invalid 'set', new local variable does not have an associated value. \
            This could be caused by pattern matching."
      withMainContext do
        let rwThm ← mkEq newVal new
        let rwPf ← mkExpectedTypeHint (← mkEqRefl new) rwThm
        -- let thm ← if rev then mkEq newVal new else mkEq new newVal
        -- let thmPf ← mkExpectedTypeHint (← mkEqRefl new) thm
        evalTactic (← `(tactic| try rewrite [$(← exprToSyntax rwPf):term] at *))
        if let some h := h? then
          liftMetaTactic1 fun g => do
            let thmPf ← if rev then pure rwPf else mkEqSymm rwPf
            let (_, g) ← g.note h.getId thmPf
            return g

example : 2 + 3 = 4 := by
  set' x := 2 with h
  -- ⊢ x + 3 = 4

[Kyle Miller]

example : True := by
  set' f x := 1 + x with h
  /-
  f : Nat → Nat := fun x ↦ 1 + x
  h : f = fun x ↦ 1 + x
  ⊢ True
  -/

[Robert Maxton]

Hm. Wish I had thought of/seen that earlier, before I got the messy parsing already working... :p
But no, you're right, it's better for maintainability to reuse existing machinery when possible. I'll go adjust.