Zulip Chat Archive

Stream: general

Topic: to_expr mystery


view this post on Zulip Fabian Glöckle (May 07 2020 at 11:31):

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

view this post on Zulip Sebastian Ullrich (May 07 2020 at 11:38):

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)

view this post on Zulip Sebastian Ullrich (May 07 2020 at 11:40):

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

view this post on Zulip Fabian Glöckle (May 07 2020 at 11:52):

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)

view this post on Zulip Fabian Glöckle (May 07 2020 at 11:53):

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

view this post on Zulip Fabian Glöckle (May 07 2020 at 11:59):

at least to_expr and a certain pexprwas used there as well

view this post on Zulip Sebastian Ullrich (May 07 2020 at 12:01):

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.

view this post on Zulip Fabian Glöckle (May 07 2020 at 12:02):

pexpr.substhowever seems to have disappeared

view this post on Zulip Sebastian Ullrich (May 07 2020 at 12:02):

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

view this post on Zulip Fabian Glöckle (May 07 2020 at 12:03):

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

view this post on Zulip Sebastian Ullrich (May 07 2020 at 12:03):

I think it has been generalized to expr.subst

view this post on Zulip Gabriel Ebner (May 07 2020 at 12:03):

Fabian Glöckle said:

pexpr.substhowever seems to have disappeared

It's now called expr.subst.

view this post on Zulip Fabian Glöckle (May 07 2020 at 12:03):

ah, thanks

view this post on Zulip Fabian Glöckle (May 07 2020 at 12:05):

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

view this post on Zulip Sebastian Ullrich (May 07 2020 at 12:07):

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.

view this post on Zulip Fabian Glöckle (May 07 2020 at 12:09):

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


Last updated: May 10 2021 at 19:16 UTC