Make TR compile with contracts enabled again.

original commit: 5fe004cd9b85eadf15957cb75f5c15dd7226392e
This commit is contained in:
Eric Dobson 2013-01-12 13:10:33 -08:00 committed by Sam Tobin-Hochstadt
parent 106b3a98cf
commit ed0bb82dcf
7 changed files with 45 additions and 22 deletions

View File

@ -27,11 +27,12 @@
(define (seen-before s t)
(cons (Type-seq s) (Type-seq t)))
(define/cond-contract (remember s t A)
(Type/c Type/c (listof (cons/c exact-nonnegative-integer? exact-nonnegative-integer?)) . -> .
(listof (cons/c exact-nonnegative-integer? exact-nonnegative-integer?)))
(Values/c Values/c
(listof (cons/c exact-nonnegative-integer? exact-nonnegative-integer?)) . -> .
(listof (cons/c exact-nonnegative-integer? exact-nonnegative-integer?)))
(cons (seen-before s t) A))
(define/cond-contract (seen? s t)
(Type/c Type/c . -> . any/c)
(Values/c Values/c . -> . any/c)
(member (seen-before s t) (current-seen)))
@ -167,7 +168,7 @@
[(_ _) (fail! s t)]))
(define/cond-contract (cgen/arr V X Y s-arr t-arr)
((listof symbol?) (listof symbol?) (listof symbol?) Type/c Type/c . -> . cset?)
((listof symbol?) (listof symbol?) (listof symbol?) arr? arr? . -> . cset?)
(define (cg S T) (cgen V X Y S T))
(match* (s-arr t-arr)
;; the simplest case - no rests, drests, keywords
@ -310,7 +311,8 @@
;; implements the V |-_X S <: T => C judgment from Pierce+Turner, extended with
;; the index variables from the TOPLAS paper
(define/cond-contract (cgen V X Y S T)
((listof symbol?) (listof symbol?) (listof symbol?) Type/c Type/c . -> . cset?)
((listof symbol?) (listof symbol?) (listof symbol?)
(or/c Values/c ValuesDots?) (or/c Values/c ValuesDots?). -> . cset?)
;; useful quick loop
(define/cond-contract (cg S T)
(Type/c Type/c . -> . cset?)
@ -584,7 +586,7 @@
;; Y : (listof symbol?) - index variables that must have entries
;; R : Type/c - result type into which we will be substituting
(define/cond-contract (subst-gen C Y R)
(cset? (listof symbol?) Type/c . -> . (or/c #f substitution/c))
(cset? (listof symbol?) (or/c Values/c ValuesDots?) . -> . (or/c #f substitution/c))
(define var-hash (free-vars-hash (free-vars* R)))
(define idx-hash (free-vars-hash (free-idxs* R)))
;; v : Symbol - variable for which to check variance
@ -691,7 +693,7 @@
;; produces a cset which determines a substitution that makes the Ss subtypes of the Ts
(define/cond-contract (cgen/list V X Y S T
#:expected-cset [expected-cset (empty-cset '() '())])
(((listof symbol?) (listof symbol?) (listof symbol?) (listof Type/c) (listof Type/c))
(((listof symbol?) (listof symbol?) (listof symbol?) (listof Values/c) (listof Values/c))
(#:expected-cset cset?) . ->* . cset?)
(unless (= (length S) (length T))
(fail! S T))
@ -716,7 +718,10 @@
(define infer
(let ()
(define/cond-contract (infer X Y S T R [expected #f])
(((listof symbol?) (listof symbol?) (listof Type/c) (listof Type/c) Type/c) ((or/c #f Type/c)) . ->* . (or/c boolean? substitution/c))
(((listof symbol?) (listof symbol?) (listof Type/c) (listof Type/c)
(or/c #f Values/c ValuesDots?))
((or/c #f Values/c ValuesDots?))
. ->* . (or/c boolean? substitution/c))
(with-handlers ([exn:infer? (lambda _ #f)])
(let* ([expected-cset (if expected
(cgen null X Y R expected)

View File

@ -39,9 +39,9 @@
;; domain
(listof Type/c)
;; range
(or/c #f Values? ValuesDots? Result? Type/c))
(or/c #f Values/c ValuesDots?))
;; optional expected type
((or/c #f Values? ValuesDots? Result? Type/c))
((or/c #f Values/c ValuesDots?))
. ->* . any)]
[cond-contracted infer/vararg ((;; variables from the forall
(listof symbol?)
@ -54,10 +54,14 @@
;; rest
(or/c #f Type/c)
;; range
(or/c #f Values? ValuesDots? Result? Type/c))
(or/c #f Values/c ValuesDots?))
;; [optional] expected type
((or/c #f Values? ValuesDots? Result? Type/c)) . ->* . any)]
((or/c #f Values/c ValuesDots?)) . ->* . any)]
[cond-contracted infer/dots (((listof symbol?)
symbol?
(listof Type/c) (listof Type/c) Type/c Type/c (listof symbol?))
(#:expected (or/c #f Type/c)) . ->* . any)]))
(listof Values/c)
(listof Values/c)
Values/c
(or/c Values/c ValuesDots?)
(listof symbol?))
(#:expected (or/c #f Values/c ValuesDots?)) . ->* . any)]))

View File

@ -19,12 +19,14 @@
(def-filter Bot () [#:fold-rhs #:base])
(def-filter Top () [#:fold-rhs #:base])
(def-filter TypeFilter ([t Type/c] [p (listof PathElem?)] [v name-ref/c])
;; TODO: t should only be a Type/c, but that leads to circular dependencies
(def-filter TypeFilter ([t Type?] [p (listof PathElem?)] [v name-ref/c])
[#:intern (list (Rep-seq t) (map Rep-seq p) (hash-name v))]
[#:frees (λ (f) (combine-frees (map f (cons t p))))]
[#:fold-rhs (*TypeFilter (type-rec-id t) (map pathelem-rec-id p) v)])
(def-filter NotTypeFilter ([t Type/c] [p (listof PathElem?)] [v name-ref/c])
;; TODO: t should only be a Type/c, but that leads to circular dependencies
(def-filter NotTypeFilter ([t Type?] [p (listof PathElem?)] [v name-ref/c])
[#:intern (list (Rep-seq t) (map Rep-seq p) (hash-name v))]
[#:frees (λ (f) (combine-frees (map f (cons t p))))]
[#:fold-rhs (*NotTypeFilter (type-rec-id t) (map pathelem-rec-id p) v)])

View File

@ -13,7 +13,7 @@
(def-pathelem SyntaxPE () [#:fold-rhs #:base])
(def-pathelem ForcePE () [#:fold-rhs #:base])
;; t is always a Name (can't put that into the contract b/c of circularity)
(def-pathelem StructPE ([t Type/c] [idx natural-number/c])
(def-pathelem StructPE ([t Type?] [idx natural-number/c])
[#:frees (λ (f) (f t))]
[#:fold-rhs (*StructPE (type-rec-id t) idx)])

View File

@ -25,7 +25,17 @@
(not (ValuesDots? e))
(not (Result? e)))))
;; (or/c Type/c Values? Results?)
(define Values/c?
(λ (e)
(and (Type? e)
(not (Scope? e))
(not (arr? e))
(not (fld? e))
(not (ValuesDots? e)))))
(define Type/c (flat-named-contract 'Type Type/c?))
(define Values/c (flat-named-contract 'Values Values/c?))
;; Name = Symbol
@ -417,7 +427,7 @@
;; handler: the type of the prompt handler
;; prompts with this tag will return a union of `body`
;; and the codomains of `handler`
(def-type Prompt-Tagof ([body Type/c] [handler Function?])
(def-type Prompt-Tagof ([body Type/c] [handler Type/c])
[#:frees (λ (f) (combine-frees (list (make-invariant (f body))
(make-invariant (f handler)))))]
[#:key 'prompt-tag])
@ -760,6 +770,7 @@
Mu? Poly? PolyDots?
Filter? Object?
Type/c Type/c?
Values/c
Poly-n
PolyDots-n
free-vars*

View File

@ -13,6 +13,7 @@
racket/function
racket/match
racket/list
racket/struct-info
(only-in racket/contract
listof any/c or/c
[->* c->*]
@ -150,7 +151,7 @@
;; Register the approriate types to the struct bindings.
(define/cond-contract (register-struct-bindings! sty names desc si)
(c-> Struct? struct-names? struct-desc? (or/c #f struct-info?) (listof def-binding?))
(c-> Struct? struct-names? struct-desc? (or/c #f struct-info?) (listof binding?))
(define tvars (struct-desc-tvars desc))

View File

@ -37,7 +37,7 @@
;; substitute-many : Hash[Name,Type] Type -> Type
(define/cond-contract (substitute-many subst target #:Un [Un (lambda (args) (apply Un args))])
((simple-substitution/c Type/c) (#:Un procedure?) . ->* . Type/c)
((simple-substitution/c (or/c Values/c arr?)) (#:Un procedure?) . ->* . (or/c Values/c arr?))
(define (sb t) (substitute-many subst t #:Un Un))
(define names (hash-keys subst))
(define fvs (free-vars* target))
@ -86,7 +86,7 @@
;; implements angle bracket substitution from the formalism
;; substitute-dots : Listof[Type] Option[type] Name Type -> Type
(define/cond-contract (substitute-dots images rimage name target)
((listof Type/c) (or/c #f Type/c) symbol? Type/c . -> . Type/c)
((listof Type/c) (or/c #f Type/c) symbol? (or/c arr? Values/c) . -> . (or/c arr? Values/c))
(define (sb t) (substitute-dots images rimage name t))
(if (or (set-member? (free-vars-names (free-idxs* target)) name)
(set-member? (free-vars-names (free-vars* target)) name))
@ -163,7 +163,7 @@
;; substitution = Listof[U List[Name,Type] List[Name,Listof[Type]]]
;; subst-all : substitution Type -> Type
(define/cond-contract (subst-all s ty)
(substitution/c Type/c . -> . Type/c)
(substitution/c (or/c arr? Values/c) . -> . (or/c Values/c arr?))
(define t-substs
(for/fold ([acc (hash)]) ([(v r) (in-hash s)])