Replace uses of Type? in contracts with Type/c.

This commit is contained in:
Eric Dobson 2012-09-01 18:44:50 -07:00 committed by Sam Tobin-Hochstadt
parent cab90c16d5
commit 8a8dc66a19
13 changed files with 50 additions and 47 deletions

View File

@ -4,7 +4,7 @@
;; maps identifiers to their types, updated by mutation ;; maps identifiers to their types, updated by mutation
(require "../types/tc-error.rkt" (require "../types/tc-error.rkt"
syntax/id-table syntax/id-table
unstable/lazy-require) unstable/lazy-require)
(provide register-type register-type-if-undefined (provide register-type register-type-if-undefined
finish-register-type finish-register-type

View File

@ -55,14 +55,9 @@
`(make-Path ,(sub p) ,(if (identifier? i) `(make-Path ,(sub p) ,(if (identifier? i)
`(quote-syntax ,i) `(quote-syntax ,i)
i))] i))]
[(? (lambda (e) (or (Filter? e) [(? Rep? rep)
(Object? e) `(,(gen-constructor (car (vector->list (struct->vector rep))))
(PathElem? e))) ,@(map sub (Rep-values rep)))]
(app (lambda (v) (vector->list (struct->vector v))) (list-rest tag seq fv fi stx vals)))
`(,(gen-constructor tag) ,@(map sub vals))]
[(? Type?
(app (lambda (v) (vector->list (struct->vector v))) (list-rest tag seq fv fi stx key vals)))
`(,(gen-constructor tag) ,@(map sub vals))]
[_ (basic v)])) [_ (basic v)]))
(define (bound-in-this-module id) (define (bound-in-this-module id)

View File

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

View File

@ -59,5 +59,5 @@
((or/c #f Values? ValuesDots? Result? Type/c)) . ->* . any)] ((or/c #f Values? ValuesDots? Result? Type/c)) . ->* . any)]
[cond-contracted infer/dots (((listof symbol?) [cond-contracted infer/dots (((listof symbol?)
symbol? symbol?
(listof Type/c) (listof Type/c) Type/c Type? (listof symbol?)) (listof Type/c) (listof Type/c) Type/c Type/c (listof symbol?))
(#:expected (or/c #f Type?)) . ->* . any)])) (#:expected (or/c #f Type/c)) . ->* . any)]))

View File

@ -19,12 +19,12 @@
(def-filter Bot () [#:fold-rhs #:base]) (def-filter Bot () [#:fold-rhs #:base])
(def-filter Top () [#:fold-rhs #:base]) (def-filter Top () [#:fold-rhs #:base])
(def-filter TypeFilter ([t Type?] [p (listof PathElem?)] [v name-ref/c]) (def-filter TypeFilter ([t Type/c] [p (listof PathElem?)] [v name-ref/c])
[#:intern (list (Rep-seq t) (map Rep-seq p) (hash-name v))] [#:intern (list (Rep-seq t) (map Rep-seq p) (hash-name v))]
[#:frees (λ (f) (combine-frees (map f (cons t p))))] [#:frees (λ (f) (combine-frees (map f (cons t p))))]
[#:fold-rhs (*TypeFilter (type-rec-id t) (map pathelem-rec-id p) v)]) [#:fold-rhs (*TypeFilter (type-rec-id t) (map pathelem-rec-id p) v)])
(def-filter NotTypeFilter ([t Type?] [p (listof PathElem?)] [v name-ref/c]) (def-filter NotTypeFilter ([t Type/c] [p (listof PathElem?)] [v name-ref/c])
[#:intern (list (Rep-seq t) (map Rep-seq p) (hash-name v))] [#:intern (list (Rep-seq t) (map Rep-seq p) (hash-name v))]
[#:frees (λ (f) (combine-frees (map f (cons t p))))] [#:frees (λ (f) (combine-frees (map f (cons t p))))]
[#:fold-rhs (*NotTypeFilter (type-rec-id t) (map pathelem-rec-id p) v)]) [#:fold-rhs (*NotTypeFilter (type-rec-id t) (map pathelem-rec-id p) v)])

View File

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

View File

@ -353,9 +353,23 @@
[Object def-object #:Object object-case print-object object-name-ht object-rec-id] [Object def-object #:Object object-case print-object object-name-ht object-rec-id]
[PathElem def-pathelem #:PathElem pathelem-case print-pathelem pathelem-name-ht pathelem-rec-id]) [PathElem def-pathelem #:PathElem pathelem-case print-pathelem pathelem-name-ht pathelem-rec-id])
(provide PathElem? (rename-out [Rep-seq Type-seq] (define (Rep-values rep)
[Rep-free-vars free-vars*] (match rep
[Rep-free-idxs free-idxs*])) [(? (lambda (e) (or (Filter? e)
(Object? e)
(PathElem? e)))
(app (lambda (v) (vector->list (struct->vector v))) (list-rest tag seq fv fi stx vals)))
vals]
[(? Type?
(app (lambda (v) (vector->list (struct->vector v))) (list-rest tag seq fv fi stx key vals)))
vals]))
(provide
Rep-values
(rename-out [Rep-seq Type-seq]
[Rep-free-vars free-vars*]
[Rep-free-idxs free-idxs*]))
(provide/cond-contract (struct Rep ([seq exact-nonnegative-integer?] (provide/cond-contract (struct Rep ([seq exact-nonnegative-integer?]
[free-vars (hash/c symbol? variance?)] [free-vars (hash/c symbol? variance?)]

View File

@ -12,8 +12,8 @@
(only-in srfi/1 split-at)) (only-in srfi/1 split-at))
(provide/cond-contract (provide/cond-contract
[check-below (-->d ([s (-or/c Type/c tc-results?)] [t (-or/c Type/c tc-results?)]) () [_ (if (Type? s) Type/c tc-results?)])] [check-below (-->d ([s (-or/c Type/c tc-results?)] [t (-or/c Type/c tc-results?)]) () [_ (if (Type/c s) Type/c tc-results?)])]
[cond-check-below (-->d ([s (-or/c Type/c tc-results?)] [t (-or/c #f Type/c tc-results?)]) () [_ (if (Type? s) Type/c tc-results?)])]) [cond-check-below (-->d ([s (-or/c Type/c tc-results?)] [t (-or/c #f Type/c tc-results?)]) () [_ (if (Type/c s) Type/c tc-results?)])])
(define (print-object o) (define (print-object o)
(match o (match o

View File

@ -333,15 +333,9 @@
(define (gen-constructor sym) (define (gen-constructor sym)
(string->symbol (string-append "make-" (substring (symbol->string sym) 7)))) (string->symbol (string-append "make-" (substring (symbol->string sym) 7))))
(match v (match v
[(? (lambda (e) (or (Filter? e) [(? Rep? rep)
(Object? e) `(,(gen-constructor (car (vector->list (struct->vector rep))))
(PathElem? e))) ,@(map sub (Rep-values rep)))]
(app (lambda (v) (vector->list (struct->vector v)))
(list-rest tag seq fv fi stx vals)))
`(,(gen-constructor tag) ,@(map sub vals))]
[(? Type?
(app (lambda (v) (vector->list (struct->vector v))) (list-rest tag seq fv fi stx key vals)))
`(,(gen-constructor tag) ,@(map sub vals))]
[_ (basic v)])) [_ (basic v)]))
(define (debug-printer v port write?) (define (debug-printer v port write?)

View File

@ -17,7 +17,7 @@
(define (resolve-name t) (define (resolve-name t)
(match t (match t
[(Name: n) (let ([t (lookup-type-name n)]) [(Name: n) (let ([t (lookup-type-name n)])
(if (Type? t) t #f))] (if (Type/c t) t #f))]
[_ (int-err "resolve-name: not a name ~a" t)])) [_ (int-err "resolve-name: not a name ~a" t)]))
(define already-resolving? (make-parameter #f)) (define already-resolving? (make-parameter #f))

View File

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