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

Fix type restriction in values->tc-results

Browse Source 
Previously the restriction didn't account for traversing
the object type with the given path. This also relies on
the previous commit that adds subtyping on filters.

(because this change seems to introduce filters which
 only differ by an unrolling of a recursive type, but
 the old subtyping only worked for identical types)
This commit is contained in:
Asumu Takikawa 2015-04-01 18:51:40 -04:00
parent 8acc86bb9b
commit c70910aaa0
2 changed files with 25 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
typed-racket-lib/typed-racket/typecheck/tc-subst.rkt
View File

@ -6,7 +6,8 @@
(require "../utils/utils.rkt"
racket/match racket/list
(contract-req)
(except-in (types abbrev utils filter-ops) -> ->* one-of/c)
(except-in (types abbrev utils filter-ops path-type)
-> ->* one-of/c)
(only-in (infer infer) restrict)
(rep type-rep object-rep filter-rep rep-utils))
@ -135,8 +136,15 @@
[(Empty:)
(if polarity -top -bot)]
[_
;; `ty` alone doesn't account for the path, so
;; first traverse it with the path to match `t`
(define ty/path (path-type p ty))
(maker
(restrict ty (subst-type t k o polarity ty))
;; don't restrict if the path doesn't match the type
(if (equal? ty/path Err)
(subst-type t k o polarity ty)
(restrict ty/path
(subst-type t k o polarity ty)))
(-acc-path p o))])]
[(index-free-in? k t) (if polarity -top -bot)]
[else f]))

15
typed-racket-test/unit-tests/metafunction-tests.rkt
View File

@ -151,6 +151,21 @@
(values->tc-results (make-Values (list (-result -Boolean (-FS (-filter -PosReal '(0 0)) (-filter -NonPosReal '(0 0))))))
(list (make-Path null #'x)) (list -Integer))
(ret -Boolean (-FS (-filter -PosInt #'x) (-filter -NonPosInt #'x))))
;; Filter restriction accounts for paths
(check-equal?
(values->tc-results
(make-Values
(list (-result -Boolean
(-FS (make-TypeFilter -PosReal
(make-Path (list -car) '(0 0)))
(make-TypeFilter -NonPosReal
(make-Path (list -car) '(0 0)))))))
(list (make-Path null #'x))
(list (-lst -Integer)))
(ret -Boolean
(-FS (make-TypeFilter -PosInt (make-Path (list -car) #'x))
(make-TypeFilter -NonPosInt (make-Path (list -car) #'x)))))
)
(test-suite "replace-names"