## Stream: general

### Topic: to_expr mystery

#### 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


#### 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)

#### 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.

#### 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)

#### Fabian Glöckle (May 07 2020 at 11:53):

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

#### Fabian Glöckle (May 07 2020 at 11:59):

at least to_expr and a certain pexprwas used there as well

#### 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.

#### Fabian Glöckle (May 07 2020 at 12:02):

pexpr.substhowever seems to have disappeared

#### 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

#### Fabian Glöckle (May 07 2020 at 12:03):

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

#### Sebastian Ullrich (May 07 2020 at 12:03):

I think it has been generalized to expr.subst

#### Gabriel Ebner (May 07 2020 at 12:03):

Fabian Glöckle said:

pexpr.substhowever seems to have disappeared

It's now called expr.subst.

ah, thanks

#### 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!

#### 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.

#### 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