Everything now compiles without names

This commit is contained in:
Sam Tobin-Hochstadt 2010-04-19 18:42:25 -04:00
parent df1572231e
commit f57ef37a66
12 changed files with 86 additions and 111 deletions

View File

@ -39,9 +39,8 @@
[(Mu-name: n b) `(make-Mu ,(sub n) ,(sub b))]
[(Poly-names: ns b) `(make-Poly (list ,@(map sub ns)) ,(sub b))]
[(PolyDots-names: ns b) `(make-PolyDots (list ,@(map sub ns)) ,(sub b))]
[(arr: dom rng rest drest kws names)
`(make-arr ,(sub dom) ,(sub rng) ,(sub rest) ,(sub drest) ,(sub kws)
(list ,@(for/list ([i names]) `(quote-syntax ,i))))]
[(arr: dom rng rest drest kws)
`(make-arr ,(sub dom) ,(sub rng) ,(sub rest) ,(sub drest) ,(sub kws))]
[(TypeFilter: t p i)
`(make-TypeFilter ,(sub t) ,(sub p) (quote-syntax ,i))]
[(NotTypeFilter: t p i)

View File

@ -158,8 +158,8 @@
[ret-mapping (cg t s)])
(cset-meet*
(list arg-mapping ret-mapping)))]
[((arr: ts t #f (cons dty dbound) '() names)
(arr: ss s #f #f '() names*))
[((arr: ts t #f (cons dty dbound) '())
(arr: ss s #f #f '()))
(unless (memq dbound X)
(fail! S T))
(unless (<= (length ts) (length ss))
@ -169,11 +169,10 @@
(gensym dbound))]
[new-tys (for/list ([var vars])
(substitute (make-F var) dbound dty))]
[new-names (generate-temporaries new-tys)]
[new-cset (cgen/arr V (append vars X) (make-arr (append ts new-tys) t #f #f null (append names new-names)) s-arr)])
[new-cset (cgen/arr V (append vars X) (make-arr (append ts new-tys) t #f #f null) s-arr)])
(move-vars-to-dmap new-cset dbound vars))]
[((arr: ts t #f #f '())
(arr: ss s #f (cons dty dbound) '() names*))
(arr: ss s #f (cons dty dbound) '()))
(unless (memq dbound X)
(fail! S T))
(unless (<= (length ss) (length ts))
@ -183,8 +182,7 @@
(gensym dbound))]
[new-tys (for/list ([var vars])
(substitute (make-F var) dbound dty))]
[new-names (generate-temporaries new-tys)]
[new-cset (cgen/arr V (append vars X) t-arr (make-arr (append ss new-tys) s #f #f null (append names* new-names)))])
[new-cset (cgen/arr V (append vars X) t-arr (make-arr (append ss new-tys) s #f #f null))])
(move-vars-to-dmap new-cset dbound vars))]
[((arr: ts t #f (cons t-dty dbound) '())
(arr: ss s #f (cons s-dty dbound) '()))
@ -208,7 +206,7 @@
(cset-meet*
(list arg-mapping darg-mapping ret-mapping)))]
[((arr: ts t t-rest #f '())
(arr: ss s #f (cons s-dty dbound) '() names*))
(arr: ss s #f (cons s-dty dbound) '()))
(unless (memq dbound X)
(fail! S T))
(if (<= (length ts) (length ss))
@ -223,9 +221,8 @@
(gensym dbound))]
[new-tys (for/list ([var vars])
(substitute (make-F var) dbound s-dty))]
[new-names (generate-temporaries new-tys)]
[new-cset (cgen/arr V (append vars X) t-arr
(make-arr (append ss new-tys) s #f (cons s-dty dbound) null (append names* new-names)))])
(make-arr (append ss new-tys) s #f (cons s-dty dbound) null))])
(move-vars+rest-to-dmap new-cset dbound vars)))]
;; If dotted <: starred is correct, add it below. Not sure it is.
[((arr: ts t #f (cons t-dty dbound) '())

View File

@ -21,7 +21,7 @@
(define (var-promote T V)
(define (vp t) (var-promote t V))
(define (inv t) (if (V-in? V t) Univ t))
(type-case (#:Type vp #:LatentFilter (sub-lf vp)) T
(type-case (#:Type vp #:Filter (sub-f vp)) T
[#:F name (if (memq name V) Univ T)]
[#:Vector t (make-Vector (inv t))]
[#:Box t (make-Box (inv t))]
@ -32,7 +32,7 @@
[#:Param in out
(make-Param (var-demote in V)
(vp out))]
[#:arr dom rng rest drest kws names
[#:arr dom rng rest drest kws
(cond
[(apply V-in? V (get-filters rng))
(make-top-arr)]
@ -41,8 +41,7 @@
(vp rng)
(var-demote (car drest) V)
#f
(for/list ([k kws]) (var-demote k V))
names)]
(for/list ([k kws]) (var-demote k V)))]
[else
(make-arr (for/list ([d dom]) (var-demote d V))
(vp rng)
@ -50,13 +49,12 @@
(and drest
(cons (var-demote (car drest) V)
(cdr drest)))
(for/list ([k kws]) (var-demote k V))
names)])]))
(for/list ([k kws]) (var-demote k V)))])]))
(define (var-demote T V)
(define (vd t) (var-demote t V))
(define (inv t) (if (V-in? V t) (Un) t))
(type-case (#:Type vd #:LatentFilter (sub-lf vd)) T
(type-case (#:Type vd #:Filter (sub-f vd)) T
[#:F name (if (memq name V) (Un) T)]
[#:Vector t (make-Vector (inv t))]
[#:Box t (make-Box (inv t))]
@ -67,7 +65,7 @@
[#:Param in out
(make-Param (var-promote in V)
(vd out))]
[#:arr dom rng rest drest kws names
[#:arr dom rng rest drest kws
(cond
[(apply V-in? V (get-filters rng))
(make-top-arr)]
@ -76,8 +74,7 @@
(vd rng)
(var-promote (car drest) V)
#f
(for/list ([k kws]) (var-demote k V))
names)]
(for/list ([k kws]) (var-demote k V)))]
[else
(make-arr (for/list ([d dom]) (var-promote d V))
(vd rng)
@ -85,5 +82,4 @@
(and drest
(cons (var-promote (car drest) V)
(cdr drest)))
(for/list ([k kws]) (var-demote k V))
names)])]))
(for/list ([k kws]) (var-demote k V)))])]))

View File

@ -14,7 +14,7 @@
'FilterSet
(λ (e) (or (FilterSet? e) (NoFilter? e)))))
(provide Filter/c FilterSet/c)
(provide Filter/c FilterSet/c name-ref/c hash-name)
(define name-ref/c (or/c identifier? integer?))
(define (hash-name v) (if (identifier? v) (hash-id v) v))
@ -48,18 +48,19 @@
(combine-frees (map free-idxs* fs))])
(df FilterSet (thn els)
[#:contract (->d ([t (cond [(Bot? t)
Bot?]
[(Bot? e)
Top?]
[else Filter/c])]
[e (cond [(Bot? e)
Bot?]
[(Bot? t)
Top?]
[else Filter/c])])
(#:syntax [stx #f])
[result FilterSet?])])
[#:contract (->d ([t (cond [(Bot? t)
Bot?]
[(Bot? e)
Top?]
[else Filter/c])]
[e (cond [(Bot? e)
Bot?]
[(Bot? t)
Top?]
[else Filter/c])])
(#:syntax [stx #f])
[result FilterSet?])]
[#:fold-rhs (*FilterSet (filter-rec-id thn) (filter-rec-id els))])
;; represents no info about the filters of this expression
;; should only be used for parsing type annotations and expected types

View File

@ -12,8 +12,8 @@
(do Empty () [#:fold-rhs #:base])
(do Path ([p (listof PathElem?)] [v identifier?])
[#:intern (list p (hash-id v))]
(do Path ([p (listof PathElem?)] [v name-ref/c])
[#:intern (list p (hash-name v))]
[#:frees (combine-frees (map free-vars* p)) (combine-frees (map free-idxs* p))]
[#:fold-rhs (*Path (map pathelem-rec-id p) v)])

View File

@ -181,13 +181,15 @@
#`[#,rec-id #,(hash-ref (attribute recs.mapping) k
#'values)])]
[(match-clauses ...)
(hash-map new-ht gen-clause)])
(hash-map new-ht gen-clause)]
[error-msg (quasisyntax/loc stx (error 'tc "no pattern for ~a" #,fold-target))])
#`(let (let-clauses ...
[#,fold-target ty])
;; then generate the fold
#,(quasisyntax/loc stx
(match #,fold-target
match-clauses ...))))])))
match-clauses ...
[_ error-msg]))))])))
(define-syntax (make-prim-type stx)
@ -237,9 +239,7 @@
(make-prim-type [Type #:key #:d dt]
[Filter #:d df]
[LatentFilter #:d dlf]
[Object #:d do]
[LatentObject #:d dlo]
[PathElem #:d dpe])
(provide PathElem? (rename-out [Rep-seq Type-seq]

View File

@ -4,7 +4,7 @@
(require (utils tc-utils)
"rep-utils.ss" "object-rep.ss" "filter-rep.ss" "free-variance.ss"
mzlib/trace scheme/match
scheme/contract
scheme/contract unstable/debug
(for-syntax scheme/base syntax/parse))
(define name-table (make-weak-hasheq))
@ -380,16 +380,16 @@
[(type<? s t) 1]
[else -1]))
(define ((sub-lf st) e)
(latentfilter-case (#:Type st
#:LatentFilter (sub-lf st))
e))
(define ((sub-f st) e)
(filter-case (#:Type st
#:Filter (sub-f st))
e))
(define ((sub-lo st) e)
(latentobject-case (#:Type st
#:LatentObject (sub-lo st)
#:PathElem (sub-pe st))
e))
(define ((sub-o st) e)
(object-case (#:Type st
#:Object (sub-o st)
#:PathElem (sub-pe st))
e))
(define ((sub-pe st) e)
(pathelem-case (#:Type st
@ -402,9 +402,8 @@
(define (nameTo name count type)
(let loop ([outer 0] [ty type])
(define (sb t) (loop outer t))
(define slf (sub-lf sb))
(type-case
(#:Type sb #:LatentFilter (sub-lf sb) #:LatentObject (sub-lo sb))
(#:Type sb #:Filter (sub-f sb) #:Object (sub-o sb))
ty
[#:F name* (if (eq? name name*) (*B (+ count outer)) ty)]
;; necessary to avoid infinite loops
@ -418,8 +417,7 @@
(cons (sb (car drest))
(if (eq? (cdr drest) name) (+ count outer) (cdr drest)))
#f)
(map sb kws)
names)]
(map sb kws))]
[#:ValuesDots rs dty dbound
(*ValuesDots (map sb rs)
(sb dty)
@ -439,6 +437,7 @@
(cdr names)
(sub1 count))))))
;; instantiate-many : List[Type] Scope^n -> Type
;; where n is the length of types
;; all of the types MUST be Fs
@ -446,9 +445,9 @@
(define (replace image count type)
(let loop ([outer 0] [ty type])
(define (sb t) (loop outer t))
(define slf (sub-lf sb))
(define sf (sub-f sb))
(type-case
(#:Type sb #:LatentFilter slf #:LatentObject (sub-lo sb))
(#:Type sb #:Filter sf #:Object (sub-o sb))
ty
[#:B idx (if (= (+ count outer) idx)
image
@ -622,10 +621,8 @@
(define-match-expander arr:*
(lambda (stx)
(syntax-parse stx
[(_ dom rng rest drest kws names)
(syntax/loc stx (arr: dom rng rest drest kws names))]
[(_ dom rng rest drest kws)
(syntax/loc stx (arr: dom rng rest drest kws _))])))
(syntax/loc stx (arr: dom rng rest drest kws))])))
;(trace subst subst-all)
(provide
@ -637,14 +634,14 @@
Mu? Poly? PolyDots?
arr
arr?
Type? Filter? LatentFilter? Object? LatentObject?
Type? Filter? Object?
Type/c
Poly-n
PolyDots-n
free-vars*
type-compare type<?
remove-dups
sub-lf sub-lo sub-pe
sub-f sub-o sub-pe
Values: Values? Values-rs
(rename-out [Mu:* Mu:]
[Poly:* Poly:]

View File

@ -731,8 +731,7 @@
;(printf "got to here 0~a~n" args-stx)
(match* (ftype0 argtys)
;; we check that all kw args are optional
[((arr: dom (Values: (list (Result: t-r f-r o-r) ...)) rest #f (list (Keyword: _ _ #f) ...)
names)
[((arr: dom (Values: (list (Result: t-r f-r o-r) ...)) rest #f (list (Keyword: _ _ #f) ...))
(list (tc-result1: t-a phi-a o-a) ...))
;(printf "got to here 1~a~n" args-stx)
(when check?
@ -748,8 +747,7 @@
(parameterize ([current-orig-stx a]) (check-below arg-t dom-t))))
;(printf "got to here 2 ~a ~a ~a ~n" dom names o-a)
(let-values ([(names o-a)
(for/lists (n o) ([d (in-list dom)]
[nm (in-list names)]
(for/lists (n o) ([(d nm) (in-indexed (in-list dom))]
[oa (in-list o-a)])
(values nm oa))])
;(printf "got to here 3~a~n" args-stx)

View File

@ -182,24 +182,18 @@
(d/c (make-arr* dom rng
#:rest [rest #f] #:drest [drest #f] #:kws [kws null]
#:filters [filters -no-filter] #:object [obj -no-obj]
#:names [names (append
(generate-temporaries dom)
(if (or drest rest) (list (generate-temporary)) null)
(generate-temporaries kws))])
#:filters [filters -no-filter] #:object [obj -no-obj])
(c:->* ((listof Type/c) (or/c Values? ValuesDots? Type/c))
(#:rest (or/c #f Type/c)
#:drest (or/c #f (cons/c Type/c symbol?))
#:kws (listof Keyword?)
#:filters FilterSet?
#:object Object?
#:names (listof identifier?))
#:object Object?)
arr?)
(make-arr dom (if (or (Values? rng) (ValuesDots? rng))
rng
(make-Values (list (-result rng filters obj))))
rest drest (sort #:key Keyword-kw kws keyword<?)
names))
rest drest (sort #:key Keyword-kw kws keyword<?)))
(define-syntax (->* stx)
(define-syntax-class c
@ -241,12 +235,10 @@
(make-Function (list (make-arr* dom rng #:drest (cons dty 'dbound) #:filters filters)))]))
(define (->acc dom rng path)
(define x (generate-temporary 'x))
(make-Function (list (make-arr* dom rng
#:names (list x)
#:filters (-FS (-not-filter (-val #f) x path)
(-filter (-val #f) x path))
#:object (make-Path path x)))))
(make-Function (list (make-arr* dom rng
#:filters (-FS (-not-filter (-val #f) 0 path)
(-filter (-val #f) 0 path))
#:object (make-Path path 0)))))
(define (cl->* . args)
(define (funty-arities f)
@ -275,7 +267,7 @@
(make-Struct name parent flds proc poly pred cert accs constructor))
(d/c (-filter t i [p null])
(c:->* (Type/c identifier?) ((listof PathElem?)) Filter/c)
(c:->* (Type/c name-ref/c) ((listof PathElem?)) Filter/c)
(make-TypeFilter t p i))
(define (-filter-at t o)
@ -329,7 +321,7 @@
[t (loop (cdr fs) (cons t result))]))))
(d/c (-not-filter t i [p null])
(c:->* (Type/c identifier?) ((listof PathElem?)) Filter/c)
(c:->* (Type/c name-ref/c) ((listof PathElem?)) Filter/c)
(make-NotTypeFilter t p i))
(define-syntax-rule (with-names (vars ...) . e)
@ -337,7 +329,7 @@
. e))
(define-syntax-rule (asym-pred (var) dom rng filter)
(with-names (var) (make-Function (list (make-arr* (list dom) rng #:names (list var) #:filters filter)))))
(with-names (var) (make-Function (list (make-arr* (list dom) rng #:filters filter)))))
(d/c make-pred-ty
(case-> (c:-> Type/c Type/c)
@ -346,12 +338,11 @@
(c:-> (listof Type/c) Type/c Type/c integer? (listof PathElem?) Type/c))
(case-lambda
[(in out t n p)
(define xs (generate-temporaries in))
(define xs (for/list ([(_ i) (in-indexed (in-list in))]) i))
(make-Function
(list
(make-arr*
in out
#:names xs
#:filters (-FS (-filter t (list-ref xs n) p) (-not-filter t (list-ref xs n) p)))))]
[(in out t n)
(make-pred-ty in out t n null)]

View File

@ -34,10 +34,10 @@
(match c
[(FilterSet: thn els) (fp "(~a | ~a)" thn els)]
[(NoFilter:) (fp "-")]
[(NotTypeFilter: type (list) id) (fp "(! ~a @ ~a)" type (syntax-e id))]
[(NotTypeFilter: type path id) (fp "(! ~a @ ~a ~a)" type path (syntax-e id))]
[(TypeFilter: type (list) id) (fp "(~a @ ~a)" type (syntax-e id))]
[(TypeFilter: type path id) (fp "(~a @ ~a ~a)" type path (syntax-e id))]
[(NotTypeFilter: type (list) id) (fp "(! ~a @ ~a)" type id)]
[(NotTypeFilter: type path id) (fp "(! ~a @ ~a ~a)" type path id)]
[(TypeFilter: type (list) id) (fp "(~a @ ~a)" type id)]
[(TypeFilter: type path id) (fp "(~a @ ~a ~a)" type path id)]
[(Bot:) (fp "Bot")]
[(Top:) (fp "Top")]
[(ImpFilter: a c) (fp "(ImpFilter ~a ~a)" a c)]
@ -58,7 +58,7 @@
(match c
[(NoObject:) (fp "-")]
[(Empty:) (fp "")]
[(Path: pes i) (fp "~a" (append pes (list (syntax-e i))))]
[(Path: pes i) (fp "~a" (append pes (list i)))]
[else (fp "(Unknown Object: ~a)" (struct->vector c))]))
;; print out a type

View File

@ -184,13 +184,13 @@
(d/c (combine-arrs arrs)
(c-> (listof arr?) (or/c #f arr?))
(match arrs
[(list (and a1 (arr: dom1 rng1 #f #f '() names)) (arr: dom rng #f #f '()) ...)
[(list (and a1 (arr: dom1 rng1 #f #f '())) (arr: dom rng #f #f '()) ...)
(cond
[(null? dom) (make-arr dom1 rng1 #f #f '() names)]
[(null? dom) (make-arr dom1 rng1 #f #f '())]
[(not (apply = (length dom1) (map length dom))) #f]
[(not (for/and ([rng2 (in-list rng)]) (type-equal? rng1 rng2)))
#f]
[else (make-arr (apply map (lambda args (make-Union (sort args type<?))) (cons dom1 dom)) rng1 #f #f '() names)])]
[else (make-arr (apply map (lambda args (make-Union (sort args type<?))) (cons dom1 dom)) rng1 #f #f '())])]
[_ #f]))

View File

@ -39,11 +39,11 @@
(define (substitute image name target #:Un [Un (get-union-maker)])
(define (sb t) (substitute image name t))
(if (hash-ref (free-vars* target) name #f)
(type-case (#:Type sb #:LatentFilter (sub-lf sb) #:LatentObject (sub-lo sb))
(type-case (#:Type sb #:Filter (sub-f sb) #:Object (sub-o sb))
target
[#:Union tys (Un (map sb tys))]
[#:F name* (if (eq? name* name) image target)]
[#:arr dom rng rest drest kws names
[#:arr dom rng rest drest kws
(begin
(when (and (pair? drest)
(eq? name (cdr drest))
@ -53,8 +53,7 @@
(sb rng)
(and rest (sb rest))
(and drest (cons (sb (car drest)) (cdr drest)))
(map sb kws)
names))]
(map sb kws)))]
[#:ValuesDots types dty dbound
(begin
(when (eq? name dbound)
@ -66,7 +65,7 @@
(define (substitute-dots images rimage name target)
(define (sb t) (substitute-dots images rimage name t))
(if (hash-ref (free-vars* target) name #f)
(type-case (#:Type sb #:LatentFilter (sub-lf sb)) target
(type-case (#:Type sb #:Filter (sub-f sb)) target
[#:ValuesDots types dty dbound
(if (eq? name dbound)
(make-Values
@ -80,7 +79,7 @@
(make-FilterSet (make-Top) (make-Top))
(make-Empty))))))
(make-ValuesDots (map sb types) (sb dty) dbound))]
[#:arr dom rng rest drest kws names
[#:arr dom rng rest drest kws
(if (and (pair? drest)
(eq? name (cdr drest)))
(make-arr (append
@ -91,14 +90,12 @@
(sb rng)
rimage
#f
(map sb kws)
names)
(map sb kws))
(make-arr (map sb dom)
(sb rng)
(and rest (sb rest))
(and drest (cons (sb (car drest)) (cdr drest)))
(map sb kws)
names))])
(map sb kws)))])
target))
;; implements sd from the formalism
@ -106,7 +103,7 @@
(define (substitute-dotted image image-bound name target)
(define (sb t) (substitute-dotted image image-bound name t))
(if (hash-ref (free-vars* target) name #f)
(type-case (#:Type sb #:LatentFilter (sub-lf sb))
(type-case (#:Type sb #:Filter (sub-f sb))
target
[#:ValuesDots types dty dbound
(make-ValuesDots (map sb types)
@ -116,15 +113,14 @@
(if (eq? name* name)
image
target)]
[#:arr dom rng rest drest kws names
[#:arr dom rng rest drest kws
(make-arr (map sb dom)
(sb rng)
(and rest (sb rest))
(and drest
(cons (sb (car drest))
(if (eq? name (cdr drest)) image-bound (cdr drest))))
(map sb kws)
names)])
(map sb kws))])
target))
;; substitute many variables