[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Chicken-hackers] [PATCH 3/5] Add basic refinement types
|
From: |
Evan Hanson |
|
Subject: |
[Chicken-hackers] [PATCH 3/5] Add basic refinement types |
|
Date: |
Thu, 30 Jun 2016 20:09:47 +1200 |
Adds a new "refine" type form to the scrutinizer, which allows other
types to be "tagged" with extra information. Applies this approach to
the existing types for input- and output- ports, which are now expressed
as "(refine (input) port)" and "(refine (output) port)", respectively.
Improves the type inference of predicates and enforcing procedures by
descending into container argument types during type reduction, and by
taking already-determined types from the branch list into account.
Other scrutinizer changes:
- Moves repeated lists of type symbols into constants.
- Removes some unnecessary cond/case clauses.
- Removes "##core#global-ref" handling.
- Improves "(not ...)" type matching.
- Removes `type<=?` and reimplements it in terms of the more complete
and correct `match-types` procedure.
---
scrutinizer.scm | 500 ++++++++++++++++++-----------------------
tests/scrutiny-tests.scm | 2 +-
tests/scrutiny.expected | 3 +
tests/specialization-tests.scm | 7 +
tests/specialization.expected | 16 ++
tests/typematch-tests.scm | 27 +++
types.db | 31 +--
7 files changed, 284 insertions(+), 302 deletions(-)
diff --git a/scrutinizer.scm b/scrutinizer.scm
index faaa9d8..94c3b3f 100644
--- a/scrutinizer.scm
+++ b/scrutinizer.scm
@@ -30,7 +30,9 @@
(module chicken.compiler.scrutinizer
(scrutinize load-type-database emit-type-file
- validate-type check-and-validate-type install-specializations)
+ validate-type check-and-validate-type install-specializations
+ ;; Exported for use in the tests:
+ match-types refine-types type<=?)
(import chicken scheme
chicken.compiler.support
@@ -64,27 +66,29 @@
;
; result specifiers:
;
-; SPEC = * | (VAL1 ...)
-; VAL = (or VAL1 ...)
-; | (not VAL)
-; | (struct NAME)
-; | (procedure [NAME] (VAL1 ... [#!optional VALOPT1 ...] [#!rest [VAL |
values]]) . RESULTS)
-; | BASIC
-; | COMPLEX
-; | (forall (TVAR1 ...) VAL)
-; | deprecated
-; | (deprecated NAME)
-; BASIC = * | string | symbol | char | number | boolean | true | false |
list | pair |
-; procedure | vector | null | eof | undefined | input-port |
output-port |
-; blob | noreturn | pointer | locative | fixnum | float | bignum |
-; ratnum | compnum | integer | pointer-vector
-; COMPLEX = (pair VAL VAL)
-; | (vector-of VAL)
-; | (list-of VAL)
-; | (vector VAL1 ...)
-; | (list VAL1 ...)
-; RESULTS = *
-; | (VAL1 ...)
+; SPEC = * | (TYPE1 ...)
+; TYPE = (or TYPE1 ...)
+; | (not TYPE)
+; | (struct NAME)
+; | (procedure [NAME] (TYPE1 ... [#!optional TYPE1 ...] [#!rest [TYPE |
values]]) . RESULTS)
+; | VALUE
+; | BASIC
+; | COMPLEX
+; | (forall (TVAR1 ...) TYPE)
+; | (refine (SYMBOL ...) VALUE)
+; | deprecated
+; | (deprecated NAME)
+; VALUE = string | symbol | char | number | boolean | true | false |
+; null | eof | blob | pointer | port | locative | fixnum |
+; float | bignum | ratnum | cplxnum | integer | pointer-vector
+; BASIC = * | list | pair | procedure | vector | undefined | noreturn |
values
+; COMPLEX = (pair TYPE TYPE)
+; | (vector-of TYPE)
+; | (list-of TYPE)
+; | (vector TYPE1 ...)
+; | (list TYPE1 ...)
+; RESULTS = *
+; | (TYPE1 ...)
; TVAR = (VAR TYPE) | VAR
;
; global symbol properties:
@@ -101,7 +105,7 @@
;
; specialization specifiers:
;
-; SPECIALIZATION = ((VAL ... [#!rest VAL]) [RESULTS] TEMPLATE)
+; SPECIALIZATION = ((TYPE ... [#!rest TYPE]) [RESULTS] TEMPLATE)
; TEMPLATE = #(INDEX)
; | #(INDEX ...)
; | #(SYMBOL)
@@ -118,7 +122,29 @@
(define-constant +maximal-union-type-length+ 20)
(define-constant +maximal-complex-object-constructor-result-type-length+ 256)
-(define-inline (unrename-type x) (strip-syntax x))
+(define-constant value-types
+ '(string symbol char null boolean true false blob eof fixnum float number
+ integer bignum ratnum cplxnum pointer-vector port pointer locative))
+
+(define-constant basic-types
+ '(* list pair procedure vector undefined deprecated noreturn values))
+
+(define-constant struct-types
+ '(u8vector s8vector u16vector s16vector u32vector s32vector u64vector
+ s64vector f32vector f64vector thread queue environment time
+ continuation lock mmap condition hash-table tcp-listener))
+
+(define-inline (struct-type? t)
+ (and (pair? t) (eq? (car t) 'struct)))
+
+(define-inline (value-type? t)
+ (or (struct-type? t) (memq t value-types)))
+
+(define (type-name x)
+ (let ((t (strip-syntax x)))
+ (if (refinement-type? t)
+ (sprintf "~a-~a" (string-intersperse (map conc (second t)) "/") (third
t))
+ (sprintf "~a" t))))
(define specialization-statistics '())
(define trail '())
@@ -213,6 +239,7 @@
(cond ((pair? t)
(case (car t)
((or) (every always-true1 (cdr t)))
+ ((not) (not (always-true1 (second t))))
((forall) (always-true1 (third t)))
(else #t)))
((memq t '(* boolean false undefined noreturn)) #f)
@@ -255,13 +282,13 @@
(when complain
(##sys#notice
(conc (location-name loc)
- (sprintf "~?" msg (map unrename-type args))))))
+ (sprintf "~?" msg (map type-name args))))))
(define (report loc msg . args)
(when complain
(warning
(conc (location-name loc)
- (sprintf "~?" msg (map unrename-type args))))))
+ (sprintf "~?" msg (map type-name args))))))
(define (report-error loc msg . args)
(set! errors #t)
@@ -439,7 +466,7 @@
(define (add-to-blist var flow type)
(let loop ((var var))
- (set! blist (alist-cons (cons var flow) type blist))
+ (set! blist (alist-update! (cons var flow) type blist equal?))
(let ((a (assq var aliased)))
(when a
(d " applying to alias: ~a -> ~a" (cdr a) type)
@@ -456,20 +483,6 @@
(make-list argc '*)))
(make-list argc '*)))
- (define (reduce-typeset t pt typeenv)
- (and-let* ((tnew
- (let rec ((t t))
- (and (pair? t)
- (case (car t)
- ((forall)
- (and-let* ((t2 (rec (third t))))
- `(forall ,(second t) ,t2)))
- ((or)
- (let ((ts (filter (cut match-types <> pt typeenv)
(cdr t))))
- (and (pair? ts) `(or ,@ts))))
- (else #f))))))
- (simplify-type tnew)))
-
(define (walk n e loc dest tail flow ctags) ; returns result specifier
(let ((subs (node-subexpressions n))
(params (node-parameters n))
@@ -485,7 +498,6 @@
((quote) (list (constant-result (first params))))
((##core#undefined) '(*))
((##core#proc) '(procedure))
- ((##core#global-ref) (global-result (first params) loc))
((##core#variable) (variable-result (first params) e loc flow))
((if)
(let ((tags (cons (tag) (tag)))
@@ -734,7 +746,7 @@
(lambda (arg argr)
(when (eq? '##core#variable (node-class arg))
(let* ((var (first (node-parameters arg)))
- (a (assq var e))
+ (a (or (blist-type var flow)
(alist-ref var e)))
(argr (resolve argr typeenv))
(oparg? (eq? arg (first subs)))
(pred (and pt
@@ -747,38 +759,24 @@
(let ((pt (resolve pt typeenv)))
(d " predicate `~a' indicates
`~a' is ~a in flow ~a"
pn var pt (car ctags))
- (add-to-blist
+ (add-to-blist
var (car ctags)
- (cond ((not a) pt)
- ((typeset-min pt (cdr a)))
- ((reduce-typeset
- (cdr a) pt
- (type-typeenv `(or ,(cdr
a) ,pt))))
- (else pt)))
+ (if (not a) pt (refine-types a
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) `(not ,pt) tenv2)))
+ (let ((at (refine-types a `(not
,pt))))
(when at
(d " predicate `~a'
indicates `~a' is ~a in flow ~a"
pn var at (cdr ctags))
(add-to-blist var (cdr
ctags) at))))))
(a
(when enforces
- (let ((ar (cond ((blist-type var
flow) =>
- (lambda (t)
- (if (type<=? t
argr)
- t
- argr)))
- ((db-get db var
'assigned) '*)
- ((typeset-min (cdr
a) argr))
- ((reduce-typeset
- (cdr a) argr
- (type-typeenv
`(or ,(cdr a) ,argr))))
- (else argr))))
+ (let ((ar (if (db-get db var
'assigned)
+ '* ; XXX necessary?
+ (refine-types a
argr))))
(d " assuming: ~a -> ~a (flow:
~a)"
var ar (car flow))
(add-to-blist var (car flow) ar)
@@ -833,12 +831,12 @@
(let loop ((types (cdr params)) (subs (cdr subs)))
(cond ((null? types)
(quit-compiling
- "~a~ano clause applies in `compiler-typecase' for
expression of type `~s':~a"
+ "~a~ano clause applies in `compiler-typecase' for
expression of type `~a':~a"
(location-name loc)
(node-source-prefix n)
- (car ts)
+ (type-name (car ts))
(string-intersperse
- (map (lambda (t) (sprintf "\n ~a" t))
+ (map (lambda (t) (sprintf "\n ~a" (type-name
t)))
(cdr params)) "")))
((match-types (car types) (car ts)
(append (type-typeenv (car types))
typeenv)
@@ -910,7 +908,7 @@
;
; - "all" means: all elements in `or'-types in second argument must match
-(define (match-types t1 t2 typeenv #!optional all)
+(define (match-types t1 t2 #!optional (typeenv (type-typeenv `(or ,t1 ,t2)))
all)
(define (match-args args1 args2)
(d "match args: ~s <-> ~s" args1 args2)
@@ -1012,17 +1010,33 @@
((eq? t2 '*) (not all))
((eq? t1 'undefined) #f)
((eq? t2 'undefined) #f)
+ ((eq? t1 'noreturn))
+ ((eq? t2 'noreturn))
+ ((eq? t1 'boolean) (match1 '(or true false) t2))
+ ((eq? t2 'boolean) (match1 t1 '(or true false)))
+ ((eq? t1 'integer) (match1 '(or fixnum bignum) t2))
+ ((eq? t2 'integer) (match1 t1 '(or fixnum bignum)))
+ ((eq? t1 'number) (match1 '(or fixnum float bignum ratnum cplxnum)
t2))
+ ((eq? t2 'number) (match1 t1 '(or fixnum float bignum ratnum
cplxnum)))
+ ((eq? t1 'pair) (match1 '(pair * *) t2))
+ ((eq? t2 'pair) (match1 t1 '(pair * *)))
+ ((eq? t1 'list) (match1 '(list-of *) t2))
+ ((eq? t2 'list) (match1 t1 '(list-of *)))
+ ((eq? t1 'vector) (match1 '(vector-of *) t2))
+ ((eq? t2 'vector) (match1 t1 '(vector-of *)))
((and (pair? t1) (eq? 'not (car t1)))
- (let* ((trail0 trail)
- (m (rawmatch1 (cadr t1) t2)))
- (trail-restore trail0 typeenv)
- (not m)))
+ (fluid-let ((all (not all)))
+ (let* ((trail0 trail)
+ (m (match1 (cadr t1) t2)))
+ (trail-restore trail0 typeenv)
+ (not m))))
((and (pair? t2) (eq? 'not (car t2)))
(and (not all)
- (let* ((trail0 trail)
- (m (match1 t1 (cadr t2))))
- (trail-restore trail0 typeenv)
- (not m))))
+ (fluid-let ((all #t))
+ (let* ((trail0 trail)
+ (m (match1 (cadr t2) t1)))
+ (trail-restore trail0 typeenv)
+ (not m)))))
;; this is subtle: "or" types for t2 are less restrictive,
;; so we handle them before "or" types for t1
((and (pair? t2) (eq? 'or (car t2)))
@@ -1042,20 +1056,6 @@
(match1 (third t1) t2)) ; assumes typeenv has already been extracted
((and (pair? t2) (eq? 'forall (car t2)))
(match1 t1 (third t2))) ; assumes typeenv has already been extracted
- ((eq? t1 'noreturn))
- ((eq? t2 'noreturn))
- ((eq? t1 'boolean) (match1 '(or true false) t2))
- ((eq? t2 'boolean) (match1 t1 '(or true false)))
- ((eq? t1 'integer) (match1 '(or fixnum bignum) t2))
- ((eq? t2 'integer) (match1 t1 '(or fixnum bignum)))
- ((eq? t1 'number) (match1 '(or fixnum float bignum ratnum cplxnum)
t2))
- ((eq? t2 'number) (match1 t1 '(or fixnum float bignum ratnum
cplxnum)))
- ((eq? t1 'pair) (match1 '(pair * *) t2))
- ((eq? t2 'pair) (match1 t1 '(pair * *)))
- ((eq? t1 'list) (match1 '(list-of *) t2))
- ((eq? t2 'list) (match1 t1 '(list-of *)))
- ((eq? t1 'vector) (match1 '(vector-of *) t2))
- ((eq? t2 'vector) (match1 t1 '(vector-of *)))
((eq? 'procedure t1)
(and (pair? t2) (eq? 'procedure (car t2))))
((eq? 'procedure t2)
@@ -1081,7 +1081,15 @@
((list vector)
(and (= (length t1) (length t2))
(every-match1 (cdr t1) (cdr t2))))
- (else #f) ) )
+ ((refine)
+ (and (match1 (third t1) (third t2))
+ (or (not all)
+ (lset<=/eq? (second t1) (second t2)))))
+ (else #f)))
+ ((and (pair? t1) (eq? 'refine (car t1)))
+ (and (not all) (match1 (third t1) t2)))
+ ((and (pair? t2) (eq? 'refine (car t2)))
+ (match1 t1 (third t2)))
((and (pair? t1) (eq? 'pair (car t1)))
(and (pair? t2)
(case (car t2)
@@ -1144,10 +1152,9 @@
(cute match1 (second t1) <>))))
(else #f)))
+ (dd "match (~a) ~a <-> ~a" (if all "all" "any") t1 t2)
(let ((m (match1 t1 t2)))
- (dd " match~a ~a <-> ~a -> ~a te: ~s"
- (if all " (all)" "")
- t1 t2 m typeenv)
+ (dd "match (~a) ~s <-> ~s -> ~s" (if all "all" "any") t1 t2 m)
m))
@@ -1254,12 +1261,18 @@
((any (cut type<=? (car ts) <>)
done)
(loop (cdr ts) done))
(else (loop (cdr ts) (cons (car
ts) done)))))))
- (cond ((equal? ts2 (cdr t)) t)
- (else
- (dd " or-simplify: ~a" ts2)
- (simplify
- `(or ,@(if (any (cut eq? <> '*) ts2) '(*)
ts2)))))))) ))
- ((pair)
+ (if (equal? ts2 (cdr t))
+ t
+ (simplify `(or ,@ts2))))))))
+ ((refine)
+ (let ((rs (second t))
+ (t2 (simplify (third t))))
+ (cond ((null? rs) t2)
+ ((refinement-type? t2)
+ (list 'refine (lset-union/eq? (second t2) rs)
(third t2)))
+ (else
+ (list 'refine (delete-duplicates rs eq?) t2)))))
+ ((pair)
(let ((tcar (simplify (second t)))
(tcdr (simplify (third t))))
(if (and (eq? '* tcar) (eq? '* tcdr))
@@ -1271,7 +1284,7 @@
(if (eq? t2 '*)
'vector
`(,(car t) ,t2))))
- ((vector-of list-of)
+ ((list-of)
(let ((t2 (simplify (second t))))
(if (eq? t2 '*)
'list
@@ -1314,6 +1327,19 @@
(dd "simplify: ~a -> ~a" t t2)
t2)))
+(define (expand-type t)
+ (case t
+ ((pair) '(pair * *))
+ ((list) '(list-of *))
+ ((vector) '(vector-of *))
+ ((boolean) '(or true false))
+ ((integer) '(or fixnum bignum))
+ ((number) '(or fixnum float bignum ratnum cplxnum))
+ ((procedure) '(procedure (#!rest *) . *))
+ (else t)))
+
+
+;;; Merging types
(define (merge-argument-types ts1 ts2)
;; this could be more elegantly done by combining non-matching
arguments/llists
@@ -1354,168 +1380,60 @@
(loop (cdr ts1) (cdr ts2)))))))))
-(define (compatible-types? t1 t2)
- (or (type<=? t1 t2)
- (type<=? t2 t1)))
+(define (compatible-types? t1 t2 #!optional (te (type-typeenv `(or ,t1 ,t2))))
+ (or (type<=? t1 t2 te)
+ (type<=? t2 t1 te)))
-(define (typeset-min t1 t2)
- (cond ((type<=? t1 t2) t1)
- ((type<=? t2 t1) t2)
+(define (type-min t1 t2 #!optional (te (type-typeenv `(or ,t1 ,t2))))
+ (cond ((type<=? t1 t2 te) t1)
+ ((type<=? t2 t1 te) 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))
- (cond ((eq? t1 t2))
- ((and (symbol? t1) (assq t1 typeenv)) =>
- (lambda (e)
- (cond ((second e) (test (second e) t2))
- (else
- (set-car! (cdr e) t2)
- (or (not (third e))
- (test (third e) t2))))))
- ((and (symbol? t2) (assq t2 typeenv)) =>
- (lambda (e)
- (cond ((second e) (test t1 (second e)))
- (else
- (set-car! (cdr e) t1)
- (or (not (third e))
- (test t1 (third e)))))))
- ((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? 'integer t1) (test '(or fixnum bignum) t2))
- ((eq? 'number t1) (test '(or fixnum float bignum ratnum
cplxnum) t2))
- ((and (eq? 'null t1)
- (pair? t2)
- (eq? (car t2) 'list-of)))
- ((and (pair? t1) (eq? 'forall (car t1)))
- (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))))
- ((boolean) (memq t1 '(true false)))
- ((integer) (memq t1 '(fixnum bignum)))
- ((number) (memq t1 '(fixnum float bignum ratnum
cplxnum)))
- ((vector) (test t1 '(vector-of *)))
- ((list) (test t1 '(list-of *)))
- ((pair) (test t1 '(pair * *)))
- (else
- (cond ((not (pair? t1)) #f)
- ((not (pair? t2)) #f)
- ((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)))
- (every (cute test (second t1) <>) (cdr t2)))
- ((and (eq? 'list (car t1)) (eq? 'list-of (car
t2)))
- (every (cute test <> (second t2)) (cdr t1)))
- ((and (eq? 'list (car t1)) (eq? 'pair (car t2)))
- (and (not (null? (cdr t1)))
- (test (second t1) (second t2))
- (test t1 (third t2))))
- ((and (eq? 'pair (car t1)) (eq? 'list (car t2)))
- (and (not (null? (cdr t2)))
- (test (second t1) (second t2))
- (test (third t1) t2)))
- ((and (eq? 'pair (car t1)) (eq? 'list-of (car
t2)))
- (and (test (second t1) (second t2))
- (test (third t1) t2)))
- ((not (eq? (car t1) (car t2))) #f)
- (else
- (case (car t1)
- ((vector-of list-of) (test (second t1) (second
t2)))
- ((pair)
- (and (test (second t1) (second t2))
- (test (third t1) (third t2))))
- ((list vector)
- (and (= (length t1) (length t2))
- (let loop ((lst1 (cdr t1)) (lst2 (cdr
t2)))
- (or (null? lst1)
- (and (test (car lst1) (car lst2))
- (loop (cdr lst1) (cdr
lst2)))))))
- ((struct) (eq? (cadr t1) (cadr t2)))
- ((procedure)
- (let ((args1 (if (named? t1) (caddr t1) (cadr
t1)))
- (args2 (if (named? t2) (caddr t2) (cadr
t2)))
- (res1 (if (named? t1) (cdddr t1) (cddr
t1)))
- (res2 (if (named? t2) (cdddr t2) (cddr
t2))) )
- (let loop1 ((args1 args1)
- (args2 args2)
- (rtype1 #f)
- (rtype2 #f)
- (m1 0)
- (m2 0))
- (cond ((null? args1)
- (and (cond ((null? args2)
- (if rtype1
- (if rtype2
- (test rtype1
rtype2)
- #f)
- #t))
- ((eq? '#!optional (car
args2))
- (not rtype1))
- ((eq? '#!rest (car
args2))
- (or (null? (cdr args2))
- rtype1
- (test rtype1 (cadr
args2))))
- (else (>= m2 m1)))
- (let loop2 ((res1 res1) (res2
res2))
- (cond ((eq? '* res2) #t)
- ((null? res2) (null?
res1))
- ((eq? '* res1) #f)
- ((test (car res1)
(car res2))
- (loop2 (cdr res1)
(cdr res2)))
- (else #f)))))
- ((eq? (car args1) '#!optional)
- (loop1 (cdr args1) args2 #f rtype2
1 m2))
- ((eq? (car args1) '#!rest)
- (if (null? (cdr args1))
- (loop1 '() args2 '* rtype2 2
m2)
- (loop1 '() args2 (cadr args1)
rtype2 2 m2)))
- ((null? args2)
- (and rtype2
- (test (car args1) rtype2)
- (loop1 (cdr args1) '() rtype1
rtype2 m1 m2)))
- ((eq? (car args2) '#!optional)
- (loop1 args1 (cdr args2) rtype1 #f
m1 1))
- ((eq? (car args2) '#!rest)
- (if (null? (cdr args2))
- (loop1 args1 '() rtype1 '* m1
2)
- (loop1 args1 '() rtype1 (cadr
args2) m1 2)))
- ((test
- (or rtype1 (car args1))
- (or rtype2 (car args2)))
- (loop1 (cdr args1) (cdr args2)
rtype1 rtype2 m1 m2))
- (else #f)))))
- (else #f)))))))))))
- (set! trail trail0)
- ;;(dd "type<=?: ~s <-> ~s -> ~s" t1 t2 r)
- r))
+(define (type<=? t1 t2 #!optional (te (type-typeenv `(or ,t1 ,t2))))
+ (with-trail-restore
+ te
+ (lambda ()
+ (match-types t2 t1 te #t))))
+
+;;
+;; Combines the information in `t1' and `t2' to produce a smaller type,
+;; with a preference for `t2' if no smaller type can be determined.
+;; Merges refinements at each step.
+;;
+(define (refine-types t1 t2)
+
+ (define (refine t1 t2 te)
+ (let loop ((t1 t1) (t2 t2))
+ (cond
+ ((and (symbol? t1) (memq t1 '(pair list vector boolean integer number)))
+ (loop (expand-type t1) t2))
+ ((and (symbol? t2) (memq t2 '(pair list vector boolean integer number)))
+ (loop t1 (expand-type t2)))
+ ((and (pair? t1) (memq (car t1) '(forall refine)))
+ (let ((t1* (loop (third t1) t2)))
+ (and t1* (list (car t1) (second t1) t1*))))
+ ((and (pair? t2) (memq (car t2) '(forall refine)))
+ (let ((t2* (loop t1 (third t2))))
+ (and t2* (list (car t2) (second 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))))
+ ((and (pair? t1)
+ (memq (car t1) '(pair list vector vector-of list-of))
+ (pair? t2)
+ (eq? (car t1) (car t2))
+ (eq? (length t1) (length t2)))
+ (let ((ts (map loop (cdr t1) (cdr t2))))
+ (and (every identity ts) (cons (car t1) ts))))
+ (else
+ (type-min t1 t2 te)))))
+
+ (let* ((te (type-typeenv `(or ,t1 ,t2)))
+ (rt (or (refine t1 t2 te) t2)))
+ (if (eq? rt t2)
+ rt
+ (simplify-type rt))))
;;; various operations on procedure types
@@ -1655,6 +1573,14 @@
((forall) (noreturn-type? (third t)))
(else #f)))))
+;;; Refinement type helpers
+
+(define (refinement-type? t)
+ (and (pair? t)
+ (case (first t)
+ ((refine) #t)
+ ((forall) (refinement-type? (third t)))
+ (else #f))))
;;; Type-environments and -variables
@@ -1663,7 +1589,9 @@
(let loop ((t t))
(when (pair? t)
(case (car t)
- ((procedure)
+ ((refine)
+ (loop (third t)))
+ ((procedure)
(cond ((or (string? (second t)) (symbol? (second t)))
(for-each loop (third t))
(when (pair? (cdddr t))
@@ -1680,7 +1608,7 @@
(second t))
te))
(loop (third t)))
- ((or and)
+ ((or)
(for-each loop (cdr t))))))
te))
@@ -1690,6 +1618,12 @@
(let ((a (assq (car tr2) typeenv)))
(set-car! (cdr a) #f))))
+(define (with-trail-restore typeenv thunk)
+ (let* ((trail0 trail)
+ (result (thunk)))
+ (trail-restore trail0 typeenv)
+ result))
+
(define (resolve t typeenv)
(simplify-type ;XXX do only when necessary
(let resolve ((t t) (done '()))
@@ -1703,19 +1637,16 @@
'*)
(resolve t2 (cons t done))))))
((not (pair? t))
- (if (memq t '(* eof char string symbol
- fixnum float bignum ratnum cplxnum
- number integer list vector pair undefined blob
- input-port output-port pointer locative boolean
- true false pointer-vector null procedure noreturn))
+ (if (or (memq t value-types) (memq t basic-types))
t
(bomb "resolve: can't resolve unknown type-variable" t)))
(else
(case (car t)
((or) `(or ,@(map (cut resolve <> done) (cdr t))))
((not) `(not ,(resolve (second t) done)))
- ((forall) `(forall ,(second t) ,(resolve (third t) done)))
- ((pair list vector vector-of list-of)
+ ((forall refine)
+ (list (car t) (second t) (resolve (third t) done)))
+ ((pair list vector vector-of list-of)
(cons (car t) (map (cut resolve <> done) (cdr t))))
((procedure)
(let* ((name (procedure-name t))
@@ -1792,7 +1723,7 @@
(warning
(sprintf "invalid type specification for `~a': ~a"
name
- (unrename-type new))))
+ (type-name new))))
(when (and old (not (compatible-types? old t)))
(warning
(sprintf
@@ -1800,7 +1731,7 @@
conflicts with previously loaded type:\
~n New type: ~a\
~n Original type: ~a"
- name (unrename-type old) (unrename-type new))))
+ name (type-name old) (type-name new))))
(mark-variable name '##compiler#type t)
(mark-variable name '##compiler#type-source 'db)
(when specs
@@ -1966,22 +1897,14 @@
(l2 (validate-llist (cdr llist))))
(and l1 l2 (cons l1 l2))))))
(define (validate t #!optional (rec #t))
- (cond ((memq t '(* string symbol char number boolean true false list pair
- procedure vector null eof undefined input-port
output-port
- blob pointer locative fixnum float integer bignum
ratnum cplxnum pointer-vector
- deprecated noreturn values))
- t)
- ((memq t '(u8vector s8vector u16vector s16vector u32vector s32vector
- u64vector s64vector f32vector f64vector
- thread queue environment time continuation
- lock mmap condition hash-table tcp-listener))
- `(struct ,t))
- ((eq? t 'immediate)
- '(or eof null fixnum char boolean))
- ((eq? t 'port)
- '(or input-port output-port))
+ (cond ((memq t value-types) t)
+ ((memq t basic-types) t)
+ ((memq t struct-types) `(struct ,t))
+ ((eq? t 'immediate) '(or eof null fixnum char boolean))
((eq? t 'any) '*)
((eq? t 'void) 'undefined)
+ ((eq? t 'input-port) '(refine (input) port))
+ ((eq? t 'output-port) '(refine (output) port))
((and (symbol? t) (##sys#get t '##compiler#type-abbreviation)))
((not (pair? t))
(cond ((memq t typevars) t)
@@ -2021,11 +1944,16 @@
(and (every identity ts)
`(or ,@ts)))))
((eq? 'struct (car t))
- (and (= 2 (length t))
- (symbol? (cadr t))
- t))
+ (and (= 2 (length t)) (symbol? (second t)) t))
((eq? 'deprecated (car t))
(and (= 2 (length t)) (symbol? (second t)) t))
+ ((eq? 'refine (car t))
+ (and (= 3 (length t))
+ (let ((t2 (validate (third t))))
+ (and (value-type? t2)
+ (list? (second t))
+ (every symbol? (second t))
+ (list 'refine (second t) t2)))))
((or (memq* '--> t) (memq* '-> t)) =>
(lambda (p)
(let* ((cleanf (eq? '--> (car p)))
diff --git a/tests/scrutiny-tests.scm b/tests/scrutiny-tests.scm
index 9413f07..5097287 100644
--- a/tests/scrutiny-tests.scm
+++ b/tests/scrutiny-tests.scm
@@ -182,7 +182,7 @@
(let ((x _))
(if (char-or-string? x)
(symbol? x) ; should report with x = (or char string)
- (string? x))) ; should not report
+ (string? x))) ; should report with x = (not (or char string))
(let ((x (the fixnum _)))
(if (char-or-string? x)
diff --git a/tests/scrutiny.expected b/tests/scrutiny.expected
index babb71f..3838f73 100644
--- a/tests/scrutiny.expected
+++ b/tests/scrutiny.expected
@@ -114,6 +114,9 @@ Note: at toplevel:
(scrutiny-tests.scm:184) 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:185) in procedure call to `string?', the predicate is
called with an argument of type `(not (or char string))' and will always return
false
+
+Note: at toplevel:
(scrutiny-tests.scm:188) 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:
diff --git a/tests/specialization-tests.scm b/tests/specialization-tests.scm
index 667b65c..0183216 100644
--- a/tests/specialization-tests.scm
+++ b/tests/specialization-tests.scm
@@ -2,3 +2,10 @@
(let ((a "yep")) (if (string? a) 'ok 'no))
(let ((a 'nope)) (if (string? a) 'ok 'no))
+
+;; bidirectional ports are specialized
+
+(let ((p (open-input-string "foo")))
+ (when (output-port? p) ; indicates `p' is bidirectional
+ (if (input-port? p) 'ok 'no)
+ (if (output-port? p) 'ok 'no)))
diff --git a/tests/specialization.expected b/tests/specialization.expected
index 9ae2fc5..8b47dcc 100644
--- a/tests/specialization.expected
+++ b/tests/specialization.expected
@@ -14,3 +14,19 @@ Note: at toplevel:
(specialization-tests.scm:4) in conditional, test expression will always
return false:
(if (string? a) 'ok 'no)
+
+Note: at toplevel:
+ (specialization-tests.scm:10) in procedure call to `input-port?', the
predicate is called with an argument of type `input/output-port' and will
always return true
+
+Note: at toplevel:
+ (specialization-tests.scm:10) expected a value of type boolean in
conditional, but was given a value of type `true' which is always true:
+
+(if (input-port? p) 'ok 'no)
+
+Note: at toplevel:
+ (specialization-tests.scm:11) in procedure call to `output-port?', the
predicate is called with an argument of type `input/output-port' and will
always return true
+
+Note: at toplevel:
+ (specialization-tests.scm:11) expected a value of type boolean in
conditional, but was given a value of type `true' which is always true:
+
+(if (output-port? p) 'ok 'no)
diff --git a/tests/typematch-tests.scm b/tests/typematch-tests.scm
index 83db2d0..26d36d8 100644
--- a/tests/typematch-tests.scm
+++ b/tests/typematch-tests.scm
@@ -129,6 +129,7 @@
(check + 1.2 procedure)
(check '#(1) 1.2 vector)
(check '() 1 null)
+(check (current-input-port) 1.2 port)
(check (current-input-port) 1.2 input-port)
(check (make-blob 10) 1.2 blob)
(check (address->pointer 0) 1.2 pointer)
@@ -184,7 +185,9 @@
(checkp condition? (##sys#make-structure 'condition) (struct condition))
(checkp fixnum? 1 fixnum)
(checkp flonum? 1.2 float)
+(checkp port? (current-input-port) port)
(checkp input-port? (current-input-port) input-port)
+(checkp output-port? (current-output-port) output-port)
(checkp pointer-vector? (make-pointer-vector 1) pointer-vector)
(checkp pointer? (address->pointer 1) pointer)
@@ -196,6 +199,16 @@
(type> list (list *))
(type> vector (vector *))
+(define-type x (struct x))
+
+(type<= (refine (a) x) x)
+(type<= (refine (a b) x) (refine (a) x))
+(type<= (refine (a) false) (refine (a) boolean))
+
+(type> (refine (a) x) (refine (b) x))
+(type> (refine (a) x) (refine (a b) x))
+(type> (refine (a) boolean) (refine (a) false))
+
(mn pair null)
(mn pair list)
@@ -206,6 +219,11 @@
(mx (forall (a) (procedure (#!rest a) a)) +)
(mx (list fixnum) '(1))
+(mx port (open-input-string "foo"))
+(mx input-port (open-input-string "bar"))
+(mx port (open-output-string))
+(mx output-port (open-output-string))
+
;;; pairs
(: car-alike (forall (a) ((pair a *) -> a)))
@@ -339,6 +357,15 @@
(fixnum 'ok))
(assert
+ (eq? 'ok (compiler-typecase (the port xxx)
+ ((not port) 'no)
+ ((not input-port) 'no)
+ ((not output-port) 'no)
+ (input-port 'no)
+ (output-port 'no)
+ (port 'ok))))
+
+(assert
(eq? 'ok (compiler-typecase (f4 1)
(fixnum 'not-ok)
(else 'ok))))
diff --git a/types.db b/types.db
index 259f191..3c3932c 100644
--- a/types.db
+++ b/types.db
@@ -729,22 +729,24 @@
(call-with-current-continuation
(#(procedure #:enforce) call-with-current-continuation ((procedure
(procedure) . *)) . *))
-(input-port? (#(procedure #:pure #:predicate input-port) input-port? (*)
boolean))
-(output-port? (#(procedure #:pure #:predicate output-port) output-port? (*)
boolean))
+(input-port? (#(procedure #:pure #:predicate (refine (input) port))
input-port? (*) boolean))
+(output-port? (#(procedure #:pure #:predicate (refine (output) port))
output-port? (*) boolean))
(current-input-port
(#(procedure #:clean #:enforce) current-input-port (#!optional input-port
boolean boolean) input-port)
- ((input-port) (let ((#(tmp1) #(1)))
- (let ((#(tmp2) (set! ##sys#standard-input #(tmp1))))
- #(tmp1))))
- (() ##sys#standard-input))
+ (() ##sys#standard-input)
+ (((refine (input) port))
+ (let ((#(tmp1) #(1)))
+ (let ((#(tmp2) (set! ##sys#standard-input #(tmp1))))
+ #(tmp1)))))
(current-output-port
(#(procedure #:clean #:enforce) current-output-port (#!optional output-port
boolean boolean) output-port)
- ((output-port) (let ((#(tmp1) #(1)))
- (let ((#(tmp2) (set! ##sys#standard-output #(tmp1))))
- #(tmp1))))
- (() ##sys#standard-output))
+ (() ##sys#standard-output)
+ (((refine (output) port))
+ (let ((#(tmp1) #(1)))
+ (let ((#(tmp2) (set! ##sys#standard-output #(tmp1))))
+ #(tmp1)))))
(call-with-input-file
(procedure call-with-input-file (string (procedure (input-port) . *)
#!rest) . *))
@@ -1251,7 +1253,7 @@
(port-position (#(procedure #:clean #:enforce) port-position (#!optional port)
fixnum fixnum))
-(port? (#(procedure #:pure #:predicate (or input-port output-port)) port? (*)
boolean))
+(port? (#(procedure #:pure #:predicate port) port? (*) boolean))
(port-closed? (#(procedure #:clean #:enforce) port-closed? (port) boolean)
((port) (eq? (##sys#slot #(1) '8) '0)))
@@ -1399,10 +1401,9 @@
((procedure *) (let ((#(tmp) #(1))) '#t)))
(##sys#check-port
- (#(procedure #:clean #:enforce) ##sys#check-port ((or input-port output-port)
#!optional *)
- *)
- (((or input-port output-port)) (let ((#(tmp) #(1))) '#t))
- (((or input-port output-port) *) (let ((#(tmp) #(1))) '#t)))
+ (#(procedure #:clean #:enforce) ##sys#check-port ((or input-port output-port)
#!optional *) *)
+ (((or (refine (input) port) (refine (output) port))) (let ((#(tmp) #(1)))
'#t))
+ (((or (refine (input) port) (refine (output) port)) *) (let ((#(tmp) #(1)))
'#t)))
(##sys#check-input-port
(#(procedure #:clean #:enforce) ##sys#check-input-port (input-port *
#!optional *) *)
--
2.1.4
- [Chicken-hackers] [PATCH 0/5][5] Generalize port directionality and add basic refinement types, Evan Hanson, 2016/06/30
- [Chicken-hackers] [PATCH 2/5] Add input-port-open? and output-port-open? procedures, Evan Hanson, 2016/06/30
- [Chicken-hackers] [PATCH 5/5] Add new `make-bidirectional-port` procedure to ports unit, Evan Hanson, 2016/06/30
- [Chicken-hackers] [PATCH 3/5] Add basic refinement types,
Evan Hanson <=
- [Chicken-hackers] [PATCH 1/5] Generalize port directionality, Evan Hanson, 2016/06/30
- [Chicken-hackers] [PATCH 4/5] Add scrutinizer test suite, Evan Hanson, 2016/06/30
- Re: [Chicken-hackers] [PATCH 4/5] Add scrutinizer test suite, felix . winkelmann, 2016/06/30
- [Chicken-hackers] [PATCH] Nicer port direction error messages, Evan Hanson, 2016/06/30