[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Chicken-hackers] [PATCH 2/2] * scrutinizer.scm (refine-types): Add spec
From: |
megane |
Subject: |
[Chicken-hackers] [PATCH 2/2] * scrutinizer.scm (refine-types): Add special case for (or pair null) and list-of |
Date: |
Tue, 18 Sep 2018 13:01:55 +0300 |
User-agent: |
mu4e 1.0; emacs 25.1.1 |
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
- [Chicken-hackers] [PATCH 2/2] * scrutinizer.scm (refine-types): Add special case for (or pair null) and list-of,
megane <=