recursive tactic

Stream: metaprogramming / tactics

[Fabian Glöckle]

I am trying to write a (noninteractive) tactic that recursively calls itself. Like in this MWE:

meta def mwe (n : ℕ) : tactic unit :=
do match n with
| 0 := do tactic.trace "done", return unit.star
| m+1 := do tactic.trace "still to go", mwe m
end

resulting in

type mismatch at application
  mwe m
term
  m
has type
  ℕ
but is expected to have type
  tactic_state

It seems to me that when the equation compiler compiles the recursive def, no special treatment is given to the tactic monad's bind, so the tactic_state leaks through.

According to https://wiki.haskell.org/Recursion_in_a_monad, recursion in monads is possible in Haskell (?), and I am asking myself if the same holds for Lean, and if so, how to do it.

[Jannis Limperg]

The problem is that n is a parameter of the function (before the colon) and so you cannot give it as an argument in recursive calls (it remains fixed throughout the recursion). If you put it after the colon, it should work (untested):

meta def mwe : nat -> tactic unit := λ n,
do match n with
| 0 := do tactic.trace "done", return unit.star
| m+1 := do tactic.trace "still to go", mwe m
end

(Changed in Lean 4 btw.)

[Mario Carneiro]

You have to use the equation compiler at the top level to write recursion

meta def mwe : ℕ → tactic unit
| 0 := do tactic.trace "done", return unit.star
| (m+1) := do tactic.trace "still to go", mwe m

[Fabian Glöckle]

oh I see! thanks a bunch to both of you!

[Mario Carneiro]

Jannis's solution also works, although only for meta definitions (otherwise you will get an error saying mwe is not in scope in the recursive call)

[Jannis Limperg]

Mario Carneiro said:

Jannis's solution also works, although only for meta definitions (otherwise you will get an error saying mwe is not in scope in the recursive call)

Oh, I didn't even realise that. I should stop commenting on Lean 3 stuff. :silence:

[Mario Carneiro]

that was one change with lean 4

[Mario Carneiro]

in fact, in earlier versions of lean 3 you couldn't do this even in meta definitions, you have to use the equation compiler

[Mario Carneiro]

so you would get stuff like

meta def loop : tactic unit
| s := loop s

which introduces a useless argument because meta def loop : tactic unit := loop didn't compile

[Mario Carneiro]

You actually still have this issue in lean 3 in mutual defs (which have to use the equation compiler), which explains the useless parameter in src#tactic.rcases_patt_parse_hi', src#tactic.rcases_patt_parse', src#tactic.rcases_patt_parse_list'

[Jannis Limperg]

One more reason Lean 4 makes me very happy.

Fabian Glöckle said:

type mismatch at application
  mwe m
term
  m
has type
  ℕ
but is expected to have type
  tactic_state

Btw to demystify this error: tactic α is defined as something like tactic_state -> (α x tactic_state) (with some layers of wrapping in between). So when you apply mwe : tactic unit to an argument, Lean tries to interpret mwe as a function, unfolds tactic and tries to interpret the argument as a tactic_state.

[Fabian Glöckle]

Yes, thank you!