suzanne.soy/typed-racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Add a helper function to add filters en masse to express propositions

Browse Source 
that are true about a function's arguments if the function returns.

original commit: bf6379c36346e061031fe2916a1f6aece2367fb1
This commit is contained in:
Vincent St-Amour 2011-02-18 17:35:12 -05:00
parent ddd2dd821b
commit f2c0187b07
2 changed files with 25 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
collects/typed-scheme/private/env-lang.rkt
View File

@ -8,7 +8,7 @@
(r:infer infer)
(only-in (r:infer infer-dummy) infer-param)
(except-in (rep object-rep filter-rep type-rep) make-arr)
(types convenience union)
(types convenience union filter-ops)
(only-in (types convenience) [make-arr* make-arr]))
(define-syntax (-#%module-begin stx)
@ -34,4 +34,4 @@
require
(except-out (all-from-out scheme/base) #%module-begin)
types rep private utils
(types-out convenience union))
(types-out convenience union filter-ops))

23
collects/typed-scheme/types/filter-ops.rkt
View File

@ -162,3 +162,26 @@
(loop (cdr fs) result)]
[else
(loop (cdr fs) (cons t result))])]))))
;; ands the given type filter to both sides of the given arr for each argument
;; useful to express properties of the form: if this function returns at all,
;; we learn this about its arguments (like fx primitives, or car/cdr, etc.)
(define (add-unconditional-filter-all-args arr type)
(match arr
[(Function: (list (arr: dom rng rest drest kws)))
(match rng
[(Values: (list (Result: tp (FilterSet: true-filter
false-filter)
op)))
(let ([new-filters (apply -and (build-list (length dom)
(lambda (i)
(-filter type i))))])
(make-Function
(list (make-arr
dom
(make-Values
(list (-result tp
(-FS (-and true-filter new-filters)
(-and false-filter new-filters))
op)))
rest drest kws))))])]))