to_expr mystery

Stream: general

[Fabian Glöckle]

Hello, I discovered a behaviour of tactic.to_expr, pexpr quotations and antiquotations which puzzles me:

set_option pp.all true

meta def tactic.interactive.quotation_test (px : interactive.parse ((lean.parser.tk "from") >> interactive.types.texpr)) (pf : interactive.parse ((lean.parser.tk "with") >> interactive.types.texpr)) : tactic unit :=
do x ← tactic.i_to_expr px,
   f ← tactic.i_to_expr pf,
   f' ← tactic.to_expr ``(id %%f),
   tactic.trace f',    -- outputs: @id.{1} (nat → nat) nat.succ
   -- uncomment these lines to get an error two lines above
--    x' ← tactic.to_expr ``(%%f' %%x),
--    tactic.trace x',
   return ()

example : true :=
begin
  quotation_test from 0 with nat.succ,
  trivial
end

Uncommenting the indicated lines gives type mismatch at application: @id.{1} ?m_1 (nat → nat), that is a different interpretation of id %%f in which apparently the correctly inferred implicit argument nat → nat is taken as the first explicit argument.

I admit that I do not have a good understanding of Lean's quotation magic, but if to_expr were a pure function only depending on its argument and the main goal as indicated in the documentation, I think this should not happen.
Documentation:

/-- Elaborate the given quoted expression with respect to the current main goal.
    If `allow_mvars` is tt, then metavariables are tolerated and become new goals if `subgoals` is tt. -/
meta constant to_expr (q : pexpr) (allow_mvars := tt) (subgoals := tt) : tactic expr

[Sebastian Ullrich]

Even if the error points at the first expression, it is most likely raised when elaborating the second expression (after the first one was inserted into it)

[Sebastian Ullrich]

You might have hit an edge case of inserting exprs into pexprs. The robust solution is to try and avoiding doing that.

[Fabian Glöckle]

Thank you. Yes, I can also build the term manually without help by the elaborator.
But I thought inserting exprs into pexprs was the way to go?
In the Tactic Paper it says: "What makes pre-expressions especially useful is that they can contain antiquotations, namely, values of type expr that should be inserted when a metaprogram is executed." (p. 8)

[Fabian Glöckle]

I mean "A Metaprgramming Framework for Formal Verification" by Tactic paper

[Fabian Glöckle]

at least to_expr and a certain pexprwas used there as well

[Sebastian Ullrich]

Antiquoting atomic exprs as in the paper example is definitely safe. It could be that specifically using them in function call position is problematic, since elaboration of applications is pretty involved. Using them as arguments should be fine.

[Fabian Glöckle]

pexpr.substhowever seems to have disappeared

[Sebastian Ullrich]

The C++ Lean code embeds terms into preterms only in a few specific cases, so any usages not covered by that might be brittle

[Fabian Glöckle]

yes, all variants without the antiquotation in function position i could think of worked

[Sebastian Ullrich]

I think it has been generalized to expr.subst

[Gabriel Ebner]

Fabian Glöckle said:

pexpr.substhowever seems to have disappeared

It's now called expr.subst.

[Fabian Glöckle]

ah, thanks

[Fabian Glöckle]

Okay, let's leave it there, no antiquotations of expr in pexpr in function position. Thanks you two!

[Sebastian Ullrich]

Lean 4 doesn't support embedding terms (Expr) into preterms (Syntax) since it doesn't need that anymore itself, so it will be interesting to see how that influences tactic writing. It's of course possible to implement such an embedding manually, just not in constant time.

[Fabian Glöckle]

I think in tactic writing, pexprs are mainly used to access the power of the elaborator and skip implicit arguments when building terms. If Lean 4 has another mechanism for that, it will work just as well