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

Basic support for contract gen for PolyRow types

Browse Source 
Currently only supports the typed export side. The other
way needs contract features that haven't been merged yet.
This commit is contained in:
Asumu Takikawa 2015-02-27 14:13:11 -05:00
parent 6a855f664c
commit ec15f58542
2 changed files with 20 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
typed-racket-lib/typed-racket/private/type-contract.rkt
View File

@ -402,6 +402,8 @@
(t->sc/poly type fail typed-side recursive-values t->sc)]
[(? PolyDots?)
(t->sc/polydots type fail typed-side recursive-values t->sc)]
[(? PolyRow?)
(t->sc/polyrow type fail typed-side recursive-values t->sc)]
[(Mu: n b)
(match-define (and n*s (list untyped-n* typed-n* both-n*)) (generate-temporaries (list n n n)))
@ -602,6 +604,8 @@
(t->sc/poly type fail typed-side recursive-values rec)]
[(? PolyDots?)
(t->sc/polydots type fail typed-side recursive-values rec)]
[(? PolyRow?)
(t->sc/polyrow type fail typed-side recursive-values rec)]
[(? Function?)
(t->sc/function type fail typed-side recursive-values loop #t)]
[_ (fail #:reason "invalid method type")]))
@ -645,6 +649,16 @@
;; in negative position, cannot generate for polydots yet
(fail #:reason "cannot generate contract for variable arity polymorphic type")))
;; Generate a contract for a row-polymorphic function type
(define (t->sc/polyrow type fail typed-side recursive-values t->sc)
(match-define (PolyRow: vs constraints body) type)
(if (not (from-untyped? typed-side))
(let ((recursive-values (for/fold ([rv recursive-values]) ([v vs])
(hash-set rv v (same any/sc)))))
(t->sc body #:recursive-values recursive-values))
;; FIXME: needs sealing contracts, disabled for now
(fail #:reason "cannot generate contract for row polymorphic type")))
;; Predicate that checks for an App type with a recursive
;; Name type in application position
(define (has-name-app? type)

6
typed-racket-test/unit-tests/contract-tests.rkt
View File

@ -144,6 +144,10 @@
(t (-polydots (a) -Symbol))
(t (-polydots (a) (->... (list) (a a) -Symbol)))
(t (-polyrow (a) (list null null null null) -Symbol))
(t (-polyrow (a) (list null null null null)
(-> (-class #:row (-v a)) (-class #:row (-v a)))))
(t (-mu x (-Syntax x)))
(t (-> (-> Univ -Bottom : -bot-filter) -Bottom : -bot-filter))
(t (-poly (A B) (-> A B (Un A B))))
@ -217,6 +221,8 @@
#f))
(t (-class #:method ([m (-poly (x) (-> x x))])))
(t (-class #:method ([m (-polydots (x) (->... (list) (x x) -Void))])))
(t (-class #:method ([m (-polyrow (x) (list null null null null)
(-> (-class #:row (-v x)) -Void))])))
;; typed/untyped interaction tests
(t-int (-poly (a) (-> a a))