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

Fix subtyping, printing, inference for refinement types.

Browse Source 
svn: r14403
This commit is contained in:
Sam Tobin-Hochstadt 2009-04-02 03:03:44 +00:00
parent 810035ff52
commit 6d07cf9128
3 changed files with 9 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
collects/typed-scheme/infer/infer-unit.ss
View File

@ -255,6 +255,9 @@
[(a a) empty]
[(_ (Univ:)) empty]
[((Refinement: S _ _) T)
(cg S T)]
[((F: (? (lambda (e) (memq e X)) v)) S)
(when (match S
[(F: v*)

8
collects/typed-scheme/private/subtype.ss
View File

@ -220,6 +220,9 @@
(unmatch))
;(printf "Poly: ~n~a ~n~a~n" b1 (subst-all (map list ms (map make-F ns)) b2))
(subtype* A0 b1 (subst-all (map list ms (map make-F ns)) b2))]
;; A refinement is a subtype of its parent
[(list (Refinement: par _ _) t)
(subtype* A0 par t)]
;; use unification to see if we can use the polytype here
[(list (Poly: vs b) s)
(=> unmatch)
@ -292,10 +295,7 @@
[(list (Values: vals1) (Values: vals2)) (subtypes* A0 vals1 vals2)]
;; single values shouldn't actually happen, but they're just like the type
[(list t (Values: (list t*))) (int-err "BUG - singleton values type~a" (make-Values (list t*)))]
[(list (Values: (list t)) t*) (int-err "BUG - singleton values type~a" (make-Values (list t)))]
;; A refinement is a subtype of its parent
[(list (Refinement: par _ _) t)
(subtype* A0 par t)]
[(list (Values: (list t)) t*) (int-err "BUG - singleton values type~a" (make-Values (list t)))]
;; subtyping on other stuff
[(list (Syntax: t) (Syntax: t*))
(subtype* A0 t t*)]

2
collects/typed-scheme/private/type-effect-printer.ss
View File

@ -123,6 +123,8 @@
[(F: nm) (fp "~a" nm)]
[(Values: (list v ...)) (fp "~a" (cons 'values v))]
[(ValuesDots: v dty dbound) (fp "~a" (cons 'values (append v (list dty '... dbound))))]
[(Refinement: parent p? _)
(fp "(Refinement ~a ~a)" parent (syntax-e p?))]
[(Param: in out)
(if (equal? in out)
(fp "(Parameter ~a)" in)