Hi,
Here's a new version of the patch. This tries to handle #!optional and
#!rest in procedure types correctly, in addition to the parameter
contravariance stuff. The implementation should be cleaner now.
This is still not ready to be merged to the master. At least the
signatures in types.db should be fixed first.
This doesn't try to address any of the issues I raised in the parent
post. Instead, it adds at least one new one:
This is the type for 'map' from the types.db:
(scheme#map (forall (a b)
(#(procedure #:enforce) scheme#map
(
(procedure (a #!rest) b)
(list-of a)
#!rest list
)
(list-of b))))
(Note that the first parameter to map is declared as (a #!rest -> b).)
The scrutinizer checks that the function you pass to map is a subtype
(or of equal type) to the declared parameter type. That is, the function
has to handle all parameters of the declared type (a and #!rest), but
can be more permissive. (Also the result type has to be b or it's
subtype.)
But for example (a -> b) is not a subtype of (a #!rest -> b), it only
allows for one parameter of type a. (Maybe passing more parameters could
cause runtime error or worse.). This means that (map add1 '(1)) fails to
type check.
Fortunately this is easy to fix by removing the #!rest from the type
signature. This shouldn't make the type any less safe than it already is
(unless there's some special case(s) in the scrutinizer I'm unaware of).
The number of arguments wasn't checked to match to the argument count to
map anyway.
Ideally you'd have some way to unify the #!rest in the map's first
argument and the #!rest for map. Maybe some other time.
diff --git a/scrutinizer.scm b/scrutinizer.scm
index ece07ed..282ec1f 100644
--- a/scrutinizer.scm
+++ b/scrutinizer.scm
@@ -942,37 +942,38 @@
(define (match-args args1 args2)
(d "match args: ~s <-> ~s" args1 args2)
- (let loop ((args1 args1) (args2 args2) (opt1 #f) (opt2 #f))
- (cond ((null? args1)
- (or opt2
- (null? args2)
- (optargs? (car args2))))
- ((null? args2)
- (or opt1
- (optargs? (car args1))))
+ (define (optargs? a)
+ (memq a '(#!rest #!optional)))
+
+ (let loop ((args1 args1) (args2 args2))
+ (cond ((null? args1)
+ (or (null? args2)
+ (optargs? (car args2))))
+ ((null? args2) #f)
((eq? '#!optional (car args1))
- (loop (cdr args1) args2 #t opt2))
+ (and (optargs? (car args2))
+ (loop (cdr args1) args2)))
((eq? '#!optional (car args2))
- (loop args1 (cdr args2) opt1 #t))
+ (loop args1 (cdr args2)))
((eq? '#!rest (car args1))
- (match-rest (rest-type (cdr args1)) args2 opt2))
+ (let ((rtype1 (rest-type (cdr args1))))
+ (let-values (((head tail) (span (lambda (x) (not (eq? '#!rest x))) args2)))
+ (and (pair? tail)
+ (null? head)
+ (rawmatch-all (rest-type (cdr tail)) rtype1)))))
((eq? '#!rest (car args2))
- (match-rest (rest-type (cdr args2)) args1 opt1))
- ((match1 (car args1) (car args2))
- (loop (cdr args1) (cdr args2) opt1 opt2))
- (else #f))))
-
- (define (match-rest rtype args opt) ;XXX currently ignores `opt'
- (let-values (((head tail) (span (lambda (x) (not (eq? '#!rest x))) args)))
- (and (every
- (lambda (t)
- (or (eq? '#!optional t)
- (match1 rtype t)))
- head)
- (match1 rtype (if (pair? tail) (rest-type (cdr tail)) '*)))))
-
- (define (optargs? a)
- (memq a '(#!rest #!optional)))
+ (let ((rtype2 (rest-type (cdr args2))))
+ (let lp ((args1 args1))
+ (cond
+ ((or (null? args1)
+ (optargs? (car args1)))
+ (loop args1 args2))
+ (else
+ (and (rawmatch-all rtype2 (car args1))
+ (lp (cdr args1))))))))
+ (else
+ (and (rawmatch-all (car args2) (car args1))
+ (loop (cdr args1) (cdr args2)))))))
(define (match-results results1 results2)
(cond ((eq? '* results1))
@@ -989,6 +990,10 @@
(fluid-let ((all #f))
(match1 t1 t2)))
+ (define (rawmatch-all t1 t2)
+ (fluid-let ((all #t))
+ (match1 t1 t2)))
+
(define (every-match1 lst1 lst2)
(let loop ((lst1 lst1) (lst2 lst2))
(cond ((null? lst1))
diff --git a/tests/scrutinizer-tests.scm b/tests/scrutinizer-tests.scm
index ed313a4..0716d05 100644
--- a/tests/scrutinizer-tests.scm
+++ b/tests/scrutinizer-tests.scm
@@ -226,20 +226,53 @@
(test (= (procedure ()) (procedure ())))
(test (= (procedure () x) (procedure () x)))
;; FIXME
-;(test (= (procedure () . x) (procedure () . x)))
+;; (test (= (procedure () . x) (procedure () . x)))
(test (>< (procedure (x)) (procedure (y))))
(test (>< (procedure () x) (procedure () y)))
+(test (! (procedure () x) (procedure ())))
+(test (! (procedure () x x) (procedure () x)))
+(test (! (procedure () x y) (procedure () x)))
-(test (? (procedure (x)) (procedure (*))))
+(test (< (procedure (*)) (procedure (x))))
(test (? (procedure () x) (procedure () *)))
(test (! (procedure (x)) (procedure ())))
(test (! (procedure (x)) (procedure (x y))))
-(test (? (procedure (x)) (procedure (x #!rest y))))
-(test (! (procedure () x) (procedure ())))
-(test (! (procedure () x) (procedure () x y)))
+(test (? (procedure () . *) (procedure ())))
+(test (? (procedure () . *) (procedure () x)))
+(test (? (procedure () . *) (procedure () noreturn)))
+
+(test (< (procedure ((or x y)) *) (procedure (x) *)))
+(test (< (procedure ((or x y)) x) (procedure (x) (or x y))))
+(test (< (procedure () x) (procedure () (or x y))))
+
+(test (< (procedure ((procedure (x) *)) *)
+ (procedure ((procedure ((or x y)) *)) *)))
+(test (< (procedure (*) (procedure ((or x y)) *))
+ (procedure (*) (procedure (x) *))))
+
+(test (< (procedure (#!rest (or x y)) *) (procedure (#!rest x) *)))
+(test (< (procedure (#!rest (or x y)) *) (procedure (x y) *)))
+(test (< (procedure (#!rest (or x y)) *) (procedure (y #!rest x) *)))
+(test (< (procedure (#!rest x) *) (procedure (x #!rest x) *)))
+(test (< (procedure (#!rest x) *) (procedure (x x) *)))
+(test (< (procedure (x #!rest x) *) (procedure (x x) *)))
+(test (< (procedure (x #!rest y) *) (procedure (x y) *)))
+(test (< (procedure (x #!rest y)) (procedure (x))))
+(test (< (procedure (x x #!rest x) *) (procedure (x x) *)))
+(test (= (procedure (#!rest x) *) (procedure (#!rest x) *)))
+(test (not (< (procedure (#!rest x) *) (procedure (x y) *))))
+
+(test (< (procedure (#!optional (or x y)) *) (procedure (#!optional x) *)))
+(test (< (procedure (#!optional x) *) (procedure () *)))
+(test (< (procedure (#!optional x) *) (procedure (x) *)))
+
+(test (< (procedure (#!rest x) *) (procedure (#!optional x) *)))
+(test (< (procedure (#!rest (or y x)) *) (procedure (#!optional x y) *)))
+(test (< (procedure (#!rest (or y x)) *) (procedure (#!optional x #!rest y) *)))
+(test (< (procedure (#!optional x #!rest y) *) (procedure (#!optional x y) *)))
;; s.a.
;(test (? (procedure () x) (procedure () x . y)))
diff --git a/tests/typematch-tests.scm b/tests/typematch-tests.scm
index 44c6c32..2381f94 100644
--- a/tests/typematch-tests.scm
+++ b/tests/typematch-tests.scm
@@ -7,6 +7,9 @@
(define (make-list n x)
(list-tabulate n (lambda _ x)))
+(define (bomb)
+ (error "bomb"))
+
(define (list-tabulate n proc)
(let loop ((i 0))
(if (fx>= i n)
@@ -212,10 +215,6 @@
(mn pair null)
(mn pair list)
-(mn (procedure (*) *) (procedure () *))
-(m (procedure (#!rest) . *) (procedure (*) . *))
-(mn (procedure () *) (procedure () * *))
-
(mx (forall (a) (procedure (#!rest a) a)) +)
(mx (list fixnum) '(1))
@@ -333,7 +332,7 @@
(define (f2 x) (car x))
(assert
(eq? 'sf
- (compiler-typecase (f2 (list (if bar 1 'a)))
+ (compiler-typecase (f2 (list (if (the * 1) 1 'a)))
(symbol 's)
(fixnum 'f)
((or fixnum symbol) 'sf))))
diff --git a/types.db b/types.db
index b84582b..e3e6deb 100644
--- a/types.db
+++ b/types.db
@@ -687,10 +687,10 @@
(scheme#procedure? (#(procedure #:pure #:predicate procedure) scheme#procedure? (*) boolean))
-(scheme#map (forall (a b) (#(procedure #:enforce) scheme#map ((procedure (a #!rest) b) (list-of a) #!rest list) (list-of b))))
+(scheme#map (forall (a b) (#(procedure #:clean #:enforce) scheme#map ((procedure (a) b) (list-of a) #!rest list) (list-of b))))
(scheme#for-each
- (forall (a) (#(procedure #:enforce) scheme#for-each ((procedure (a #!rest) . *) (list-of a) #!rest list) undefined)))
+ (forall (a) (#(procedure #:enforce) scheme#for-each ((procedure (a) . *) (list-of a) #!rest list) undefined)))
(scheme#apply (#(procedure #:enforce) scheme#apply (procedure #!rest) . *))
(##sys#apply (#(procedure #:enforce) ##sys#apply (procedure #!rest) . *))
@@ -972,7 +972,7 @@
(chicken.base#getter-with-setter
(#(procedure #:clean #:enforce)
chicken.base#getter-with-setter
- ((procedure (#!rest) *) (procedure (* #!rest) . *) #!optional string)
+ ((procedure () *) (procedure (*) . *) #!optional string)
procedure))
(chicken.base#setter (#(procedure #:clean #:enforce) chicken.base#setter (procedure) procedure))
_______________________________________________
Chicken-hackers mailing list
Chicken-hackers@nongnu.org
https://lists.nongnu.org/mailman/listinfo/chicken-hackers
