Sync to trunk again.

Fix require/contract.
Subtyping, printing for refinements.

svn: r14626

original commit: f2bffcabab6e027a2cd59dc78ab0fd5a77be99c7
This commit is contained in:
Sam Tobin-Hochstadt 2009-04-27 18:26:00 +00:00
parent 8b96f98595
commit f4ebee3d68
6 changed files with 35 additions and 10 deletions

View File

@ -46,6 +46,6 @@
(define (type-name-env-map f)
(module-identifier-mapping-map the-mapping f))
(define (add-alias from to)
(define (add-alias from to)
(when (lookup-type-name to (lambda () #f))
(register-resolved-type-alias from (make-Name to))))

View File

@ -242,10 +242,10 @@
(S T)
[(a a) empty]
[(_ (Univ:)) empty]
[((Refinement: S _ _) T)
(cg S T)]
[((F: (? (lambda (e) (memq e X)) v)) S)
(when (match S
[(F: v*)
@ -260,7 +260,7 @@
[_ #f])
(fail! S T))
(singleton (var-promote S V) v Univ)]
;; two unions with the same number of elements, so we just try to unify them pairwise
#;[((Union: l1) (Union: l2))
(=> unmatch)

View File

@ -40,7 +40,7 @@
@defidform[Namespace]
@defidform[EOF]
@defidform[Char])]{
These types represent primitive Scheme data.}
These types represent primitive Scheme data. Note that @scheme[Integer] represents exact integers.}
@defidform[Any]{Any Scheme value. All other types are subtypes of @scheme[Any].}

View File

@ -181,6 +181,8 @@
[(Result: t (LFilterSet: (list) (list)) (LEmpty:)) (fp "~a" t)]
[(Result: t fs (LEmpty:)) (fp "(~a : ~a)" t fs)]
[(Result: t fs lo) (fp "(~a : ~a : ~a)" t fs lo)]
[(Refinement: parent p? _)
(fp "(Refinement ~a ~a)" parent (syntax-e p?))]
[else (fp "Unknown Type: ~a" (struct->vector c))]
))

View File

@ -226,6 +226,8 @@
(unmatch))
;(printf "Poly: ~n~a ~n~a~n" b1 (subst-all (map list ms (map make-F ns)) b2))
(subtype* A0 b1 (subst-all (map list ms (map make-F ns)) b2))]
[(list (Refinement: par _ _) t)
(subtype* A0 par t)]
;; use unification to see if we can use the polytype here
[(list (Poly: vs b) s)
(=> unmatch)

View File

@ -1,6 +1,9 @@
#lang scheme/base
(require scheme/contract (for-syntax scheme/base syntax/kerncase))
(require scheme/contract (for-syntax scheme/base syntax/kerncase
"../utils/tc-utils.ss"
(prefix-in tr: "../private/typed-renaming.ss")))
(provide require/contract define-ignored)
(define-syntax (define-ignored stx)
@ -20,12 +23,30 @@
'inferred-name
(syntax-e #'name)))])]))
(define-syntax (get-alternate stx)
(syntax-case stx ()
[(_ id)
(tr:get-alternate #'id)]))
(define-syntax (require/contract stx)
(syntax-case stx ()
[(require/contract nm cnt lib)
(identifier? #'nm)
#`(begin (require (only-in lib [nm tmp]))
(define-ignored nm (contract cnt tmp '(interface for #,(syntax->datum #'nm)) 'never-happen (quote-syntax nm))))]
(begin
#`(begin (require (only-in lib [nm tmp]))
(define-ignored nm
(contract cnt
(get-alternate tmp)
'(interface for #,(syntax->datum #'nm))
'never-happen
(quote-syntax nm)))))]
[(require/contract (orig-nm nm) cnt lib)
#`(begin (require (only-in lib [orig-nm tmp]))
(define-ignored nm (contract cnt tmp '#,(syntax->datum #'nm) 'never-happen (quote-syntax nm))))]))
(begin
#`(begin (require (only-in lib [orig-nm tmp]))
(define-ignored nm
(contract cnt
(get-alternate tmp)
'#,(syntax->datum #'nm)
'never-happen
(quote-syntax nm)))))]))