[Chicken-hackers] [PATCH 2/2] * scrutinizer.scm (refine-types): Add special case for (or pair null) and list-of

[megane]

Hi,

Here's a patch for #1533. The fix itself is pretty simple.

The first patch makes scrutinizer tests give more info when a test
fails, which makes it faster to figure out these refinement issues.


>From 7eca29fcaef8a8465b900c1400118982e58eaa7b Mon Sep 17 00:00:00 2001
From: megane <address@hidden>
Date: Tue, 18 Sep 2018 11:30:45 +0300
Subject: [PATCH 1/2] * tests/scrutinizer-tests.scm (test): Add more
 information to failure messages

---
 tests/scrutinizer-tests.scm | 33 ++++++++++++++++++++++++---------
 1 file changed, 24 insertions(+), 9 deletions(-)

diff --git a/tests/scrutinizer-tests.scm b/tests/scrutinizer-tests.scm
index ed313a4..94ce66b 100644
--- a/tests/scrutinizer-tests.scm
+++ b/tests/scrutinizer-tests.scm
@@ -9,6 +9,10 @@
 (define-syntax test
   (er-macro-transformer
    (lambda (expr rename _)
+     (define extra-fail-info '())
+     (define (add-fail-info msg)
+       (set! extra-fail-info (cons (string-append "  " msg) extra-fail-info))
+       #f)
      (define pass
        (let loop ((e (cadr expr)))
          (case (car e)
@@ -18,25 +22,36 @@
            ((<=)  (and (type<=? (cadr e) (caddr e))
                        (match-types (caddr e) (cadr e))))
            ;; subtype
-           ((<)   (and (type<=? (cadr e) (caddr e))
-                       (match-types (caddr e) (cadr e))
-                       (not (type<=? (caddr e) (cadr e)))))
+           ((<)   (and (or (type<=? (cadr e) (caddr e))
+                          (add-fail-info "<= returned #f"))
+                      (or (match-types (caddr e) (cadr e))
+                          (add-fail-info ">= returned #f"))
+                       (or (not (type<=? (caddr e) (cadr e)))
+                          (add-fail-info "not >= returned #f"))))
            ;; type equality
-           ((=)   (and (type<=? (cadr e) (caddr e))
-                       (type<=? (caddr e) (cadr e))))
+           ((=)   (and (or (type<=? (cadr e) (caddr e))
+                          (add-fail-info "<= failed"))
+                       (or (type<=? (caddr e) (cadr e))
+                          (add-fail-info ">= failed"))))
            ;; fuzzy match (both directions)
            ((?)   (and (match-types (cadr e) (caddr e))
                        (match-types (caddr e) (cadr e))))
            ;; fuzzy non-match (both directions)
-           ((!)   (and (not (match-types (cadr e) (caddr e)))
-                       (not (match-types (caddr e) (cadr e)))))
+           ((!)   (and (or (not (match-types (cadr e) (caddr e)))
+                          (add-fail-info ">= was true"))
+                       (or (not (match-types (caddr e) (cadr e)))
+                          (add-fail-info "<= was true"))))
            ;; strict non-match (both directions)
            ((><)  (and (not (type<=? (cadr e) (caddr e)))
                        (not (type<=? (caddr e) (cadr e)))))
            ;; A refined with B gives C
-           ((~>)  (equal? (refine-types (cadr e) (caddr e))
-                          (cadddr e))))))
+           ((~>)  (let ((t (refine-types (cadr e) (caddr e))))
+                   (or (equal? t (cadddr e))
+                       (add-fail-info
+                        (format "Refined to `~a', but expected `~a'" t (cadddr 
e)) )))))))
      (printf "[~a] ~a~n" (if pass " OK " "FAIL") (cadr expr))
+     (unless pass
+       (for-each print extra-fail-info))
      (when (not pass) (set! success #f))
      (rename '(void)))))
 
-- 
2.7.4

>From f3dba60ba79de65969d51bc2c93281b8d18413a7 Mon Sep 17 00:00:00 2001
From: megane <address@hidden>
Date: Tue, 18 Sep 2018 12:42:44 +0300
Subject: [PATCH 2/2] * scrutinizer.scm (refine-types): Add special case for
 (or pair null) and list-of

Fixes #1533
* tests/scrutinizer-tests.scm: New test. Note list is an alias for (list-of *)
* tests/typematch-tests.scm: Add test + fix 'infer' macro
---
 scrutinizer.scm             |  5 +++++
 tests/scrutinizer-tests.scm |  1 +
 tests/typematch-tests.scm   | 16 +++++++++++-----
 3 files changed, 17 insertions(+), 5 deletions(-)

diff --git a/scrutinizer.scm b/scrutinizer.scm
index e30d81b..ce84d91 100644
--- a/scrutinizer.scm
+++ b/scrutinizer.scm
@@ -1442,6 +1442,11 @@
        ((and (pair? t2) (memq (car t2) '(forall refine)))
         (let ((t2* (loop t1 (third t2))))
           (and t2* (list (car t2) (second t2) t2*))))
+       ;; (or pair null) ~> (list-of a) -> (list-of a)
+       [(and (pair? t1) (eq? (car t1) 'or)
+             (lset=/eq? '(null pair) (cdr t1))
+             (and (pair? t2) (eq? 'list-of (car t2))))
+        t2]
        ((and (pair? t1) (eq? (car t1) 'or))
         (let ((ts (filter-map (lambda (t) (loop t t2)) (cdr t1))))
           (and (pair? ts) (cons 'or ts))))
diff --git a/tests/scrutinizer-tests.scm b/tests/scrutinizer-tests.scm
index 94ce66b..939351a 100644
--- a/tests/scrutinizer-tests.scm
+++ b/tests/scrutinizer-tests.scm
@@ -304,6 +304,7 @@
 (test (~> (list (refine (a) x))
           (refine (a) (list (refine (b) y)))
           (refine (a) (list (refine (b) y)))))
+(test (~> (or pair null) list list))
 
 (begin-for-syntax
   (when (not success) (exit 1)))
diff --git a/tests/typematch-tests.scm b/tests/typematch-tests.scm
index e4123cd..4919496 100644
--- a/tests/typematch-tests.scm
+++ b/tests/typematch-tests.scm
@@ -66,11 +66,12 @@
    (lambda (e _i _c)
      (apply
       (lambda (t x)
-       `(test-equal ',(strip-syntax e)
-          (compiler-typecase ,x
-            (,t #t)
-            (else #f))
-          #t))
+       ;; TODO: test-equal smashes types: change rest of the macros
+       ;; to handle this
+       `(let ([res (compiler-typecase ,x
+                     (,t #t)
+                     (else #f))])
+          (test-equal ',(strip-syntax e) res #t)))
       (cdr e)))))
 
 (define-syntax infer-not
@@ -392,4 +393,9 @@
 ;; Always a bignum
 (infer-last (fixnum bignum) #x7fffffffffffffff)
 
+;; Issue #1533
+(let ([a (the (or pair null) (cons 1 '()))])
+  (length a) ; refine (or pair null) with list (= (list-of *))
+  (infer list a))
+
 (test-exit)
-- 
2.7.4