Remove tc-results? and other minor improvements.

This commit is contained in:
Eric Dobson 2013-01-20 14:49:06 -08:00 committed by Sam Tobin-Hochstadt
parent 5a43a5c730
commit a2f33f17e9
12 changed files with 57 additions and 46 deletions

View File

@ -2028,7 +2028,9 @@
(-> (-> b) Univ)))]
[abort-current-continuation
(-polydots (a b d e c)
(->... (list (make-Prompt-Tagof b (->... '() (c c) d))) (c c) e))]
(cl->*
(->... (list (make-Prompt-Tagof b (->... '() (c c) d))) (c c) e)
(->... (list (make-Prompt-Tagof b (->... '() (c c) ManyUniv))) (c c) e)))]
[make-continuation-prompt-tag
(-poly (a b) (->opt [Sym] (make-Prompt-Tagof a b)))]
;; default-continuation-prompt-tag is defined in "base-contracted.rkt"

View File

@ -312,7 +312,7 @@
;; the index variables from the TOPLAS paper
(define/cond-contract (cgen V X Y S T)
((listof symbol?) (listof symbol?) (listof symbol?)
(or/c Values/c ValuesDots?) (or/c Values/c ValuesDots?). -> . cset?)
(or/c Values/c ValuesDots? AnyValues?) (or/c Values/c ValuesDots? AnyValues?) . -> . cset?)
;; useful quick loop
(define/cond-contract (cg S T)
(Type/c Type/c . -> . cset?)
@ -334,6 +334,7 @@
[(a a) empty]
;; CG-Top
[(_ (Univ:)) empty]
[(_ (AnyValues:)) empty]
;; check all non Type/c first so that calling subtype is safe

View File

@ -21,8 +21,8 @@
(provide/cond-contract [parse-type (syntax? . c:-> . Type/c)]
[parse-type/id (syntax? c:any/c . c:-> . Type/c)]
[parse-tc-results (syntax? . c:-> . tc-results?)]
[parse-tc-results/id (syntax? c:any/c . c:-> . tc-results?)])
[parse-tc-results (syntax? . c:-> . tc-results/c)]
[parse-tc-results/id (syntax? c:any/c . c:-> . tc-results/c)])
(provide star ddd/bound)
(define enable-mu-parsing (make-parameter #t))

View File

@ -117,6 +117,11 @@
(tc-expr/check expr (ret anns))
(let ([ty (tc-expr expr)])
(match ty
[(tc-any-results:)
(ret
(tc-error/expr
"Expression should produce ~a values, but produces an unknown number of values"
(length stxs)))]
[(tc-results: tys fs os)
(if (not (= (length stxs) (length tys)))
(begin
@ -127,8 +132,8 @@
(combine-results
(for/list ([stx stxs] [ty tys] [a anns] [f fs] [o os])
(cond [a (check-type stx ty a) (ret a f o)]
;; mutated variables get generalized, so that we don't infer too small a type
[(is-var-mutated? stx) (ret (generalize ty) f o)]
;; mutated variables get generalized, so that we don't infer too small a type
[(is-var-mutated? stx) (ret (generalize ty) f o)]
[else (ret ty f o)]))))]))))]))
;; check that e-type is compatible with ty in context of stx

View File

@ -15,6 +15,30 @@
(define name-table (make-weak-hasheq))
(define Type/c?
(λ (e)
(and (Type? e)
(not (Scope? e))
(not (arr? e))
(not (fld? e))
(not (Values? e))
(not (ValuesDots? e))
(not (AnyValues? e))
(not (Result? e)))))
;; (or/c Type/c Values? Results?)
;; Anything that can be treated as a Values by sufficient expansion
(define Values/c?
(λ (e)
(and (Type? e)
(not (Scope? e))
(not (arr? e))
(not (fld? e))
(not (ValuesDots? e))
(not (AnyValues? e)))))
(define Type/c (flat-named-contract 'Type Type/c?))
(define Values/c (flat-named-contract 'Values Values/c?))
;; Name = Symbol
@ -215,6 +239,8 @@
(combine-frees (map free-idxs* (cons dty rs))))]
[#:fold-rhs (*ValuesDots (map type-rec-id rs) (type-rec-id dty) dbound)])
(define SomeValues/c (or/c Values? AnyValues? ValuesDots?))
;; arr is NOT a Type
(def-type arr ([dom (listof Type/c)]
[rng SomeValues/c]
@ -743,31 +769,6 @@
;(trace subst subst-all)
(define Type/c?
(λ (e)
(and (Type? e)
(not (Scope? e))
(not (arr? e))
(not (fld? e))
(not (Values? e))
(not (ValuesDots? e))
(not (AnyValues? e))
(not (Result? e)))))
;; (or/c Type/c Values? Results?)
;; Anything that can be treated as a Values by sufficient expansion
(define Values/c?
(λ (e)
(and (Type? e)
(not (Scope? e))
(not (arr? e))
(not (fld? e))
(not (ValuesDots? e))
(not (AnyValues? e)))))
(define Type/c (flat-named-contract 'Type Type/c?))
(define Values/c (flat-named-contract 'Values Values/c?))
(define SomeValues/c (or/c Values? AnyValues? ValuesDots?))
(provide
Mu-name:

View File

@ -12,8 +12,10 @@
(only-in srfi/1 split-at))
(provide/cond-contract
[check-below (-->d ([s (-or/c Type/c tc-results/c)] [t (-or/c Type/c tc-results/c)]) () [_ (if (Type? s) Type/c tc-results/c)])]
[cond-check-below (-->d ([s (-or/c Type/c tc-results/c)] [t (-or/c #f Type/c tc-results/c)]) () [_ (if (Type? s) Type/c tc-results/c)])])
[check-below (-->d ([s (-or/c Type/c tc-results/c)] [t (-or/c Type/c tc-results/c)]) ()
[_ (if (Type/c? s) Type/c tc-results/c)])]
[cond-check-below (-->d ([s (-or/c Type/c tc-results/c)] [t (-or/c #f Type/c tc-results/c)]) ()
[_ (if (Type/c? s) Type/c tc-results/c)])])
(define (print-object o)
(match o
@ -103,6 +105,13 @@
(unless (for/and ([t t1] [s t2]) (subtype t s))
(tc-error/expr "Expected ~a, but got ~a" (stringify t2) (stringify t1)))
expected]
[((tc-any-results:) (or (? Type/c? t) (tc-result1: t _ _)))
(tc-error/expr "Expected 1 value, but got unknown number")
expected]
[((tc-any-results:) (tc-results: t2 fs os))
(tc-error/expr "Expected ~a values, but got unknown number" (length t2))
expected]
[((tc-result1: t1 f o) (? Type/c? t2))
(unless (subtype t1 t2)
(tc-error/expr "Expected ~a, but got ~a" t2 t1))

View File

@ -27,7 +27,7 @@
;; we just ignore the values, except that it forces arg to return one value
(pattern (values arg)
(match expected
[#f (single-value #'arg)]
[(or #f (tc-any-results:)) (single-value #'arg)]
[(tc-result1: tp)
(single-value #'arg expected)]
[(tc-results: ts)

View File

@ -242,7 +242,7 @@
(match (find-expected expected f*)
;; very conservative -- only do anything interesting if we get exactly one thing that matches
[(list)
(if (and (= 1 (length formals*)) (tc-results? expected))
(if (and (= 1 (length formals*)) (match expected ((tc-results: _) #t) (_ #f)))
(tc-error/expr #:return (list (lam-result null null (list #'here Univ) #f (ret (Un))))
"Expected a function of type ~a, but got a function with the wrong arity"
(match expected [(tc-result1: t) t]))

View File

@ -29,7 +29,7 @@
(define/cond-contract (do-check expr->type namess results expected-results form exprs body clauses expected #:abstract [abstract null])
(((syntax? syntax? tc-results/c . c:-> . any/c)
(listof (listof identifier?)) (listof tc-results?) (listof tc-results?)
(listof (listof identifier?)) (listof tc-results/c) (listof tc-results/c)
syntax? (listof syntax?) syntax? (listof syntax?) (or/c #f tc-results/c))
(#:abstract any/c)
. c:->* .
@ -130,7 +130,6 @@
(cond
;; after everything, check the body expressions
[(null? names)
;(if expected (tc-exprs/check (syntax->list body) expected) (tc-exprs (syntax->list body)))
(do-check void null null null form null body null expected #:abstract orig-flat-names)]
;; if none of the names bound in the letrec are free vars of this rhs
[(not (ormap (lambda (n) (s:member n flat-names bound-identifier=?))

View File

@ -13,7 +13,7 @@
(define/cond-contract (abstract-results results arg-names)
(tc-results? (listof identifier?) . -> . SomeValues/c)
(tc-results/c (listof identifier?) . -> . SomeValues/c)
(define keys (for/list ([(nm k) (in-indexed arg-names)]) k))
(match results
[(tc-any-results:) (make-AnyValues)]

View File

@ -17,12 +17,7 @@
;A Type that corresponds to the any contract for the
;return type of functions
;FIXME
;This is not correct as Univ is only a single value.
(define ManyUniv Univ)
(define ManyUniv (make-AnyValues))
;; Char type (needed because of how sequences are checked in subtype)
(define -Char (make-Base 'Char #'char? char? #'-Char #f))

View File

@ -110,7 +110,7 @@
Object?)]
[dty Type/c]
[dbound symbol?])
[res tc-results?])])
[res tc-results/c])])
(define (combine-results tcs)
(match tcs
@ -124,7 +124,6 @@
(tc-any-results* tc-any-results)))
(provide/cond-contract
[combine-results ((listof tc-results?) . -> . tc-results?)]
[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?)]