Jason Gross (Sep 26 2022 at 15:14): Jason Gross (Sep 26 2022 at 15:14):Does Ltac2 allocate a new evar for every antiquotation? (Things like '($foo $bar))
Janno (Sep 26 2022 at 15:17):EDIT: it is _'s fault that an evar for the type is created.
From Ltac2 Require Import Ltac2.
Set Default Proof Mode "Classic".
Goal True.
unshelve ltac2:(let x := '(_) in ()); [| |].
seems to indicate that open_constr: creates an evar for the type (and the value, in this case).
Gaëtan Gilbert (Sep 26 2022 at 15:18):no, _ with no type constraint does that
Janno (Sep 26 2022 at 15:18):Oh, I see.
Jason Gross (Sep 26 2022 at 15:21):I guess Ltac2 is smart enough to not generate spurious evars, according to
Require Import Ltac2.Ltac2.
Goal True.
Optimize Proof. (* Evars: 1 -> 1 *)
ltac1:(let v := open_constr:(I) in idtac).
Optimize Proof. (* Evars: 1 -> 1 *)
let v := open_constr:(I) in ().
Optimize Proof. (* Evars: 1 -> 1 *)
ltac1:(let v := constr:(I) in let w := open_constr:(v) in idtac).
Optimize Proof. (* Evars: 1 -> 1 *)
let v := open_constr:(I) in let w := open_constr:($v) in ().
Optimize Proof. (* Evars: 1 -> 1 *)
let v := open_constr:(I) in let w := open_constr:(ltac2:(Control.refine (fun () => v))) in ().
Optimize Proof. (* Evars: 3 -> 1 *)
let v := open_constr:(I) in let w := open_constr:(@conj True True $v $v) in ().
Optimize Proof. (* Evars: 1 -> 1 *)
Jason Gross has marked this topic as resolved.
Gaëtan Gilbert (Sep 26 2022 at 15:22):why would it even generate an evar?
Jason Gross (Sep 26 2022 at 15:26):I vaguely recall the documentation saying something about how $v is equivalent to ltac2:(Control.refine (fun () => v)), which, if taken literally, suggests evar generation. And I have a vague sense that when I translate Ltac1 to Ltac2 without introducing anything unsafe, it gets a little bit slower, and was wondering if this could be a cause.
Last updated: Oct 12 2024 at 12:01 UTC