The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

I get similar times to Gregory.  I tried an uconstr version of the cps
ltac1 build_it, and it runs about 25% faster than the constr version.


On Sat, 1 Aug 2020 23:56:47 -0400
Gregory Malecha <gregory AT bedrocksystems.com> wrote:

> The unsafe version of the tactic is included below, constructing the
> array is quite annoying, maybe there is notation that I missed?
> Certainly adding the [check] here is pretty expensive.
> 
> I filed an issue here which contains the full text (also included
> below): https://github.com/coq/coq/issues/12785
> 
> Returning to the earlier question, I get back a decent amount of
> performance in my original tactic by using [@conj p q l r] rather than
> [conj l r] in both the Ltac and the Ltac2 case.
> 
> My latest figures show less performance loss than I originally
> measured (2x instead of 3x), there might have been too much jitter in
> my tests. The numbers below are averages of 10 fresh runs.
> 
> (* Ltac2 implementation *)
> Ltac2 rec build2 p :=
>   lazy_match! p with
>   | True => constr:(I)
>   | ?p /\ ?q =>
>     let l := build2 p in
>     let r := build2 q in
>     constr:(@conj $p $q $l $r)
>   end.
> 
> (* Ltac2 (Unsafe) implementation *)
> Ltac2 rec build2_unsafe p :=
>   lazy_match! p with
>   | True => constr:(I)
>   | ?p /\ ?q =>
>     let l := build2_unsafe p in
>     let r := build2_unsafe q in
>     let ary := Array.make 4 p in
>     let _ := Array.set ary 1 q in
>     let _ := Array.set ary 2 l in
>     let _ := Array.set ary 3 r in
>     Unsafe.make (Unsafe.App 'conj ary)
>   end.
> 
> (* Ltac2 (Unsafe-Check) implementation *)
> Ltac2 rec build2_unsafe_check p :=
>   lazy_match! p with
>   | True => constr:(I)
>   | ?p /\ ?q =>
>     let l := build2_unsafe_check p in
>     let r := build2_unsafe_check q in
>     let ary := Array.make 4 p in
>     let _ := Array.set ary 1 q in
>     let _ := Array.set ary 2 l in
>     let _ := Array.set ary 3 r in
>     match Unsafe.check (Unsafe.make (Unsafe.App 'conj ary)) with
>     | Val v => v
>     | Err e => Control.throw e
>     end
>   end.
> 
> (* Ltac implementation *)
> Ltac build_it p k :=
>   lazymatch p with
>   | True => k constr:(I)
>   | ?p /\ ?q => build_it p ltac:(fun P => build_it q ltac:(fun Q => k
> constr:(@conj p q P Q)))
>   end.
> 
> Fixpoint build_goal (n : nat) : Prop :=
>   match n with
>   | 0 => True
>   | S n => build_goal n /\ build_goal n
>   end.
> 
> Goal build_goal 10.
>   simpl.
>   Time Control.enter (fun () =>
>     let g := Control.goal () in
>     let pf := build2 g in
>     exact $pf).
>   (** *~0.2241s* *)
>   Undo.
>   Time Control.enter (fun () =>
>     let g := Control.goal () in
>     let pf := build2_unsafe g in
>     exact $pf).
>   (** *~0.1444s* *)
> Time Control.enter (fun () =>
>     let g := Control.goal () in
>     let pf := build2_unsafe_check g in
>     exact $pf).
>   (** *~0.2307s* *)
>   Undo.
>   Time repeat constructor.
>   (** *~0.1658s* *)
>   Undo.
>   Time ltac1:(match goal with
>               | |- ?G => build_it G ltac:(fun p => exact p)
>               end).
>   (** *~0.0939s* *)
> Qed.
> 
>