coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Ltac2 Performance Question

From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
To: Gregory Malecha <gregory AT bedrocksystems.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Ltac2 Performance Question
Date: Sat, 1 Aug 2020 14:02:39 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qv1-f54.google.com
Ironport-phdr: 9a23:FcTIRBf1xz/v4G9Dht4Y44MvlGMj4u6mDksu8pMizoh2WeGdxcW8Zx7h7PlgxGXEQZ/co6odzbaP7ea/ASdZuMvJmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MRS7oR/Tu8UKjoduN7s9xxvUqXZUZupawn9lK0iOlBjm/Mew+5Bj8yVUu/0/8sNLTLv3caclQ7FGFToqK2866tHluhnFVguP+2ATUn4KnRpSAgjK9w/1U5HsuSbnrOV92S2aPcrrTbAoXDmp8qlmRAP0hCoBKjU063/chNBug61HoRKhvx1/zJDSYIGJL/p1Y6fRccoHSWZdQspdUipMCZ6+YYQSFeoMJehWoYnjqVUTrhWxBwesCuTgxTBUiXH7xrE63uY7HA3axgEsA8wCvXLJp9v1LqcSVuW1wbHGwTXBaPNW3zb96IvWfRAlv/6DQ6l9ccXUyUY1FgPFik+cppDiPzOQ2OgGrm+W7+hnVeKpim4nqB9+ojyxycgykYTJiYcVxUrF9SV92oo6Odq4SEtibNOiDZBfuD2UOZFsTcM+X2Fnpjw6yrsetJKncyUG1YkrygDfZvGEcIWF7QzuWuieLDl2in9odqyzihiy/EW91+DyVse53EtUoyRLjNTBtX4D2hjT5MaHSfZw+Fqq1zWX1w3L9O1IPUQ5mbDYJpMh2LI8iIcfvEDZEiL2l0j6lLGae0Q49uS17unrf7HrqYOZOoJ7iwzyLrgil8mxDOk3PAgDWnWX9vi42bDg+ED2W6hFjvM4kqTcvpDVO8sWq6G8DgJRyIkv9gqwAjG729oCh3YHNkhKeBefgojpJV7OJPf4AO+6g1u2kTdrw+nKPqT/ApnQN3TDnrfscLln505Tzwozyt9f55ZKBb0bPP3zXUrxuMTZDh8/LQO03/7qBMth2o4aQ26CAa+UPLnMvVOV4u8jOemBaYANtDb4Mfcl5vrujXEjmV8aeKmkxZkXaHe+HvRnIEWWf37sjckfHmoRsQo+SfbliFyGUTJJe3myWKc86ikhCI26FYfDWpytgLuZ0SinGZ1Wf3lKBUyIEXf1bIqJQOwMaSKXIs95iDMIT7mhS4k71RGvrgD20bRnLvCHshEf4L352ddy/fybsBg2+Dd0BozJ3HuAQGZuj0sCSjMs26t8ul1m1lqGyu5zhPkORvJJ4PYcGAU9M5/fwuh3Bvj9XwvAepGCT1PsCoGkBjcwTd81ztImbEN0GtHkhRfGiXn5S4QJnqCGUcRnupnX2GL8coMkky6fiPsRymI+S84KDlWIw7Zl/lGKVYHMmkSd0a2tcPZEhXOfxCK41WOL+XpgfktwXKHCBy1NY0LXqZHg+BqHQeLyT7sgNQRFxIiJLa4YMoS432UDf+/qPZHlW0z0nm6xARiSwbbVNdjlfmwc2GPWD01Wyg0=

On Sat, 1 Aug 2020 13:16:32 -0400
Gregory Malecha <gregory AT bedrocksystems.com> wrote:

> Thanks for pointing that out. It inspired me to look at the resulting
> code. I get the following:
>
> build : constr -> constr
> build :=
> fun x =>
> let rec build :=
> fun p =>
> let m :=
> [Pattern.MatchPattern, pattern:(True), (fun _ => fun _ =>
> constr:(I)); Pattern.MatchPattern, pattern:(and ?p ?q),
> (fun _ =>
> fun p => let q := Array.get p 1 with p := Array.get p 0 in
> let l := build p in let r := build q in constr:(@conj _ _ _ _))] with
> t := p in
> Pattern.lazy_match0 t m in
> build x
>
> I assume that the `_`s in the constr: are printing artifacts.
>
> You are right, building the term with Unsafe gets me performance on
> par with Ltac. It seems like this would be a natural implementation
> of constr, and for some reason I thought that I had read that it was
> in the manual, but I must be mistaken.

Grregory,

What does the Unsafe-using version of your example look like?

[Coq-Club] Ltac2 Performance Question, Gregory Malecha, 08/01/2020
- Re: [Coq-Club] Ltac2 Performance Question, Jason Gross, 08/01/2020
  - Re: [Coq-Club] Ltac2 Performance Question, Gregory Malecha, 08/01/2020
    - Re: [Coq-Club] Ltac2 Performance Question, Jason Gross, 08/01/2020
    - Re: [Coq-Club] Ltac2 Performance Question, jonikelee AT gmail.com, 08/01/2020
      - Re: [Coq-Club] Ltac2 Performance Question, Gregory Malecha, 08/02/2020
        
        Re: [Coq-Club] Ltac2 Performance Question, Jason Gross, 08/02/2020
        
        Re: [Coq-Club] Ltac2 Performance Question, Gregory Malecha, 08/02/2020
        
        Re: [Coq-Club] Ltac2 Performance Question, Jason Gross, 08/02/2020
        
        Re: [Coq-Club] Ltac2 Performance Question, jonikelee AT gmail.com, 08/02/2020