From e4997f6176afa79266867681172658a4ba92bb4e Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Tue, 5 May 2009 23:03:02 +0000 Subject: [PATCH] Remove `make-arr/values' Accessors now have appropriate latent objects Handle function application for unions, error, mu, parameters svn: r14724 original commit: 07341c605b9660333444665265a4fb3104efdc6e --- collects/typed-scheme/env/init-envs.ss | 5 +- collects/typed-scheme/private/base-env.ss | 4 +- collects/typed-scheme/test2.ss | 12 +++++ collects/typed-scheme/typecheck/tc-app.ss | 49 ++++++++++++++----- collects/typed-scheme/typecheck/tc-envops.ss | 22 ++++++--- .../typed-scheme/typecheck/tc-lambda-unit.ss | 2 +- collects/typed-scheme/typecheck/tc-structs.ss | 10 +++- collects/typed-scheme/types/abbrev.ss | 13 ----- collects/typed-scheme/types/resolve.ss | 5 +- 9 files changed, 83 insertions(+), 39 deletions(-) diff --git a/collects/typed-scheme/env/init-envs.ss b/collects/typed-scheme/env/init-envs.ss index 02981069..4b87fadc 100644 --- a/collects/typed-scheme/env/init-envs.ss +++ b/collects/typed-scheme/env/init-envs.ss @@ -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))) diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss index 17e73dbf..7e8b742b 100644 --- a/collects/typed-scheme/private/base-env.ss +++ b/collects/typed-scheme/private/base-env.ss @@ -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 diff --git a/collects/typed-scheme/test2.ss b/collects/typed-scheme/test2.ss index d895c3b5..a4305927 100644 --- a/collects/typed-scheme/test2.ss +++ b/collects/typed-scheme/test2.ss @@ -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") diff --git a/collects/typed-scheme/typecheck/tc-app.ss b/collects/typed-scheme/typecheck/tc-app.ss index eee6b699..43b4ba8d 100644 --- a/collects/typed-scheme/typecheck/tc-app.ss +++ b/collects/typed-scheme/typecheck/tc-app.ss @@ -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? diff --git a/collects/typed-scheme/typecheck/tc-envops.ss b/collects/typed-scheme/typecheck/tc-envops.ss index 292391ed..a96e1b42 100644 --- a/collects/typed-scheme/typecheck/tc-envops.ss +++ b/collects/typed-scheme/typecheck/tc-envops.ss @@ -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 Γ)]))) diff --git a/collects/typed-scheme/typecheck/tc-lambda-unit.ss b/collects/typed-scheme/typecheck/tc-lambda-unit.ss index 59080124..48f5a6e9 100644 --- a/collects/typed-scheme/typecheck/tc-lambda-unit.ss +++ b/collects/typed-scheme/typecheck/tc-lambda-unit.ss @@ -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) diff --git a/collects/typed-scheme/typecheck/tc-structs.ss b/collects/typed-scheme/typecheck/tc-structs.ss index 395a82bd..c388b8b7 100644 --- a/collects/typed-scheme/typecheck/tc-structs.ss +++ b/collects/typed-scheme/typecheck/tc-structs.ss @@ -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))) diff --git a/collects/typed-scheme/types/abbrev.ss b/collects/typed-scheme/types/abbrev.ss index 1b785e17..7ec654ed 100644 --- a/collects/typed-scheme/types/abbrev.ss +++ b/collects/typed-scheme/types/abbrev.ss @@ -169,19 +169,6 @@ (make-Values (list (-result rng filters obj)))) rest drest (sort #:key Keyword-kw kws keyword* ((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* (syntax-rules (:) [(_ dom rng) diff --git a/collects/typed-scheme/types/resolve.ss b/collects/typed-scheme/types/resolve.ss index 7a132543..520cc444 100644 --- a/collects/typed-scheme/types/resolve.ss +++ b/collects/typed-scheme/types/resolve.ss @@ -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))