Fold tc/let-values/check into tc/let-values.

Remove printfs.
More metafunctions to handle splitting and merging filter sets.
Handle `delay', `list', `list*'
Implement tc/funapp for the simple case.
Make `id-from' a stxclass.
Shuffle code around so that it compiles.
Type parsing now handles multiple values properly, and has a values and results entry point.

svn: r14680
This commit is contained in:
Sam Tobin-Hochstadt 2009-05-01 21:18:23 +00:00
parent 91f5c26964
commit b4d100d60c
12 changed files with 217 additions and 98 deletions

View File

@ -1,25 +1,31 @@
#lang scheme/base
(provide parse-type parse-type/id parse-type*)
(require (except-in "../utils/utils.ss" extend))
(require (except-in (rep type-rep) make-arr)
(rename-in (types convenience union utils) [make-arr* make-arr])
(utils tc-utils stxclass-util)
syntax/stx
syntax/stx (prefix-in c: scheme/contract)
stxclass stxclass/util
(env type-environments type-name-env type-alias-env lexical-env)
(prefix-in t: "base-types-extra.ss")
scheme/match
(for-template scheme/base "base-types-extra.ss"))
(p/c [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-type* (syntax? . c:-> . Type/c)])
(define enable-mu-parsing (make-parameter #t))
(define (parse-type/id loc datum)
(define ((parse/id p) loc datum)
#;(printf "parse-type/id id : ~a~n ty: ~a~n" (syntax-object->datum loc) (syntax-object->datum stx))
(let* ([stx* (datum->syntax loc datum loc loc)])
(parse-type stx*)))
(p stx*)))
(define (stx-cadr stx) (stx-car (stx-cdr stx)))
@ -322,19 +328,20 @@
[(pred t)
(eq? (syntax-e #'pred) 'pred)
(make-pred-ty (parse-type #'t))]
;; function types
[(dom -> rng : pred-ty)
(and
(eq? (syntax-e #'->) '->)
(eq? (syntax-e #':) ':))
(begin
(add-type-name-reference (stx-cadr stx))
(make-pred-ty (list (parse-type #'dom)) (parse-type #'rng) (parse-type #'pred-ty)))]
(make-pred-ty (list (parse-type #'dom)) (parse-values-type #'rng) (parse-type #'pred-ty)))]
[(dom ... rest ::: -> rng)
(and (eq? (syntax-e #'->) '->)
(eq? (syntax-e #':::) '*))
(begin
(add-type-name-reference #'->)
(->* (map parse-type (syntax->list #'(dom ...))) (parse-type #'rest) (parse-type #'rng)))]
(->* (map parse-type (syntax->list #'(dom ...))) (parse-type #'rest) (parse-values-type #'rng)))]
[(dom ... rest ::: bound -> rng)
(and (eq? (syntax-e #'->) '->)
(eq? (syntax-e #':::) '...)
@ -347,7 +354,7 @@
(make-Function
(list
(make-arr-dots (map parse-type (syntax->list #'(dom ...)))
(parse-type #'rng)
(parse-values-type #'rng)
(parameterize ([current-tvars (extend-env (list (syntax-e #'bound))
(list (make-DottedBoth (make-F (syntax-e #'bound))))
(current-tvars))])
@ -367,7 +374,7 @@
(make-Function
(list
(make-arr-dots (map parse-type (syntax->list #'(dom ...)))
(parse-type #'rng)
(parse-values-type #'rng)
(parameterize ([current-tvars (extend-env (list var)
(list (make-DottedBoth t))
(current-tvars))])
@ -378,40 +385,8 @@
(eq? (syntax-e #'->) '->)
(begin
(add-type-name-reference #'->)
(->* (map parse-type (syntax->list #'(dom ...))) (parse-type #'rng)))]
[(values tys ... dty dd bound)
(and (eq? (syntax-e #'dd) '...)
(identifier? #'bound)
(eq? (syntax-e #'values) 'values))
(let ([var (lookup (current-tvars) (syntax-e #'bound) (lambda (_) #f))])
(if (not (Dotted? var))
(tc-error/stx #'bound "Used a type variable (~a) not bound with ... as a bound on a ..." (syntax-e #'bound))
(make-ValuesDots (map parse-type (syntax->list #'(tys ...)))
(parameterize ([current-tvars (extend-env (list (syntax-e #'bound))
(list (make-DottedBoth (make-F (syntax-e #'bound))))
(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 ...))))]
(->* (map parse-type (syntax->list #'(dom ...))) (parse-values-type #'rng)))]
[(case-lambda tys ...)
(eq? (syntax-e #'case-lambda) 'case-lambda)
(make-Function
@ -459,7 +434,7 @@
[tv (make-Dotted (make-F v))])
(add-type-name-reference #'All)
(parameterize ([current-tvars (extend-env (cons v vars) (cons tv tvars) (current-tvars))])
(make-PolyDots (append vars (list v)) (parse-type #'t))))]
(make-PolyDots (append vars (list v)) (parse-values-type #'t))))]
[(All (vars ...) t)
(and (or (eq? (syntax-e #'All) 'All)
(eq? (syntax-e #'All) '))
@ -468,7 +443,7 @@
[tvars (map make-F vars)])
(add-type-name-reference #'All)
(parameterize ([current-tvars (extend-env vars tvars (current-tvars))])
(make-Poly vars (parse-type #'t))))]
(make-Poly vars (parse-values-type #'t))))]
[(Opaque p?)
(eq? (syntax-e #'Opaque) 'Opaque)
(begin
@ -554,3 +529,45 @@
(string? (syntax-e #'t)))
(-val (syntax-e #'t))]
[_ (tc-error "not a valid type: ~a" (syntax->datum stx))])))
(define (parse-values-type stx)
(parameterize ([current-orig-stx stx])
(syntax-parse stx
[(values tys ... dty :ddd bound:id)
#:when (eq? (syntax-e #'values) 'values)
(let ([var (lookup (current-tvars) (syntax-e #'bound) (lambda (_) #f))])
(if (not (Dotted? var))
(tc-error/stx #'bound "Used a type variable (~a) not bound with ... as a bound on a ..." (syntax-e #'bound))
(make-ValuesDots (map parse-type (syntax->list #'(tys ...)))
(parameterize ([current-tvars (extend-env (list (syntax-e #'bound))
(list (make-DottedBoth (make-F (syntax-e #'bound))))
(current-tvars))])
(parse-type #'dty))
(syntax-e #'bound))))]
[(values tys ... dty :ddd)
#:when (and (eq? (syntax-e #'values) 'values))
(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 ...)
#:when (eq? (syntax-e #'values) 'values)
(-values (map parse-type (syntax->list #'(tys ...))))]
[t
(-values (list (parse-type #'t)))])))
(define (parse-tc-results stx)
(values->tc-results (parse-values-type stx)))
(define parse-tc-results/id (parse/id parse-tc-results))
(define parse-type/id (parse/id parse-type))

View File

@ -58,8 +58,8 @@
(define (pt prop)
#;(print-size prop)
(if (syntax? prop)
(parse-type prop)
(parse-type/id stx prop)))
(parse-tc-results prop)
(parse-tc-results/id stx prop)))
(cond
[(syntax-property stx type-ascrip-symbol) => pt]
[else #f]))

View File

@ -79,6 +79,7 @@ xxx6-y
(: ff (Number -> Number))
(define (ff x) x)
(ff 1)
(lambda: ([y : String][x : Number]) (values 1 x 1))
(lambda: ([x : Number]) (values 1 x 1))
@ -86,4 +87,15 @@ xxx6-y
(lambda () 1)
#{(lambda (x) x) :: (Number -> Number)}
;; BUG - this should work
{ann (values (lambda (x) x) (lambda (x) x)) (values (Number -> Number) (String -> String))}
{ann (values (lambda (x) x) (lambda (x) x)) (values (Number -> Number) (String -> String))}
(list 1 2 3)
(ann (list 1 2 3) (Pair Number (Listof Integer)))
(ann (list 1 2 3) (Listof Integer))
(ann (list 1 2 3) (Listof Number))
(list* 1 2 3)
(ann (list* 1 2 3 (list)) (Pair Number (Listof Integer)))
((lambda (x) 1) 1)
((lambda (x y) 1) 1 2)

View File

@ -39,9 +39,8 @@
[cnt tc/funapp (syntax? syntax? tc-result? (listof tc-results?) (or/c #f tc-results?) . -> . tc-results?)]))
(define-signature tc-let^
([cnt tc/let-values (syntax? syntax? syntax? syntax? . -> . tc-results?)]
([cnt tc/let-values ((syntax? syntax? syntax? syntax?) ((or/c #f tc-results?)) . ->* . tc-results?)]
[cnt tc/letrec-values (syntax? syntax? syntax? syntax? . -> . tc-results?)]
[cnt tc/let-values/check (syntax? syntax? syntax? syntax? tc-results? . -> . tc-results?)]
[cnt tc/letrec-values/check (syntax? syntax? syntax? syntax? tc-results? . -> . tc-results?)]))
(define-signature tc-dots^

View File

@ -1,10 +1,11 @@
#lang scheme/unit
(require (rename-in "../utils/utils.ss" [infer r:infer])
"signatures.ss"
"signatures.ss" "tc-metafunctions.ss"
stxclass scheme/match mzlib/trace
(for-syntax stxclass)
(types utils)
(types utils abbrev)
(utils tc-utils)
(rep type-rep filter-rep object-rep)
(for-template
(only-in '#%kernel [apply k:apply])
@ -20,6 +21,7 @@
#:literals (#%plain-app #%plain-lambda letrec-values
values apply k:apply not list list* call-with-values do-make-object make-object cons
andmap ormap)
;; special case for `values'
[(#%plain-app values arg) (single-value #'arg expected)]
[(#%plain-app values . args)
(match expected
@ -35,7 +37,36 @@
[_ (match-let ([(list (tc-result1: ts fs os) ...)
(for/list ([arg (syntax->list #'args)])
(single-value arg))])
(ret ts fs os))])]))
(ret ts fs os))])]
;; special case for `delay'
[(#%plain-app
mp1
(#%plain-lambda ()
(#%plain-app mp2 (#%plain-app call-with-values (#%plain-lambda () e) list))))
#:declare mp1 (id-from 'make-promise 'scheme/promise)
#:declare mp2 (id-from 'make-promise 'scheme/promise)
(ret (-Promise (tc-expr/t #'e)))]
;; special case for `list'
[(#%plain-app list . args)
(let ([tys (map tc-expr/t (syntax->list #'args))])
(ret (apply -lst* tys)))]
;; special case for `list*'
[(#%plain-app list* . args)
(match-let* ([(list last tys-r ...) (reverse (map tc-expr/t (syntax->list #'args)))]
[tys (reverse tys-r)])
(ret (foldr make-Pair last tys)))]
;; inference for ((lambda
[(#%plain-app (#%plain-lambda (x ...) . body) args ...)
#:when (= (length (syntax->list #'(x ...)))
(length (syntax->list #'(args ...))))
(tc/let-values #'((x) ...) #'(args ...) #'body
#'(let-values ([(x) args] ...) . body)
expected)]
[(#%plain-app f . args)
(let* ([f-ty (single-value #'f)]
[arg-tys (map single-value (syntax->list #'args))])
(tc/funapp #'f #'args f-ty arg-tys expected))]
[_ (int-err "tc/app NYI")]))
;(trace tc/app/internal)
@ -48,6 +79,41 @@
(check-below t expected)
expected)
;; syntax? syntax? tc-result? (listof tc-results?) (or/c #f tc-results) -> tc-results?
(define (object-index os i)
(unless (number? i)
(int-err "object-index for keywords NYI"))
(list-ref os i))
;; in-indexes : Listof[Type] -> Sequence[index/c]
(define (in-indexes dom)
(in-range (length dom)))
;; syntax? syntax? tc-results? (listof tc-results?) (or/c #f tc-results) -> tc-results?
(define (tc/funapp f-stx args-stx ftype0 argtys expected)
(error "tc/funapp NYI"))
(match* (ftype0 argtys)
[((tc-result1: (Function: (list (arr: dom (Values: (list (Result: t-r lf-r lo-r) ...)) #f #f '()))))
(list (tc-result1: t-a phi-a o-a) ...))
(unless (= (length dom) (length t-a))
(tc-error/expr #:return (ret t-r)
"Wrong number of arguments"))
(for ([dom-t (in-list dom)] [arg-t (in-list t-a)])
(check-below arg-t dom-t))
(let* (;; Listof[Listof[LFilterSet]]
[lfs-f (for/list ([lf lf-r])
(for/list ([i (in-indexes dom)])
(split-lfilters lf i)))]
;; Listof[FilterSet]
[f-r (for/list ([lfs lfs-f])
(merge-filter-sets (for/list ([lf lfs] [t t-a] [o o-a])
(apply-filter lf t o))))]
;; Listof[Object]
[o-r (for/list ([lo lo-r])
(match lo
[(LPath: pi* i)
(match (object-index o-a i)
[(Path: pi x) (make-Path (append pi* pi) x)]
[_ (make-Empty)])]
[_ (make-Empty)]))])
(ret t-r f-r o-r))]
[(_ _)
(int-err "funapp with keyword/rest args NYI")]))

View File

@ -238,7 +238,7 @@
(tc/send #'rcvr #'meth #'(args ...) expected)]
;; let
[(let-values ([(name ...) expr] ...) . body)
(tc/let-values/check #'((name ...) ...) #'(expr ...) #'body form expected)]
(tc/let-values #'((name ...) ...) #'(expr ...) #'body form expected)]
[(letrec-values ([(name ...) expr] ...) . body)
(tc/letrec-values/check #'((name ...) ...) #'(expr ...) #'body form expected)]
;; other
@ -340,7 +340,7 @@
(int-err "bad form input to tc-expr: ~a" form))
;; typecheck form
(let ([ty (cond [(type-ascription form) => (lambda (ann)
(tc-expr/check/type form ann))]
(tc-expr/check form ann))]
[else (internal-tc-expr form)])])
(match ty
[(tc-results: ts fs os)

View File

@ -11,7 +11,7 @@
(rename-in (types convenience utils union)
[make-arr* make-arr])
(private type-annotation)
(types abbrev)
(types abbrev utils)
(env type-environments lexical-env)
(utils tc-utils)
mzlib/plt-match)
@ -68,7 +68,6 @@
arg-list arg-types
(make lam-result (map list arg-list arg-types) null rest-ty drest
(tc-exprs/check (syntax->list body) ret-ty))))
(printf "arg-types old new: ~a ~a~n" arg-tys arg-types)
(when (or (not (= arg-len tys-len))
(and rest (and (not rest-ty)
(not drest))))
@ -199,7 +198,6 @@
(match expected
[(tc-result1: (Mu: _ _)) (loop (unfold expected))]
[(tc-result1: (Function: (list (arr: argss rets rests drests '()) ...)))
(printf "expe: ~a~n" expected)
(for/list ([args argss] [ret rets] [rest rests] [drest drests])
(tc/lambda-clause/check (car (syntax->list formals)) (car (syntax->list bodies)) args (values->tc-results ret) rest drest))]
[_ (go (syntax->list formals) (syntax->list bodies) null null null)]))]

View File

@ -119,7 +119,7 @@
(-> expected))]
[_ (tc-expr/t e)]))
(define (tc/let-values/internal namess exprs body form expected)
(define (tc/let-values namess exprs body form [expected #f])
(let* (;; a list of each name clause
[names (map syntax->list (syntax->list namess))]
;; all the trailing expressions - the ones actually bound to the names
@ -133,12 +133,4 @@
[clauses (syntax-case form () [(lv cl . b) (syntax->list #'cl)])])
(do-check void names types form types body clauses expected)))
(define (tc/let-values/check namess exprs body form expected)
(tc/let-values/internal namess exprs body form expected))
(define (tc/let-values namess exprs body form)
(tc/let-values/internal namess exprs body form #f))
;(trace tc/letrec-values/internal)

View File

@ -10,7 +10,8 @@
stxclass/util
(for-syntax scheme/base))
(provide combine-filter apply-filter abstract-filter abstract-filters)
(provide combine-filter apply-filter abstract-filter abstract-filters
split-lfilters merge-filter-sets)
;; this implements the sequence invariant described on the first page relating to Bot
(define (lcombine l1 l2)
@ -57,7 +58,7 @@
[(Path: p (lookup: idx)) (make-LPath p idx)]
[_ (make-LEmpty)]))
(define/contract (abstract-filter ids keys fs)
(d/c (abstract-filter ids keys fs)
(-> (listof identifier?) (listof index/c) FilterSet? LFilterSet?)
(match fs
[(FilterSet: f+ f-)
@ -65,7 +66,7 @@
(apply append (for/list ([f f+]) (abo ids keys f)))
(apply append (for/list ([f f-]) (abo ids keys f))))]))
(define/contract (abo xs idxs f)
(d/c (abo xs idxs f)
(-> (listof identifier?) (listof index/c) Filter/c (or/c '() (list/c LatentFilter/c)))
(define (lookup y)
(for/first ([x xs] [i idxs] #:when (free-identifier=? x y)) i))
@ -78,7 +79,12 @@
[(NotTypeFilter: t p (lookup: idx)) (list (make-LNotTypeFilter t p idx))]
[_ null]))
(define/contract (apply-filter lfs t o)
(define (merge-filter-sets fs)
(match fs
[(list (FilterSet: f+ f-) ...)
(make-FilterSet (apply append f+) (apply append f-))]))
(d/c (apply-filter lfs t o)
(-> LFilterSet? Type/c Object? FilterSet?)
(match lfs
[(LFilterSet: lf+ lf-)
@ -86,7 +92,7 @@
(apply append (for/list ([lf lf+]) (apo lf t o)))
(apply append (for/list ([lf lf-]) (apo lf t o))))]))
(define/contract (apo lf s o)
(d/c (apo lf s o)
(-> LatentFilter/c Type/c Object? (or/c '() (list/c Filter/c)))
(match* (lf s o)
[((LBot:) _ _) (list (make-Bot))]
@ -96,12 +102,23 @@
[((LTypeFilter: t pi* _) _ (Path: pi x)) (list (make-TypeFilter t (append pi* pi) x))]
[((LNotTypeFilter: t pi* _) _ (Path: pi x)) (list (make-NotTypeFilter t (append pi* pi) x))]))
(define/contract (split-lfilters lf idx)
(LFilterSet? index/c . -> . LFilterSet?)
(define (idx= lf)
(match lf
[(LBot:) #t]
[(LNotTypeFilter: _ _ idx*) (type-equal? idx* idx)]
[(LTypeFilter: _ _ idx*) (type-equal? idx* idx)]))
(match lf
[(LFilterSet: lf+ lf-)
(make-LFilterSet (filter idx= lf+) (filter idx= lf-))]))
(define-match-expander T-FS:
(lambda (stx) #'(FilterSet: _ (list (Bot:)))))
(define-match-expander F-FS:
(lambda (stx) #'(FilterSet: (list (Bot:)) _)))
(define/contract (combine-filter f1 f2 f3)
(d/c (combine-filter f1 f2 f3)
(FilterSet? FilterSet? FilterSet? . -> . FilterSet?)
(match* (f1 f2 f3)
[(f (T-FS:) (F-FS:)) f] ;; the student expansion

View File

@ -262,19 +262,4 @@
(make-Function (list (make-arr* (append args (take opt-args i)) result))))))
(define-syntax-rule (->opt args ... [opt ...] res)
(opt-fn (list args ...) (list opt ...) res))
(define (tc-results->values tc)
(match tc
[(tc-results: ts fs os dty dbound)
(make-ValuesDots (map -result ts fs os) dty dbound)]
[(tc-results: ts fs os)
(make-Values (map -result ts fs os))]))
;; FIXME - this should really be a new metafunction like abstract-filter
(define (values->tc-results tc)
(match tc
[(ValuesDots: (list (Result: ts fs os)) dty dbound)
(int-err "values->tc-results NYI for Dots")]
[(Values: (list (Result: ts fs os)))
(ret ts)]))
(opt-fn (list args ...) (list opt ...) res))

View File

@ -30,7 +30,9 @@
just-Dotted?
tc-error/expr
lookup-fail
lookup-type-fail)
lookup-type-fail
values->tc-results
tc-results->values)
;; substitute : Type Name Type -> Type
@ -192,10 +194,13 @@
(define ret
(case-lambda [(t)
(make-tc-results
(if (Type? t)
(list (make-tc-result t (make-FilterSet null null) (make-Empty)))
(for/list ([i t])
(make-tc-result i (make-FilterSet null null) (make-Empty))))
(cond [(Type? t)
(list (make-tc-result t (make-FilterSet null null) (make-Empty)))]
[(or (Values? t) (ValuesDots? t))
(values->tc-results t)]
[else
(for/list ([i t])
(make-tc-result i (make-FilterSet null null) (make-Empty)))])
#f)]
[(t f)
(make-tc-results
@ -221,7 +226,7 @@
(p/c
[ret
(->d ([t (or/c Type/c (listof Type/c))])
(->d ([t (or/c Type/c (listof Type/c) Values? ValuesDots?)])
([f (if (list? t)
(listof FilterSet?)
FilterSet?)]
@ -278,3 +283,18 @@
(define (lookup-type-fail i)
(tc-error/expr "~a is not bound as a type" (syntax-e i)))
(define (tc-results->values tc)
(match tc
[(tc-results: ts fs os dty dbound)
(make-ValuesDots (map make-Result ts fs os) dty dbound)]
[(tc-results: ts fs os)
(make-Values (map make-Result ts fs os))]))
;; FIXME - this should really be a new metafunction like abstract-filter
(define (values->tc-results tc)
(match tc
[(ValuesDots: (list (Result: ts fs os)) dty dbound)
(int-err "values->tc-results NYI for Dots")]
[(Values: (list (Result: ts fs os) ...))
(ret ts)]))

View File

@ -6,7 +6,7 @@ don't depend on any other portion of the system
|#
(provide (all-defined-out))
(require "syntax-traversal.ss" (for-syntax scheme/base stxclass) scheme/match)
(require "syntax-traversal.ss" stxclass (for-syntax scheme/base stxclass) scheme/match)
;; a parameter representing the original location of the syntax being currently checked
(define current-orig-stx (make-parameter #'here))
@ -168,4 +168,17 @@ don't depend on any other portion of the system
e))))
(syntax-parse stx
[(_ e:spec ...)
#'(list (list e.id e.ty) ...)]))
#'(list (list e.id e.ty) ...)]))
;; id: identifier
;; sym: a symbol
;; mod: a quoted require spec like 'scheme/base
;; is id the name sym defined in mod?
(define (id-from? id sym mod)
(and (eq? (syntax-e id) sym)
(eq? (module-path-index-resolve (syntax-source-module id))
((current-module-name-resolver) mod #f #f #f))))
(define-syntax-class (id-from sym mod)
(pattern i:id
#:when (id-from? #'i sym mod)))