~ chicken-core (chicken-5) 097f6425f7fabf02d876fc82eb15be69e246e509
commit 097f6425f7fabf02d876fc82eb15be69e246e509
Author: Evan Hanson <evhan@foldling.org>
AuthorDate: Thu Sep 25 19:40:51 2014 +1200
Commit: Peter Bex <peter.bex@xs4all.nl>
CommitDate: Sun Oct 12 19:22:09 2014 +0200
Minor improvements to predicated/enforcing type inference
Improves inference for #:predicate and #:enforce branches by trying a
bit harder to find the smaller of the possible typesets.
Improves inference for enforcing calls when the procedure is found in
the type environment by ensuring procedure names are preserved by
`resolve`.
Fixes a bug in `type<=` where a right-hand-side type variable would be
overwritten by its type when unified, possibly causing a cxr-style error
later on.
Handles some previously ignored cases in `type<=`: left-side boolean,
number & undefined; (not ...) types; (or ...) comparisons against simple
types.
Adds predicate types for `port?` and `pointer-like?` to types.db.
Signed-off-by: Peter Bex <peter.bex@xs4all.nl>
diff --git a/scrutinizer.scm b/scrutinizer.scm
index fc88438a..3af3fab7 100644
--- a/scrutinizer.scm
+++ b/scrutinizer.scm
@@ -30,7 +30,7 @@
procedure-type? named? procedure-result-types procedure-argument-types
noreturn-type? rest-type procedure-name d-depth
noreturn-procedure-type? trail trail-restore walked-result
- multiples procedure-arguments procedure-results
+ multiples procedure-arguments procedure-results typeset-min
smash-component-types! generate-type-checks! over-all-instantiations
compatible-types? type<=? match-types resolve match-argument-types))
@@ -462,7 +462,8 @@
(and-let* ((t2 (rec (third t))))
`(forall ,(second t) ,t2)))
((or)
- `(or ,@(remove (cut match-types <> pt typeenv #t) (cdr t))))
+ (let ((ts (filter (cut match-types <> pt typeenv) (cdr t))))
+ (and (pair? ts) `(or ,@ts))))
(else #f))))))
(simplify-type tnew)))
@@ -743,14 +744,19 @@
pn var pt (car ctags))
(add-to-blist
var (car ctags)
- (if (and a (type<=? (cdr a) pt)) (cdr a) pt))
+ (cond ((not a) pt)
+ ((typeset-min pt (cdr a)))
+ ((reduce-typeset
+ (cdr a) pt
+ (type-typeenv `(or ,(cdr a) ,pt))))
+ (else pt)))
;; if the variable type is an "or"-type, we can
;; can remove all elements that match the predicate
;; type
(when a
;;XXX hack, again:
(let* ((tenv2 (type-typeenv `(or ,(cdr a) ,pt)))
- (at (reduce-typeset (cdr a) pt tenv2)))
+ (at (reduce-typeset (cdr a) `(not ,pt) tenv2)))
(when at
(d " predicate `~a' indicates `~a' is ~a in flow ~a"
pn var at (cdr ctags))
@@ -763,7 +769,10 @@
t
argr)))
((get db var 'assigned) '*)
- ((type<=? (cdr a) argr) (cdr a))
+ ((typeset-min (cdr a) argr))
+ ((reduce-typeset
+ (cdr a) argr
+ (type-typeenv `(or ,(cdr a) ,argr))))
(else argr))))
(d " assuming: ~a -> ~a (flow: ~a)"
var ar (car flow))
@@ -1376,8 +1385,13 @@
(or (type<=? t1 t2)
(type<=? t2 t1)))
+(define (typeset-min t1 t2)
+ (cond ((type<=? t1 t2) t1)
+ ((type<=? t2 t1) t2)
+ (else #f)))
(define (type<=? t1 t2)
+ ;; NOTE various corner cases require t1 and t2 to have been simplified.
(let* ((typeenv (append-map type-typeenv (list t1 t2)))
(trail0 trail)
(r (let test ((t1 t1) (t2 t2))
@@ -1393,13 +1407,16 @@
(lambda (e)
(cond ((second e) (test t1 (second e)))
(else
- (set-cdr! e t1)
+ (set-car! (cdr e) t1)
(or (not (third e))
(test t1 (third e)))))))
- ((memq t2 '(* undefined)))
+ ((memq t2 '(* undefined)) #t)
+ ((memq t1 '(* undefined)) #f)
((eq? 'pair t1) (test '(pair * *) t2))
((eq? 'vector t1) (test '(vector-of *) t2))
((eq? 'list t1) (test '(list-of *) t2))
+ ((eq? 'boolean t1) (test '(or true false) t2))
+ ((eq? 'number t1) (test '(or fixnum float) t2))
((and (eq? 'null t1)
(pair? t2)
(eq? (car t2) 'list-of)))
@@ -1407,6 +1424,23 @@
(test (third t1) t2))
((and (pair? t2) (eq? 'forall (car t2)))
(test t1 (third t2)))
+ ((and (pair? t1) (eq? 'or (first t1)))
+ (over-all-instantiations
+ (cdr t1)
+ typeenv
+ #t
+ (lambda (t) (test t t2))))
+ ((and (pair? t2) (eq? 'or (first t2)))
+ (over-all-instantiations
+ (cdr t2)
+ typeenv
+ #f
+ (lambda (t) (test t1 t))))
+ ((and (pair? t1) (eq? 'not (first t1)))
+ (and (pair? t2) (eq? 'not (first t2))
+ (test (second t2) (second t1))))
+ ((and (pair? t2) (eq? 'not (first t2)))
+ (not (test t1 (second t2)))) ; sic
(else
(case t2
((procedure) (and (pair? t1) (eq? 'procedure (car t1))))
@@ -1418,12 +1452,6 @@
(else
(cond ((not (pair? t1)) #f)
((not (pair? t2)) #f)
- ((eq? 'or (car t2))
- (over-all-instantiations
- (cdr t2)
- typeenv
- #t
- (lambda (t) (test t1 t))))
((and (eq? 'vector (car t1)) (eq? 'vector-of (car t2)))
(every (cute test <> (second t2)) (cdr t1)))
((and (eq? 'vector-of (car t1)) (eq? 'vector (car t2)))
@@ -1444,12 +1472,6 @@
((not (eq? (car t1) (car t2))) #f)
(else
(case (car t1)
- ((or)
- (over-all-instantiations
- (cdr t1)
- typeenv
- #t
- (lambda (t) (test t t2))))
((vector-of list-of) (test (second t1) (second t2)))
((pair) (every test (cdr t1) (cdr t2)))
((list vector)
@@ -1714,9 +1736,11 @@
((pair list vector vector-of list-of)
(cons (car t) (map (cut resolve <> done) (cdr t))))
((procedure)
- (let* ((argtypes (procedure-arguments t))
+ (let* ((name (procedure-name t))
+ (argtypes (procedure-arguments t))
(rtypes (procedure-results t)))
`(procedure
+ ,@(if name (list name) '())
,(let loop ((args argtypes))
(cond ((null? args) '())
((eq? '#!rest (car args))
diff --git a/tests/scrutiny-tests.scm b/tests/scrutiny-tests.scm
index 3ac754f9..81c7c1a4 100644
--- a/tests/scrutiny-tests.scm
+++ b/tests/scrutiny-tests.scm
@@ -161,3 +161,36 @@
;; multiple-value return syntax
(: mv (-> . *))
(: mv (procedure () . *))
+
+;; procedures from the type environment should still enforce, etc.
+(let ((x (the (or fixnum string) _))
+ (f (the (forall (a)
+ (a -> (-> a)))
+ (lambda (a)
+ (lambda () a)))))
+ (((f +)) x) ; (or fixnum string) -> fixnum
+ (fixnum? x)) ; should report
+
+;; typeset reduction
+
+(: char-or-string? (* -> boolean : (or char string)))
+
+(let ((x _))
+ (if (char-or-string? x)
+ (symbol? x) ; should report with x = (or char string)
+ (string? x))) ; should not report
+
+(let ((x (the fixnum _)))
+ (if (char-or-string? x)
+ (symbol? x) ; should report with x = (or char string)
+ (string? x))) ; should report with x = fixnum
+
+(let ((x (the (or char symbol) _)))
+ (if (char-or-string? x)
+ (symbol? x) ; should report with x = char
+ (string? x))) ; should report with x = symbol
+
+(let ((x (the (or char symbol string) _)))
+ (if (char-or-string? x)
+ (symbol? x) ; should report with x = (or char string)
+ (string? x))) ; should report with x = symbol
diff --git a/tests/scrutiny.expected b/tests/scrutiny.expected
index f9df9f82..2968d691 100644
--- a/tests/scrutiny.expected
+++ b/tests/scrutiny.expected
@@ -34,7 +34,7 @@ Warning: at toplevel:
(scrutiny-tests.scm:25) in procedure call to `+', expected argument #2 of type `number', but was given an argument of type `symbol'
Warning: at toplevel:
- assignment of value of type `fixnum' to toplevel variable `car' does not match declared type `(forall (a158) (procedure car ((pair a158 *)) a158))'
+ assignment of value of type `fixnum' to toplevel variable `car' does not match declared type `(forall (a176) (procedure car ((pair a176 *)) a176))'
Warning: at toplevel:
expected in `let' binding of `g8' a single result, but were given 2 results
@@ -105,4 +105,40 @@ Warning: at toplevel:
Warning: at toplevel:
(scrutiny-tests.scm:159) in procedure call to `apply1', expected argument #2 of type `(list-of number)', but was given an argument of type `(list symbol fixnum fixnum)'
+Note: at toplevel:
+ (scrutiny-tests.scm:172) in procedure call to `fixnum?', the predicate is called with an argument of type
+ `fixnum' and will always return true
+
+Note: at toplevel:
+ (scrutiny-tests.scm:180) in procedure call to `symbol?', the predicate is called with an argument of type
+ `(or char string)' and will always return false
+
+Note: at toplevel:
+ (scrutiny-tests.scm:184) in procedure call to `char-or-string?', the predicate is called with an argument of type
+ `fixnum' and will always return false
+
+Note: at toplevel:
+ (scrutiny-tests.scm:185) in procedure call to `symbol?', the predicate is called with an argument of type
+ `(or char string)' and will always return false
+
+Note: at toplevel:
+ (scrutiny-tests.scm:186) in procedure call to `string?', the predicate is called with an argument of type
+ `fixnum' and will always return false
+
+Note: at toplevel:
+ (scrutiny-tests.scm:190) in procedure call to `symbol?', the predicate is called with an argument of type
+ `char' and will always return false
+
+Note: at toplevel:
+ (scrutiny-tests.scm:191) in procedure call to `string?', the predicate is called with an argument of type
+ `symbol' and will always return false
+
+Note: at toplevel:
+ (scrutiny-tests.scm:195) in procedure call to `symbol?', the predicate is called with an argument of type
+ `(or char string)' and will always return false
+
+Note: at toplevel:
+ (scrutiny-tests.scm:196) in procedure call to `string?', the predicate is called with an argument of type
+ `symbol' and will always return false
+
Warning: redefinition of standard binding: car
diff --git a/types.db b/types.db
index 8614109e..b036928b 100644
--- a/types.db
+++ b/types.db
@@ -1015,7 +1015,7 @@
(port-position (#(procedure #:clean #:enforce) port-position (#!optional port) fixnum fixnum))
-(port? (#(procedure #:pure) port? (*) boolean))
+(port? (#(procedure #:pure #:predicate (or input-port output-port)) port? (*) boolean))
(print (procedure print (#!rest *) undefined))
(print-call-chain (#(procedure #:clean #:enforce) print-call-chain (#!optional output-port fixnum * string) undefined))
@@ -1523,7 +1523,7 @@
(pointer->object (#(procedure #:clean #:enforce) pointer->object (pointer) *)
((pointer) (##core#inline "C_pointer_to_object" #(1))))
-(pointer-like? (#(procedure #:pure) pointer-like? (*) boolean) ;XXX predicate?
+(pointer-like? (#(procedure #:pure #:predicate (or pointer locative procedure port)) pointer-like? (*) boolean)
(((or pointer locative procedure port)) (let ((#(tmp) #(1))) '#t)))
(pointer-f32-ref (#(procedure #:clean #:enforce) pointer-f32-ref (pointer) number))
Trap