Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: recursive tactic


Fabian Glöckle (May 10 2022 at 12:04):

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 (May 10 2022 at 12:10):

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 (May 10 2022 at 12:10):

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 (May 10 2022 at 12:11):

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

Mario Carneiro (May 10 2022 at 12:11):

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 (May 10 2022 at 12:13):

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 (May 10 2022 at 12:13):

that was one change with lean 4

Mario Carneiro (May 10 2022 at 12:13):

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 (May 10 2022 at 12:14):

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 (May 10 2022 at 12:18):

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 (May 10 2022 at 12:20):

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 (May 10 2022 at 15:04):

Yes, thank you!


Last updated: Dec 20 2023 at 11:08 UTC