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

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

View File

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

View File

@ -55,14 +55,9 @@
`(make-Path ,(sub p) ,(if (identifier? i)
`(quote-syntax ,i)
i))]
[(? (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)))
`(,(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))]
[(? Rep? rep)
`(,(gen-constructor (car (vector->list (struct->vector rep))))
,@(map sub (Rep-values rep)))]
[_ (basic v)]))
(define (bound-in-this-module id)

View File

@ -1,7 +1,7 @@
#lang racket/base
(require "../utils/utils.rkt")
(require syntax/boundmap
(require syntax/boundmap
racket/dict
(env type-alias-env)
(utils tc-utils)

View File

@ -27,11 +27,11 @@
(define (seen-before s t)
(cons (Type-seq s) (Type-seq t)))
(define/cond-contract (remember s t A)
(Type? Type? (listof (cons/c exact-nonnegative-integer? exact-nonnegative-integer?)) . -> .
(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?)))
(cons (seen-before s t) A))
(define/cond-contract (seen? s t)
(Type? Type? . -> . any/c)
(Type/c Type/c . -> . any/c)
(member (seen-before s t) (current-seen)))
@ -167,7 +167,7 @@
[(_ _) (fail! s t)]))
(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))
(match* (s-arr t-arr)
;; the simplest case - no rests, drests, keywords
@ -310,10 +310,10 @@
;; 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? Type? . -> . cset?)
((listof symbol?) (listof symbol?) (listof symbol?) Type/c Type/c . -> . cset?)
;; useful quick loop
(define/cond-contract (cg S T)
(Type? Type? . -> . cset?)
(Type/c Type/c . -> . cset?)
(cgen V X Y S T))
;; this places no constraints on any variables in X
(define empty (empty-cset X Y))
@ -578,9 +578,9 @@
;; C : cset? - set of constraints found by the inference engine
;; 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)
(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 idx-hash (free-vars-hash (free-idxs* R)))
;; 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
(define/cond-contract (cgen/list V X Y S T
#: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?)
(unless (= (length S) (length T))
(fail! S T))
@ -712,7 +712,7 @@
(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?) ((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)])
(let* ([expected-cset (if expected
(cgen null X Y R expected)

View File

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

View File

@ -19,12 +19,12 @@
(def-filter Bot () [#: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))]
[#: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?] [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))]
[#:frees (λ (f) (combine-frees (map f (cons t p))))]
[#: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 SyntaxPE () [#:fold-rhs #:base])
;; 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))]
[#: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]
[PathElem def-pathelem #:PathElem pathelem-case print-pathelem pathelem-name-ht pathelem-rec-id])
(provide PathElem? (rename-out [Rep-seq Type-seq]
[Rep-free-vars free-vars*]
[Rep-free-idxs free-idxs*]))
(define (Rep-values rep)
(match rep
[(? (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?]
[free-vars (hash/c symbol? variance?)]

View File

@ -12,8 +12,8 @@
(only-in srfi/1 split-at))
(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?)])]
[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?)])])
[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/c s) Type/c tc-results?)])])
(define (print-object o)
(match o

View File

@ -328,22 +328,16 @@
#'(begin
(require racket/pretty)
(require mzlib/pconvert)
(define (converter v basic sub)
(define (gen-constructor sym)
(string->symbol (string-append "make-" (substring (symbol->string sym) 7))))
(match v
[(? (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)))
`(,(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))]
[(? Rep? rep)
`(,(gen-constructor (car (vector->list (struct->vector rep))))
,@(map sub (Rep-values rep)))]
[_ (basic v)]))
(define (debug-printer v port write?)
((if write? pretty-write pretty-print)
(parameterize ((current-print-convert-hook converter))

View File

@ -17,7 +17,7 @@
(define (resolve-name t)
(match t
[(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)]))
(define already-resolving? (make-parameter #f))

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?) (#:Un procedure?) . ->* . Type?)
((simple-substitution/c Type/c) (#:Un procedure?) . ->* . Type/c)
(define (sb t) (substitute-many subst t #:Un Un))
(define names (hash-keys subst))
(define fvs (free-vars* target))
@ -74,13 +74,13 @@
;; substitute : Type Name Type -> Type
(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))
;; 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? . -> . Type?)
((listof Type/c) (or/c #f Type/c) symbol? Type/c . -> . Type/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))
@ -157,7 +157,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? . -> . Type?)
(substitution/c Type/c . -> . Type/c)
(define t-substs
(for/fold ([acc (hash)]) ([(v r) (in-hash s)])

View File

@ -113,4 +113,4 @@
[tc-result? (any/c . -> . boolean?)]
[tc-result-t (tc-result? . -> . Type/c)]
[tc-result-equal? (tc-result? tc-result? . -> . boolean?)]
[tc-results? (any/c . -> . boolean?)])
[tc-results? (any/c . -> . boolean?)])