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

Remove `make-arr/values'

Browse Source 
Accessors now have appropriate latent objects
Handle function application for unions, error, mu, parameters

svn: r14724

original commit: 07341c605b9660333444665265a4fb3104efdc6e
This commit is contained in:
Sam Tobin-Hochstadt 2009-05-05 23:03:02 +00:00
parent dfcd59c8fa
commit e4997f6176
9 changed files with 83 additions and 39 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
collects/typed-scheme/env/init-envs.ss vendored
View File

@ -5,7 +5,7 @@
(require "type-env.ss"
"type-name-env.ss"
"type-alias-env.ss"
(rep type-rep object-rep filter-rep)
(rep type-rep object-rep filter-rep rep-utils)
(for-template (rep type-rep object-rep filter-rep)
(types union)
mzlib/pconvert mzlib/shared scheme/base)
@ -36,7 +36,8 @@
[(Poly-names: ns b) `(make-Poly (list ,@(map sub ns)) ,(sub b))]
[(PolyDots-names: ns b) `(make-PolyDots (list ,@(map sub ns)) ,(sub b))]
[(? (lambda (e) (or (LatentFilter? e)
(LatentObject? e)))
(LatentObject? e)
(PathElem? e)))
(app (lambda (v) (vector->list (struct->vector v))) (list-rest tag seq vals)))
`(,(gen-constructor tag) ,@(map sub vals))]
[(? (lambda (e) (or (Type? e)))

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

@ -250,7 +250,7 @@
[apply (-poly (a b) (((list) a . ->* . b) (-lst a) . -> . b))]
[kernel:apply (-poly (a b) (((list) a . ->* . b) (-lst a) . -> . b))]
[time-apply (-polydots (b a) (make-arr/values
[time-apply (-polydots (b a) (make-arr
(list ((list) (a a) . ->... . b)
(-lst a))
(-values (list (-pair b (-val '())) N N N))))]
@ -261,7 +261,7 @@
[quotient (-Integer -Integer . -> . -Integer)]
[remainder (-Integer -Integer . -> . -Integer)]
[quotient/remainder
(make-arr/values (list -Integer -Integer) (-values (list -Integer -Integer)))]
(make-arr (list -Integer -Integer) (-values (list -Integer -Integer)))]
;; parameter stuff

12
collects/typed-scheme/test2.ss
View File

@ -19,6 +19,18 @@
(+)
(+ 1 2 3)
(+ 1 2 3.5)
#|
(define-struct: (Z) x ([y : Z]))
(define: my-x : (x Number) (make-x 1))
(number? (x-y my-x))
(if (number? (x-y my-x)) (+ 1 (x-y my-x)) 7)
|#
(define: (f2) : (U) (error 'foo))
(lambda: ([x : Number]) #{((f2)) :: (U)})
(: f3 (U (Number -> Number) (Number -> String)))
(define (f3 x) 7)
;(f 12 "hi")

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

@ -5,7 +5,7 @@
"tc-app-helper.ss"
stxclass scheme/match mzlib/trace
(for-syntax stxclass)
(types utils abbrev union subtype)
(types utils abbrev union subtype resolve)
(utils tc-utils)
(rep type-rep filter-rep object-rep)
(for-template
@ -95,17 +95,44 @@
[((tc-result1: (and t (Function: (list (and a (arr: dom (Values: (list (Result: t-r lf-r lo-r) ...)) rest #f kws))))))
argtys)
(tc/funapp1 f-stx args-stx a argtys expected)]
[((tc-result1: (and t (Function: (and arrs (list (arr: doms rngs rests #f kws) ...)))))
[((tc-result1: (and t (Function: (and arrs (list (arr: doms rngs rests (and drests #f) kws) ...)))))
(and argtys (list (tc-result1: argtys-t) ...)))
(let loop ([doms* doms] [rngs rngs] [rests* rests] [a arrs])
(cond [(null? doms*)
(tc-error/expr
#:return (or expected (ret (Un)))
(string-append "No function domains matched in function application:\n"
(domain-mismatches t doms rests #f rngs argtys #f #f)))]
[(subtypes/varargs argtys-t (car doms*) (car rests*))
(tc/funapp1 f-stx args-stx (car a) argtys expected #:check #f)]
[else (loop (cdr doms*) (cdr rngs) (cdr rests*) (cdr a))]))]))
(or
;; find the first function where the argument types match
(for/first ([dom doms] [rng rngs] [rest rests] [a arrs]
#:when (subtypes/varargs argtys-t dom rest))
;; then typecheck here
;; we call the separate function so that we get the appropriate filters/objects
(tc/funapp1 f-stx args-stx a argtys expected #:check #f))
;; if nothing matched, error
(tc-error/expr
#:return (or expected (ret (Un)))
(string-append "No function domains matched in function application:\n"
(domain-mismatches t doms rests drests rngs argtys-t #f #f))))]
;; parameters are functions too
[((tc-result1: (Param: in out)) (list)) (ret out)]
[((tc-result1: (Param: in out)) (list (tc-result1: t)))
(if (subtype t in)
(ret -Void true-filter)
(tc-error/expr #:return (ret -Void true-filter)
"Wrong argument to parameter - expected ~a and got ~a" in t))]
[((tc-result1: (Param: _ _)) _)
(tc-error/expr #:return (ret (Un))
"Wrong number of arguments to parameter - expected 0 or 1, got ~a"
(length argtys))]
;; resolve names, polymorphic apps, mu, etc
[((tc-result1: (? needs-resolving? t) f o) _)
(tc/funapp f-stx args-stx (ret (resolve-once t) f o) argtys expected)]
;; a union of functions can be applied if we can apply all of the elements
[((tc-result1: (Union: (and ts (list (Function: _) ...)))) _)
(ret (for/fold ([result (Un)]) ([fty ts])
(match (tc/funapp f-stx args-stx (ret fty) argtys expected)
[(tc-result1: t) (Un result t)])))]
;; error type is a perfectly good fcn type
[((tc-result1: (Error:)) _) (ret (make-Error))]
;; otherwise fail
[((tc-result1: f-ty) _) (tc-error/expr #:return (ret (Un))
"Cannot apply expression of type ~a, since it is not a function type" f-ty)]))
;; syntax? syntax? arr? (listof tc-results?) (or/c #f tc-results) [boolean?] -> tc-results?

22
collects/typed-scheme/typecheck/tc-envops.ss
View File

@ -7,9 +7,11 @@
[one-of/c -one-of/c])
(infer-in infer)
(rep type-rep)
(utils tc-utils)
(types resolve)
(only-in (env type-environments lexical-env) env? update-type/lexical env-map)
scheme/contract scheme/match
stxclass/util
stxclass/util mzlib/trace
(for-syntax scheme/base))
(provide env+)
@ -19,9 +21,11 @@
[(zero? i) (cons (f (car l)) (cdr l))]
[else (cons (car l) (replace-nth (cdr l) (sub1 i) f))]))
(trace replace-nth)
(define/contract (update t lo)
(Type/c Filter/c . -> . Type/c)
(match* (t lo)
(match* ((resolve t) lo)
;; pair ops
[((Pair: t s) (TypeFilter: u (list* (CarPE:) rst) x))
(make-Pair (update t (make-TypeFilter u rst x)) s)]
@ -34,17 +38,19 @@
;; struct ops
[((Struct: nm par flds proc poly pred cert)
(TypeFilter: u (list* (StructPE: (? (lambda (s) (subtype t s)) s) idx) rst) x))
(make-Struct nm par (replace-nth flds idx (lambda (e) (update e (make-TypeFilter u rst x)))))]
(TypeFilter: u (list* (StructPE: (? (lambda (s) (subtype t s)) s) idx) rst) x))
(make-Struct nm par (replace-nth flds idx (lambda (e) (update e (make-TypeFilter u rst x)))) proc poly pred cert)]
[((Struct: nm par flds proc poly pred cert)
(NotTypeFilter: u (list* (StructPE: (? (lambda (s) (subtype t s)) s) idx) rst) x))
(make-Struct nm par (replace-nth flds idx (lambda (e) (update e (make-NotTypeFilter u rst x)))))]
(make-Struct nm par (replace-nth flds idx (lambda (e) (update e (make-NotTypeFilter u rst x)))) proc poly pred cert)]
;; otherwise
[(t (TypeFilter: u (list) _))
(restrict t u)]
[(t (NotTypeFilter: u (list) _))
(remove t u)]))
(remove t u)]
[(_ _)
(int-err "update along ill-typed path: ~a ~a" t lo)]))
(define/contract (env+ env fs)
(env? (listof Filter/c) . -> . env?)
@ -52,4 +58,6 @@
(match f
[(Bot:) (env-map (lambda (x) (cons (car x) (Un))) Γ)]
[(or (TypeFilter: _ _ x) (NotTypeFilter: _ _ x))
(update-type/lexical (lambda (x t) (update t f)) x Γ)])))
(update-type/lexical (lambda (x t)
(printf "upd: ~a ~a ~a~n" t f (update t f))
(update t f)) x Γ)])))

2
collects/typed-scheme/typecheck/tc-lambda-unit.ss
View File

@ -30,7 +30,7 @@
(define (lam-result->type lr)
(match lr
[(struct lam-result ((list (list arg-ids arg-tys) ...) (list (list kw kw-id kw-ty req?) ...) rest drest body))
(make-arr/values
(make-arr
arg-tys
(abstract-filters (append (for/list ([i (in-naturals)] [_ arg-ids]) i) kw)
(append arg-ids kw-id)

10
collects/typed-scheme/typecheck/tc-structs.ss
View File

@ -3,7 +3,7 @@
(require (except-in "../utils/utils.ss" extend))
(require (rep type-rep)
(private parse-type)
(types convenience utils union resolve)
(types convenience utils union resolve abbrev)
(env type-env type-environments type-name-env)
(utils tc-utils)
"def-binding.ss"
@ -129,7 +129,13 @@
(wrapper (->* external-fld-types (if cret cret name))))
(cons pred
(make-pred-ty (pred-wrapper name))))
(map (lambda (g t) (cons g (wrapper (->* (list name) t)))) getters external-fld-types/no-parent)
(for/list ([g (in-list getters)] [t (in-list external-fld-types/no-parent)] [i (in-naturals)])
(let ([func (if setters?
(->* (list name) t)
(make-Function
(list (make-arr* (list sty) t
#:object (make-LPath (list (make-StructPE name i)) 0)))))])
(cons g (wrapper func))))
(if setters?
(map (lambda (g t) (cons g (wrapper (->* (list name t) -Void)))) setters external-fld-types/no-parent)
null)))

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

@ -169,19 +169,6 @@
(make-Values (list (-result rng filters obj))))
rest drest (sort #:key Keyword-kw kws keyword<?)))
(d/c (make-arr/values dom rng
#:rest [rest #f] #:drest [drest #f] #:kws [kws null]
#:filters [filters -no-lfilter] #:object [obj -no-lobj])
(c:->* ((listof Type/c) (or/c ValuesDots? Values?))
(#:rest (or/c Type/c #f)
#:drest (or/c (cons/c Type/c symbol?) #f)
#:kws (listof Keyword?)
#:filters LFilterSet?
#:object LatentObject?)
arr?)
(make-arr dom rng rest drest (sort #:key Keyword-kw kws keyword<?)))
(define-syntax ->*
(syntax-rules (:)
[(_ dom rng)

5
collects/typed-scheme/types/resolve.ss
View File

@ -8,7 +8,7 @@
scheme/match
mzlib/trace)
(provide resolve-name resolve-app needs-resolving? resolve-once)
(provide resolve-name resolve-app needs-resolving? resolve-once resolve)
(define (resolve-name t)
(match t
@ -33,3 +33,6 @@
[(Mu: _ _) (unfold t)]
[(App: r r* s) (resolve-app r r* s)]
[(Name: _) (resolve-name t)]))
(define (resolve t)
(if (needs-resolving? t) (resolve-once t) t))