Re: feature/native-comp c60f2f4: Fix `comp-cstr-intersection-no-hashcons' for negated result cstr

Re: feature/native-comp c60f2f4: Fix `comp-cstr-intersection-no-hashcons' for negated result cstr

[Pip Cet]

On Sat, Mar 6, 2021 at 10:17 PM Andrea Corallo <akrl@savannah.gnu.org> wrote:
> branch: feature/native-comp
> commit c60f2f458a63a8ae4288652228f24e43fdc7bba7
> Author: Andrea Corallo <akrl@sdf.org>
> Commit: Andrea Corallo <akrl@sdf.org>
>
>     Fix `comp-cstr-intersection-no-hashcons' for negated result cstr
>
>         * lisp/emacs-lisp/comp-cstr.el
>         (comp-cstr-intersection-no-hashcons): When negated and
>         necessary relax dst to t.
>         * test/src/comp-tests.el (comp-tests-type-spec-tests): Add a test.
> ---
>  lisp/emacs-lisp/comp-cstr.el | 32 +++++++++++++++++++-------------
>  test/src/comp-tests.el       |  9 ++++++++-
>  2 files changed, 27 insertions(+), 14 deletions(-)
>
> diff --git a/lisp/emacs-lisp/comp-cstr.el b/lisp/emacs-lisp/comp-cstr.el
> index d6423ef..4397a91 100644
> --- a/lisp/emacs-lisp/comp-cstr.el
> +++ b/lisp/emacs-lisp/comp-cstr.el
> @@ -1001,20 +1001,26 @@ promoted to their types.
>  DST is returned."
>    (with-comp-cstr-accessors
>      (apply #'comp-cstr-intersection dst srcs)

I still think this code is incorrect, because it does an eq/eql-based
intersection first and tries to relax the constraint later. Consider

(let ((comp-ctxt (make-comp-cstr-ctxt)))
  (comp-cstr-intersection-no-hashcons
   (make-comp-cstr)
   (comp-value-to-cstr '(a))
   (comp-value-to-cstr '(a))))

That should return a constraint matching all (or many) conses, right?
It returns an empty constraint.

(let* ((cons1 '(a))
       (cons2 (copy-sequence cons1))
       (cons3 (copy-sequence cons1)))
  (funcall (native-compile
            `(lambda (x y)
               (if (equal x '(a))
                   (setq x ',cons1))
               (if (equal y '(a))
                   (setq y ',cons2))
                 (unless (or (eq x ',cons1)
                             (eq x 'a))
                   (error "x is %S" x))
                 (unless (eq y ',cons2)
                   (error "2"))
                 (if (equal x y) x)))
           '(a) '(a)))

Should return (a), but returns nil.

Pip

Re: feature/native-comp c60f2f4: Fix `comp-cstr-intersection-no-hashcons' for negated result cstr

[Andrea Corallo via Emacs development discussions.]

Pip Cet <pipcet@gmail.com> writes:

> On Sat, Mar 6, 2021 at 10:17 PM Andrea Corallo <akrl@savannah.gnu.org> wrote:
>> branch: feature/native-comp
>> commit c60f2f458a63a8ae4288652228f24e43fdc7bba7
>> Author: Andrea Corallo <akrl@sdf.org>
>> Commit: Andrea Corallo <akrl@sdf.org>
>>
>>     Fix `comp-cstr-intersection-no-hashcons' for negated result cstr
>>
>>         * lisp/emacs-lisp/comp-cstr.el
>>         (comp-cstr-intersection-no-hashcons): When negated and
>>         necessary relax dst to t.
>>         * test/src/comp-tests.el (comp-tests-type-spec-tests): Add a test.
>> ---
>>  lisp/emacs-lisp/comp-cstr.el | 32 +++++++++++++++++++-------------
>>  test/src/comp-tests.el       |  9 ++++++++-
>>  2 files changed, 27 insertions(+), 14 deletions(-)
>>
>> diff --git a/lisp/emacs-lisp/comp-cstr.el b/lisp/emacs-lisp/comp-cstr.el
>> index d6423ef..4397a91 100644
>> --- a/lisp/emacs-lisp/comp-cstr.el
>> +++ b/lisp/emacs-lisp/comp-cstr.el
>> @@ -1001,20 +1001,26 @@ promoted to their types.
>>  DST is returned."
>>    (with-comp-cstr-accessors
>>      (apply #'comp-cstr-intersection dst srcs)
>
> I still think this code is incorrect, because it does an eq/eql-based
> intersection first and tries to relax the constraint later. Consider
>
> (let ((comp-ctxt (make-comp-cstr-ctxt)))
>   (comp-cstr-intersection-no-hashcons
>    (make-comp-cstr)
>    (comp-value-to-cstr '(a))
>    (comp-value-to-cstr '(a))))
>
> That should return a constraint matching all (or many) conses, right?
> It returns an empty constraint.

I think you are right, will have a look into this evening.

Thanks

  Andrea