suzanne.soy/typed-racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

sync ts to trunk

Browse Source 
svn: r14257

original commit: fcc2a24545b0b4f71052457acdf8097f084a4b27
This commit is contained in:
Sam Tobin-Hochstadt 2009-03-25 01:07:34 +00:00
parent d8ac05e077
commit fc897da813
9 changed files with 184 additions and 22 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
collects/typed-scheme/env/type-environments.ss vendored
View File

@ -10,6 +10,9 @@
dotted-env
initial-tvar-env
env-map
env-filter
env-vals
env-keys+vals
with-dotted-env/extend)
(require (prefix-in r: "../utils/utils.ss"))
@ -19,6 +22,17 @@
;; eq? has the type of equal?, and l is an alist (with conses!)
(define-struct env (eq? l))
(define (env-vals e)
(map cdr (env-l e)))
(define (env-keys+vals e)
(env-l e))
(define (env-filter f e)
(match e
[(struct env (eq? l))
(make-env eq? (filter f l))]))
;; the initial type variable environment - empty
;; this is used in the parsing of types
(define initial-tvar-env (make-env eq? '()))

39
collects/typed-scheme/private/base-env.ss
View File

@ -102,10 +102,14 @@
[fold-right (-polydots (c a b) ((list ((list c a) (b b) . ->... . c) c (-lst a))
((-lst b) b) . ->... . c))]
[foldl
(-poly (a b c)
(-poly (a b c d)
(cl-> [((a b . -> . b) b (-lst a)) b]
[((a b c . -> . c) c (-lst a) (-lst b)) c]))]
[foldr (-poly (a b c) ((a b . -> . b) b (-lst a) . -> . b))]
[((a b c . -> . c) c (-lst a) (-lst b)) c]
[((a b c d . -> . d) d (-lst a) (-lst b) (-lst d)) d]))]
[foldr (-poly (a b c d)
(cl-> [((a b . -> . b) b (-lst a)) b]
[((a b c . -> . c) c (-lst a) (-lst b)) c]
[((a b c d . -> . d) d (-lst a) (-lst b) (-lst d)) d]))]
[filter (-poly (a b) (cl->*
((make-pred-ty (list a) B b)
(-lst a)
@ -537,6 +541,10 @@
[maybe-print-message (-String . -> . -Void)]
[list->string ((-lst -Char) . -> . -String)]
[string->list (-String . -> . (-lst -Char))]
[sort (-poly (a) ((-lst a) (a a . -> . B) . -> . (-lst a)))]
;; scheme/list
[last-pair (-poly (a) ((-mu x (Un a (-val '()) (-pair a x)))
. -> .
@ -567,3 +575,28 @@
[real->decimal-string (N [-Nat] . ->opt . -String)]
[current-continuation-marks (-> -Cont-Mark-Set)]
;; scheme/path
[explode-path (-Pathlike . -> . (-lst (Un -Path (-val 'up) (-val 'same))))]
[find-relative-path (-Pathlike -Pathlike . -> . -Path)]
[simple-form-path (-Pathlike . -> . -Path)]
[normalize-path (cl->* (-Pathlike . -> . -Path)
(-Pathlike -Pathlike . -> . -Path))]
[filename-extension (-Pathlike . -> . (-opt -Bytes))]
[file-name-from-path (-Pathlike . -> . (-opt -Path))]
[path-only (-Pathlike . -> . -Path)]
[some-system-path->string (-Path . -> . -String)]
[string->some-system-path
(-String (Un (-val 'unix) (-val 'windows)) . -> . -Path)]
;; scheme/math
[sgn (-Real . -> . -Real)]
[pi N]
[sqr (N . -> . N)]
[sgn (N . -> . N)]
[conjugate (N . -> . N)]
[sinh (N . -> . N)]
[cosh (N . -> . N)]
[tanh (N . -> . N)]

37
collects/typed-scheme/private/parse-type.ss
View File

@ -346,6 +346,26 @@
(current-tvars))])
(parse-type #'rest))
(syntax-e #'bound)))))))]
[(dom ... rest ::: -> rng)
(and (eq? (syntax-e #'->) '->)
(eq? (syntax-e #':::) '...))
(begin
(add-type-name-reference #'->)
(let ([bounds (filter (compose Dotted? cdr) (env-keys+vals (current-tvars)))])
(when (null? bounds)
(tc-error/stx stx "No type variable bound with ... in scope for ... type"))
(unless (null? (cdr bounds))
(tc-error/stx stx "Cannot infer bound for ... type"))
(match-let ([(cons var (struct Dotted (t))) (car bounds)])
(make-Function
(list
(make-arr-dots (map parse-type (syntax->list #'(dom ...)))
(parse-type #'rng)
(parameterize ([current-tvars (extend-env (list var)
(list (make-DottedBoth t))
(current-tvars))])
(parse-type #'rest))
var))))))]
;; has to be below the previous one
[(dom ... -> rng)
(eq? (syntax-e #'->) '->)
@ -365,6 +385,23 @@
(current-tvars))])
(parse-type #'dty))
(syntax-e #'bound))))]
[(values tys ... dty dd)
(and (eq? (syntax-e #'values) 'values)
(eq? (syntax-e #'dd) '...))
(begin
(add-type-name-reference #'values)
(let ([bounds (filter (compose Dotted? cdr) (env-keys+vals (current-tvars)))])
(when (null? bounds)
(tc-error/stx stx "No type variable bound with ... in scope for ... type"))
(unless (null? (cdr bounds))
(tc-error/stx stx "Cannot infer bound for ... type"))
(match-let ([(cons var (struct Dotted (t))) (car bounds)])
(make-ValuesDots (map parse-type (syntax->list #'(tys ...)))
(parameterize ([current-tvars (extend-env (list var)
(list (make-DottedBoth t))
(current-tvars))])
(parse-type #'dty))
var))))]
[(values tys ...)
(eq? (syntax-e #'values) 'values)
(-values (map parse-type (syntax->list #'(tys ...))))]

33
collects/typed-scheme/private/type-contract.ss
View File

@ -17,7 +17,7 @@
mzlib/trace
scheme/list
(only-in scheme/contract -> ->* case-> cons/c flat-rec-contract provide/contract any/c)
(for-template scheme/base scheme/contract (only-in scheme/class object% is-a?/c subclass?/c)))
(for-template scheme/base scheme/contract (utils poly-c) (only-in scheme/class object% is-a?/c subclass?/c)))
(define (define/fixup-contract? stx)
(or (syntax-property stx 'typechecker:contract-def)
@ -51,7 +51,9 @@
(define (type->contract ty fail)
(define vars (make-parameter '()))
(let/cc exit
(let t->c ([ty ty])
(let loop ([ty ty] [pos? #t])
(define (t->c t) (loop t pos?))
(define (t->c/neg t) (loop t (not pos?)))
(match ty
[(or (App: _ _ _) (Name: _)) (t->c (resolve-once ty))]
[(Univ:) #'any/c]
@ -71,13 +73,13 @@
(define-values (dom* rngs* rst)
(match a
[(arr: dom (Values: rngs) #f #f '())
(values (map t->c dom) (map t->c rngs) #f)]
(values (map t->c/neg dom) (map t->c rngs) #f)]
[(arr: dom rng #f #f '())
(values (map t->c dom) (list (t->c rng)) #f)]
(values (map t->c/neg dom) (list (t->c rng)) #f)]
[(arr: dom (Values: rngs) rst #f '() )
(values (map t->c dom) (map t->c rngs) (t->c rst))]
(values (map t->c/neg dom) (map t->c rngs) (t->c/neg rst))]
[(arr: dom rng rst #f '())
(values (map t->c dom) (list (t->c rng)) (t->c rst))]))
(values (map t->c/neg dom) (list (t->c rng)) (t->c/neg rst))]))
(with-syntax
([(dom* ...) dom*]
[rng* (match rngs*
@ -99,12 +101,22 @@
#`(cons/c #,(t->c t1) #,(t->c t2))]
[(Opaque: p? cert)
#`(flat-contract #,(cert p?))]
[(F: v) (cond [(assoc v (vars)) => cadr]
[(F: v) (cond [(assoc v (vars)) => (if pos? second third)]
[else (int-err "unknown var: ~a" v)])]
[(Poly: vs (and b (Function: _)))
(match-let ([(Poly-names: vs-nm _) ty])
(with-syntax ([(vs+ ...) (generate-temporaries (for/list ([v vs-nm]) (symbol-append v '+)))]
[(vs- ...) (generate-temporaries (for/list ([v vs-nm]) (symbol-append v '-)))])
(parameterize ([vars (append (map list
vs
(syntax->list #'(vs+ ...))
(syntax->list #'(vs- ...)))
(vars))])
#`(poly/c ([vs- vs+] ...) #,(t->c b)))))]
[(Mu: n b)
(match-let ([(Mu-name: n-nm _) ty])
(with-syntax ([(n*) (generate-temporaries (list n-nm))])
(parameterize ([vars (cons (list n #'n*) (vars))])
(parameterize ([vars (cons (list n #'n* #'n*) (vars))])
#`(flat-rec-contract n* #,(t->c b)))))]
[(Value: #f) #'false/c]
[(Instance: _) #'(is-a?/c object%)]
@ -112,10 +124,7 @@
[(Value: '()) #'null?]
[(Struct: _ _ _ _ #f pred? cert) (cert pred?)]
[(Syntax: (Base: 'Symbol _)) #'identifier?]
[(Syntax: t)
(if (equal? ty t:Any-Syntax)
#`syntax?
#`(syntax/c #,(t->c t)))]
[(Syntax: t) #`(syntax/c #,(t->c t))]
[(Value: v) #`(flat-named-contract #,(format "~a" v) (lambda (x) (equal? x '#,v)))]
[(Param: in out) #`(parameter/c #,(t->c out))]
[(Hashtable: k v) #`hash?]

53
collects/typed-scheme/ts-reference.scrbl
View File

@ -1,7 +1,10 @@
#lang scribble/doc
@begin[(require scribble/manual)
(require (for-label typed-scheme))]
@begin[(require scribble/manual scribble/eval
scheme/sandbox)
(require (for-label typed-scheme
scheme/list srfi/14
version/check))]
@begin[
(define (item* header . args) (apply item @bold[header]{: } args))
@ -52,6 +55,8 @@ The following base types are parameteric in their type arguments.
the first is the type the parameter accepts, and the second is the type returned.}
@defform[(Pair s t)]{is the pair containing @scheme[s] as the @scheme[car]
and @scheme[t] as the @scheme[cdr]}
@defform[(HashTable k v)]{is the type of a @rtech{hash table} with key type
@scheme[k] and value type @scheme[v].}
@subsubsub*section{Type Constructors}
@ -245,3 +250,47 @@ known to Typed Scheme, either via @scheme[define-struct:] or
Like @scheme[do], but each @scheme[id] having the associated type @scheme[t], and
the final body @scheme[expr] having the type @scheme[u].
}
@section{Libraries Provided With Typed Scheme}
The @schememodname[typed-scheme] language corresponds to the
@schememodname[scheme/base] language---that is, any identifier provided
by @schememodname[scheme/base], such as @scheme[mod] is available by default in
@schememodname[typed-scheme].
@schememod[typed-scheme
(modulo 12 2)
]
Any value provided by @schememodname[scheme] is available by simply
@scheme[require]ing it; use of @scheme[require/typed] is not
neccessary.
@schememod[typed-scheme
(require scheme/list)
(display (first (list 1 2 3)))
]
Some libraries have counterparts in the @schemeidfont{typed}
collection, which provide the same exports as the untyped versions.
Such libraries include @schememodname[srfi/14],
@schememodname[net/url], and many others.
@schememod[typed-scheme
(require typed/srfi/14)
(char-set= (string->char-set "hello")
(string->char-set "olleh"))
]
To participate in making more libraries available, please visit
@link["http://www.ccs.neu.edu/home/samth/adapt/"]{here}.
Other libraries can be used with Typed Scheme via
@scheme[require/typed].
@schememod[typed-scheme
(require/typed version/check
[check-version (-> (U Symbol (Listof Any)))])
(check-version)
]

12
collects/typed-scheme/typecheck/provide-handling.ss
View File

@ -54,15 +54,18 @@
(define/contract cnt-id #,cnt id)
(define-syntax export-id
(if (unbox typed-context?)
(make-rename-transformer #'id)
(make-rename-transformer #'cnt-id)))
(make-rename-transformer (syntax-property #'id
'not-free-identifier=? #t))
(make-rename-transformer (syntax-property #'cnt-id
'not-free-identifier=? #t))))
(#%provide (rename export-id out-id)))))]
[else
(with-syntax ([(export-id) (generate-temporaries #'(id))])
#`(begin
(define-syntax export-id
(if (unbox typed-context?)
(make-rename-transformer #'id)
(make-rename-transformer (syntax-property #'id
'not-free-identifier=? #t))
(lambda (stx) (tc-error/stx stx "The type of ~a cannot be converted to a contract" (syntax-e #'id)))))
(provide (rename-out [export-id out-id]))))])))]
[(mem? internal-id stx-defs)
@ -76,7 +79,8 @@
(if (unbox typed-context?)
(begin
(add-alias #'export-id #'id)
(make-rename-transformer #'id))
(make-rename-transformer (syntax-property #'id
'not-free-identifier=? #t)))
(lambda (stx)
(tc-error/stx stx "Macro ~a from typed module used in untyped code" (syntax-e #'out-id)))))
(provide (rename-out [export-id out-id]))))))]

13
collects/typed-scheme/typecheck/tc-app-unit.ss
View File

@ -342,6 +342,19 @@
drest-bound
(subst-all (alist-delete drest-bound substitution eq?)
(car rngs*)))))]
;; ... function, (List A B C etc) arg
[(and (car drests*)
(not tail-bound)
(eq? (cdr (car drests*)) dotted-var)
(= (length (car doms*))
(length arg-tys))
(untuple tail-ty)
(infer/dots fixed-vars dotted-var (append arg-tys (untuple tail-ty)) (car doms*)
(car (car drests*)) (car rngs*) (fv (car rngs*))))
=> (lambda (substitution)
(define drest-bound (cdr (car drests*)))
(do-apply-log substitution 'dots 'dots)
(ret (subst-all substitution (car rngs*))))]
;; if nothing matches, around the loop again
[else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))]
[(tc-result: (PolyDots: vars (Function: '())))

1
collects/typed-scheme/types/abbrev.ss
View File

@ -96,6 +96,7 @@
(define Err (make-Error))
(define -Nat -Integer)
(define -Real -Number)
(define Any-Syntax
(-mu x

4
collects/typed-scheme/utils/utils.ss
View File

@ -20,7 +20,9 @@ at least theoretically.
in-list-forever
extend
debug
in-syntax)
in-syntax
symbol-append
rep utils typecheck infer env private)
(define-syntax (define-requirer stx)
(syntax-parse stx