Merge V, X, and Y arguments into a single context in infer.
original commit: 615776f8d1feb3d761f0dbf97ab0e14f61eff51b
This commit is contained in:
Eric Dobson
parent
d3705800c3
commit
10a4412490
|
|
@ -43,6 +43,46 @@
|
|||
(define (seen-before s t)
|
||||
(cons (Type-seq s) (Type-seq t)))
|
||||
|
||||
;; Context, contains which type variables and indices to infer and which cannot be mentioned in
|
||||
;; constraints.
|
||||
(define-struct/cond-contract context
|
||||
([bounds (listof symbol?)]
|
||||
[vars (listof symbol?)]
|
||||
[indices (listof symbol?)]) #:transparent)
|
||||
|
||||
(define (context-add-vars ctx vars)
|
||||
(match ctx
|
||||
[(context V X Y)
|
||||
(context V (append vars X) Y)]))
|
||||
|
||||
(define (context-add-var ctx var)
|
||||
(match ctx
|
||||
[(context V X Y)
|
||||
(context V (cons var X) Y)]))
|
||||
|
||||
(define (context-add ctx #:bounds [bounds empty] #:vars [vars empty] #:indices [indices empty])
|
||||
(match ctx
|
||||
[(context V X Y)
|
||||
(context (append bounds V) (append vars X) (append indices Y))]))
|
||||
|
||||
(define (inferable-index? ctx bound)
|
||||
(match ctx
|
||||
[(context _ _ Y)
|
||||
(memq bound Y)]))
|
||||
|
||||
(define ((inferable-var? ctx) var)
|
||||
(match ctx
|
||||
[(context _ X _)
|
||||
(memq var X)]))
|
||||
|
||||
(define (empty-cset/context ctx)
|
||||
(match ctx
|
||||
[(context _ X Y)
|
||||
(empty-cset X Y)]))
|
||||
|
||||
|
||||
|
||||
|
||||
;; Type Type Seen -> Seen
|
||||
;; Add the type pair to the set of seen type pairs
|
||||
(define/cond-contract (remember s t A)
|
||||
|
|
@ -184,77 +224,77 @@
|
|||
(substitute (make-F var) v ty*))))
|
||||
|
||||
|
||||
(define/cond-contract (cgen/filter V X Y s t)
|
||||
((listof symbol?) (listof symbol?) (listof symbol?) Filter? Filter? . -> . (or/c #f cset?))
|
||||
(define/cond-contract (cgen/filter context s t)
|
||||
(context? Filter? Filter? . -> . (or/c #f cset?))
|
||||
(match* (s t)
|
||||
[(e e) (empty-cset X Y)]
|
||||
[(e (Top:)) (empty-cset X Y)]
|
||||
[(e e) (empty-cset/context context)]
|
||||
[(e (Top:)) (empty-cset/context context)]
|
||||
;; FIXME - is there something to be said about the logical ones?
|
||||
[((TypeFilter: s p) (TypeFilter: t p)) (cgen/inv V X Y s t)]
|
||||
[((NotTypeFilter: s p) (NotTypeFilter: t p)) (cgen/inv V X Y s t)]
|
||||
[((TypeFilter: s p) (TypeFilter: t p)) (cgen/inv context s t)]
|
||||
[((NotTypeFilter: s p) (NotTypeFilter: t p)) (cgen/inv context s t)]
|
||||
[(_ _) #f]))
|
||||
|
||||
;; s and t must be *latent* filter sets
|
||||
(define/cond-contract (cgen/filter-set V X Y s t)
|
||||
((listof symbol?) (listof symbol?) (listof symbol?) FilterSet? FilterSet? . -> . (or/c #f cset?))
|
||||
(define/cond-contract (cgen/filter-set context s t)
|
||||
(context? FilterSet? FilterSet? . -> . (or/c #f cset?))
|
||||
(match* (s t)
|
||||
[(e e) (empty-cset X Y)]
|
||||
[(e e) (empty-cset/context context)]
|
||||
[((FilterSet: s+ s-) (FilterSet: t+ t-))
|
||||
(% cset-meet (cgen/filter V X Y s+ t+) (cgen/filter V X Y s- t-))]
|
||||
(% cset-meet (cgen/filter context s+ t+) (cgen/filter context s- t-))]
|
||||
[(_ _) #f]))
|
||||
|
||||
(define/cond-contract (cgen/object V X Y s t)
|
||||
((listof symbol?) (listof symbol?) (listof symbol?) Object? Object? . -> . (or/c #f cset?))
|
||||
(define/cond-contract (cgen/object context s t)
|
||||
(context? Object? Object? . -> . (or/c #f cset?))
|
||||
(match* (s t)
|
||||
[(e e) (empty-cset X Y)]
|
||||
[(e (Empty:)) (empty-cset X Y)]
|
||||
[(e e) (empty-cset/context context)]
|
||||
[(e (Empty:)) (empty-cset/context context)]
|
||||
;; FIXME - do something here
|
||||
[(_ _) #f]))
|
||||
|
||||
(define/cond-contract (cgen/seq V X Y s-seq t-seq)
|
||||
((listof symbol?) (listof symbol?) (listof symbol?) seq? seq? . -> . (or/c #f cset?))
|
||||
(define/cond-contract (cgen/seq context s-seq t-seq)
|
||||
(context? seq? seq? . -> . (or/c #f cset?))
|
||||
(match*/early (s-seq t-seq)
|
||||
;; The simplest case - both are null-end
|
||||
[((seq ss (null-end))
|
||||
(seq ts (null-end)))
|
||||
(cgen/list V X Y ss ts)]
|
||||
(cgen/list context ss ts)]
|
||||
;; One is null-end the other is uniform-end
|
||||
[((seq ss (null-end))
|
||||
(seq ts (uniform-end t-rest)))
|
||||
(cgen/list V X Y ss (extend ss ts t-rest))]
|
||||
(cgen/list context ss (extend ss ts t-rest))]
|
||||
[((seq ss (uniform-end s-rest))
|
||||
(seq ts (null-end)))
|
||||
#f]
|
||||
;; Both are uniform-end
|
||||
[((seq ss (uniform-end s-rest))
|
||||
(seq ts (uniform-end t-rest)))
|
||||
(cgen/list V X Y
|
||||
(cgen/list context
|
||||
(cons s-rest ss)
|
||||
(cons t-rest (extend ss ts t-rest)))]
|
||||
;; dotted below, nothing above
|
||||
[((seq ss (dotted-end dty dbound))
|
||||
(seq ts (null-end)))
|
||||
#:return-unless (memq dbound Y)
|
||||
#:return-unless (inferable-index? context dbound)
|
||||
#f
|
||||
#:return-unless (<= (length ss) (length ts))
|
||||
#f
|
||||
(define-values (vars new-tys) (generate-dbound-prefix dbound dty (- (length ts) (length ss)) #f))
|
||||
(define-values (ts-front ts-back) (split-at ts (length ss)))
|
||||
(% cset-meet
|
||||
(cgen/list V X Y ss ts-front)
|
||||
(% move-vars-to-dmap (cgen/list V (append vars X) Y new-tys ts-back) dbound vars))]
|
||||
(cgen/list context ss ts-front)
|
||||
(% move-vars-to-dmap (cgen/list (context-add context #:vars vars) new-tys ts-back) dbound vars))]
|
||||
;; dotted above, nothing below
|
||||
[((seq ss (null-end))
|
||||
(seq ts (dotted-end dty dbound)))
|
||||
#:return-unless (memq dbound Y)
|
||||
#:return-unless (inferable-index? context dbound)
|
||||
#f
|
||||
#:return-unless (<= (length ts) (length ss))
|
||||
#f
|
||||
(define-values (vars new-tys) (generate-dbound-prefix dbound dty (- (length ss) (length ts)) #f))
|
||||
(define-values (ss-front ss-back) (split-at ss (length ts)))
|
||||
(% cset-meet
|
||||
(cgen/list V X Y ss-front ts)
|
||||
(% move-vars-to-dmap (cgen/list V (append vars X) Y ss-back new-tys) dbound vars))]
|
||||
(cgen/list context ss-front ts)
|
||||
(% move-vars-to-dmap (cgen/list (context-add-vars context vars) ss-back new-tys) dbound vars))]
|
||||
|
||||
;; same dotted bound
|
||||
[((seq ss (dotted-end s-dty dbound))
|
||||
|
|
@ -262,33 +302,35 @@
|
|||
#:return-unless (= (length ss) (length ts))
|
||||
#f
|
||||
(% cset-meet
|
||||
(cgen/list V X Y ss ts)
|
||||
(if (memq dbound Y)
|
||||
(cgen/list context ss ts)
|
||||
(if (inferable-index? context dbound)
|
||||
(extend-tvars (list dbound)
|
||||
(% move-vars+rest-to-dmap (cgen V (cons dbound X) Y s-dty t-dty) null dbound))
|
||||
(cgen V X Y s-dty t-dty)))]
|
||||
(% move-vars+rest-to-dmap (cgen (context-add-var context dbound) s-dty t-dty) null dbound))
|
||||
(cgen context s-dty t-dty)))]
|
||||
|
||||
;; bounds are different
|
||||
[((seq ss (dotted-end s-dty (? (λ (db) (memq db Y)) dbound)))
|
||||
(seq ts (dotted-end t-dty dbound*)))
|
||||
#:return-unless (= (length ss) (length ts)) #f
|
||||
#:return-when (memq dbound* Y) #f
|
||||
(% cset-meet
|
||||
(cgen/list V X Y ss ts)
|
||||
(extend-tvars (list dbound*)
|
||||
(% move-dotted-rest-to-dmap (cgen V (cons dbound X) Y s-dty t-dty) dbound dbound*)))]
|
||||
[((seq ss (dotted-end s-dty dbound))
|
||||
(seq ts (dotted-end t-dty (? (λ (db) (memq db Y)) dbound*))))
|
||||
(seq ts (dotted-end t-dty dbound*)))
|
||||
#:when (inferable-index? context dbound)
|
||||
#:return-unless (= (length ss) (length ts)) #f
|
||||
#:return-when (inferable-index? context dbound*) #f
|
||||
(% cset-meet
|
||||
(cgen/list context ss ts)
|
||||
(extend-tvars (list dbound*)
|
||||
(% move-dotted-rest-to-dmap (cgen (context-add-var context dbound) s-dty t-dty) dbound dbound*)))]
|
||||
[((seq ss (dotted-end s-dty dbound))
|
||||
(seq ts (dotted-end t-dty dbound*)))
|
||||
#:when (inferable-index? context dbound*)
|
||||
#:return-unless (= (length ss) (length ts)) #f
|
||||
(% cset-meet
|
||||
(cgen/list V X Y ss ts)
|
||||
(cgen/list context ss ts)
|
||||
(extend-tvars (list dbound)
|
||||
(% move-dotted-rest-to-dmap (cgen V (cons dbound* X) Y s-dty t-dty) dbound* dbound)))]
|
||||
(% move-dotted-rest-to-dmap (cgen (context-add-var context dbound*) s-dty t-dty) dbound* dbound)))]
|
||||
|
||||
;; * <: ...
|
||||
[((seq ss (uniform-end s-rest))
|
||||
(seq ts (dotted-end t-dty dbound)))
|
||||
#:return-unless (memq dbound Y)
|
||||
#:return-unless (inferable-index? context dbound)
|
||||
#f
|
||||
#:return-unless (<= (length ts) (length ss))
|
||||
#f
|
||||
|
|
@ -297,37 +339,38 @@
|
|||
new-bound))
|
||||
(define-values (ss-front ss-back) (split-at ss (length ts)))
|
||||
(% cset-meet
|
||||
(cgen/list V X Y ss-front ts)
|
||||
(cgen/list context ss-front ts)
|
||||
(% move-vars+rest-to-dmap
|
||||
(% cset-meet
|
||||
(cgen/list (cons new-bound V) (append vars X) (cons new-bound Y) ss-back new-tys)
|
||||
(cgen V (cons dbound X) Y s-rest t-dty))
|
||||
(cgen/list (context-add context #:bounds (list new-bound) #:vars vars #:indices (list new-bound))
|
||||
ss-back new-tys)
|
||||
(cgen (context-add-var context dbound) s-rest t-dty))
|
||||
vars dbound #:exact #t))]
|
||||
|
||||
[((seq ss (dotted-end s-dty dbound))
|
||||
(seq ts (uniform-end t-rest)))
|
||||
(cond
|
||||
[(memq dbound Y)
|
||||
[(inferable-index? context dbound)
|
||||
(define new-bound (gensym dbound))
|
||||
(define length-delta (- (length ts) (length ss)))
|
||||
(define-values (vars new-tys)
|
||||
(generate-dbound-prefix dbound s-dty (max 0 length-delta) new-bound))
|
||||
(% cset-meet
|
||||
(cgen/list V X Y ss (if (positive? length-delta)
|
||||
(drop-right ts length-delta)
|
||||
(extend ss ts t-rest)))
|
||||
(cgen/list context ss (if (positive? length-delta)
|
||||
(drop-right ts length-delta)
|
||||
(extend ss ts t-rest)))
|
||||
(% move-vars+rest-to-dmap
|
||||
(% cset-meet
|
||||
(cgen/list (cons new-bound V) (append vars X) (cons new-bound Y)
|
||||
(cgen/list (context-add context #:bounds (list new-bound) #:vars vars #:indices (list new-bound))
|
||||
new-tys (take-right ts (max 0 length-delta)))
|
||||
(cgen V (cons dbound X) Y s-dty t-rest))
|
||||
(cgen (context-add-var context dbound) s-dty t-rest))
|
||||
vars dbound))]
|
||||
[else
|
||||
(extend-tvars (list dbound)
|
||||
(cgen/seq (cons dbound V) X Y (seq ss (uniform-end s-dty)) t-seq))])]))
|
||||
(cgen/seq (context-add context #:bounds (list dbound)) (seq ss (uniform-end s-dty)) t-seq))])]))
|
||||
|
||||
(define/cond-contract (cgen/arr V X Y s-arr t-arr)
|
||||
((listof symbol?) (listof symbol?) (listof symbol?) arr? arr? . -> . (or/c #f cset?))
|
||||
(define/cond-contract (cgen/arr context s-arr t-arr)
|
||||
(context? arr? arr? . -> . (or/c #f cset?))
|
||||
|
||||
(match* (s-arr t-arr)
|
||||
[((arr: ss s s-rest s-drest s-kws) (arr: ts t t-rest t-drest t-kws))
|
||||
|
|
@ -342,45 +385,41 @@
|
|||
(and (null? s-kws)
|
||||
(null? t-kws)
|
||||
(% cset-meet
|
||||
(cgen V X Y s t)
|
||||
(cgen/seq V X Y t-seq s-seq)))]))
|
||||
(cgen context s t)
|
||||
(cgen/seq context t-seq s-seq)))]))
|
||||
|
||||
(define/cond-contract (cgen/flds V X Y flds-s flds-t)
|
||||
((listof symbol?) (listof symbol?) (listof symbol?) (listof fld?) (listof fld?)
|
||||
. -> . (or/c #f cset?))
|
||||
(define/cond-contract (cgen/flds context flds-s flds-t)
|
||||
(context? (listof fld?) (listof fld?) . -> . (or/c #f cset?))
|
||||
(% cset-meet*
|
||||
(for/list/fail ([s (in-list flds-s)] [t (in-list flds-t)])
|
||||
(match* (s t)
|
||||
;; mutable - invariant
|
||||
[((fld: s _ #t) (fld: t _ #t)) (cgen/inv V X Y s t)]
|
||||
[((fld: s _ #t) (fld: t _ #t)) (cgen/inv context s t)]
|
||||
;; immutable - covariant
|
||||
[((fld: s _ #f) (fld: t _ #f)) (cgen V X Y s t)]))))
|
||||
[((fld: s _ #f) (fld: t _ #f)) (cgen context s t)]))))
|
||||
|
||||
(define (cgen/inv V X Y s t)
|
||||
(% cset-meet (cgen V X Y s t) (cgen V X Y t s)))
|
||||
(define (cgen/inv context s t)
|
||||
(% cset-meet (cgen context s t) (cgen context t s)))
|
||||
|
||||
|
||||
;; V : a set of variables not to mention in the constraints
|
||||
;; X : the set of type variables to be constrained
|
||||
;; Y : the set of index variables to be constrained
|
||||
;; context : the context of what to infer/not infer
|
||||
;; S : a type to be the subtype of T
|
||||
;; T : a type
|
||||
;; produces a cset which determines a substitution that makes S a subtype of T
|
||||
;; implements the V |-_X S <: T => C judgment from Pierce+Turner, extended with
|
||||
;; the index variables from the TOPLAS paper
|
||||
(define/cond-contract (cgen V X Y S T)
|
||||
((listof symbol?) (listof symbol?) (listof symbol?)
|
||||
(or/c Values/c ValuesDots? AnyValues?) (or/c Values/c ValuesDots? AnyValues?)
|
||||
(define/cond-contract (cgen context S T)
|
||||
(context? (or/c Values/c ValuesDots? AnyValues?) (or/c Values/c ValuesDots? AnyValues?)
|
||||
. -> . (or/c #F cset?))
|
||||
;; useful quick loop
|
||||
(define/cond-contract (cg S T)
|
||||
(Type/c Type/c . -> . (or/c #f cset?))
|
||||
(cgen V X Y S T))
|
||||
(cgen context S T))
|
||||
(define/cond-contract (cg/inv S T)
|
||||
(Type/c Type/c . -> . (or/c #f cset?))
|
||||
(cgen/inv V X Y S T))
|
||||
;; this places no constraints on any variables in X
|
||||
(define empty (empty-cset X Y))
|
||||
(cgen/inv context S T))
|
||||
;; this places no constraints on any variables
|
||||
(define empty (empty-cset/context context))
|
||||
;; this constrains just x (which is a single var)
|
||||
(define (singleton S x T)
|
||||
(insert empty x S T))
|
||||
|
|
@ -401,7 +440,7 @@
|
|||
[(_ (Univ:)) empty]
|
||||
;; AnyValues
|
||||
[((AnyValues: s-f) (AnyValues: t-f))
|
||||
(cgen/filter V X Y s-f t-f)]
|
||||
(cgen/filter context s-f t-f)]
|
||||
|
||||
[((or (Values: (list (Result: _ fs _) ...))
|
||||
(ValuesDots: (list (Result: _ fs _) ...) _ _))
|
||||
|
|
@ -411,7 +450,7 @@
|
|||
(for/list ([f (in-list fs)])
|
||||
(match f
|
||||
[(FilterSet: f+ f-)
|
||||
(% cset-meet (cgen/filter V X Y f+ t-f) (cgen/filter V X Y f- t-f))]))))]
|
||||
(% cset-meet (cgen/filter context f+ t-f) (cgen/filter context f- t-f))]))))]
|
||||
|
||||
;; check all non Type/c first so that calling subtype is safe
|
||||
|
||||
|
|
@ -419,8 +458,8 @@
|
|||
[((Result: s f-s o-s)
|
||||
(Result: t f-t o-t))
|
||||
(% cset-meet (cg s t)
|
||||
(cgen/filter-set V X Y f-s f-t)
|
||||
(cgen/object V X Y o-s o-t))]
|
||||
(cgen/filter-set context f-s f-t)
|
||||
(cgen/object context o-s o-t))]
|
||||
|
||||
;; Values just delegate to cgen/seq, except special handling for -Bottom.
|
||||
;; A single -Bottom in a Values means that there is no value returned and so any other
|
||||
|
|
@ -430,10 +469,10 @@
|
|||
(define bottom-case
|
||||
(match S
|
||||
[(Values: (list (Result: s f-s o-s)))
|
||||
(cgen V X Y s -Bottom)]
|
||||
(cgen context s -Bottom)]
|
||||
[else #f]))
|
||||
(define regular-case
|
||||
(cgen/seq V X Y s-seq t-seq))
|
||||
(cgen/seq context s-seq t-seq))
|
||||
;; If we want the OR of the csets that the two cases return.
|
||||
(cset-join
|
||||
(filter values
|
||||
|
|
@ -446,7 +485,7 @@
|
|||
|
||||
;; Lists delegate to sequences
|
||||
[((ListSeq: s-seq) (ListSeq: t-seq))
|
||||
(cgen/seq V X Y s-seq t-seq)]
|
||||
(cgen/seq context s-seq t-seq)]
|
||||
|
||||
;; refinements are erased to their bound
|
||||
[((Refinement: S _) T)
|
||||
|
|
@ -454,24 +493,24 @@
|
|||
|
||||
;; variables that are in X and should be constrained
|
||||
;; all other variables are compatible only with themselves
|
||||
[((F: (? (λ (e) (memq e X)) v)) T)
|
||||
[((F: (? (inferable-var? context) v)) T)
|
||||
#:return-when
|
||||
(match T
|
||||
;; fail when v* is an index variable
|
||||
[(F: v*) (and (bound-index? v*) (not (bound-tvar? v*)))]
|
||||
[_ #f])
|
||||
#f
|
||||
;; constrain v to be below T (but don't mention V)
|
||||
(singleton (Un) v (var-demote T V))]
|
||||
;; constrain v to be below T (but don't mention bounds)
|
||||
(singleton (Un) v (var-demote T (context-bounds context)))]
|
||||
|
||||
[(S (F: (? (lambda (e) (memq e X)) v)))
|
||||
[(S (F: (? (inferable-var? context) v)))
|
||||
#:return-when
|
||||
(match S
|
||||
[(F: v*) (and (bound-index? v*) (not (bound-tvar? v*)))]
|
||||
[_ #f])
|
||||
#f
|
||||
;; constrain v to be above S (but don't mention V)
|
||||
(singleton (var-promote S V) v Univ)]
|
||||
;; constrain v to be above S (but don't mention bounds)
|
||||
(singleton (var-promote S (context-bounds context)) v Univ)]
|
||||
|
||||
;; recursive names should get resolved as they're seen
|
||||
[(s (? Name? t))
|
||||
|
|
@ -480,7 +519,7 @@
|
|||
(cg (resolve-once s) t)]
|
||||
|
||||
;; constrain b1 to be below T, but don't mention the new vars
|
||||
[((Poly: v1 b1) T) (cgen (append v1 V) X Y b1 T)]
|
||||
[((Poly: v1 b1) T) (cgen (context-add context #:bounds v1) b1 T)]
|
||||
|
||||
;; constrain *each* element of es to be below T, and then combine the constraints
|
||||
[((Union: es) T)
|
||||
|
|
@ -506,7 +545,7 @@
|
|||
(cg proc proc*)]
|
||||
[proc* #f]
|
||||
[else empty])])
|
||||
(% cset-meet proc-c (cgen/flds V X Y flds flds*)))]
|
||||
(% cset-meet proc-c (cgen/flds context flds flds*)))]
|
||||
|
||||
;; two struct names, need to resolve b/c one could be a parent
|
||||
[((Name: n _ _ #t) (Name: n* _ _ #t))
|
||||
|
|
@ -518,7 +557,7 @@
|
|||
(% cset-meet (cg a a*) (cg b b*))]
|
||||
;; sequences are covariant
|
||||
[((Sequence: ts) (Sequence: ts*))
|
||||
(cgen/list V X Y ts ts*)]
|
||||
(cgen/list context ts ts*)]
|
||||
[((Listof: t) (Sequence: (list t*)))
|
||||
(cg t t*)]
|
||||
[((Pair: t1 t2) (Sequence: (list t*)))
|
||||
|
|
@ -533,10 +572,10 @@
|
|||
(% cset-meet* (for/list/fail ([t (in-list ts)])
|
||||
(cg t t*)))]
|
||||
[((HeterogeneousVector: ts) (HeterogeneousVector: ts*))
|
||||
(% cset-meet (cgen/list V X Y ts ts*) (cgen/list V X Y ts* ts))]
|
||||
(% cset-meet (cgen/list context ts ts*) (cgen/list context ts* ts))]
|
||||
[((HeterogeneousVector: ts) (Vector: s))
|
||||
(define ts* (map (λ _ s) ts)) ;; invariant, everything has to match
|
||||
(% cset-meet (cgen/list V X Y ts ts*) (cgen/list V X Y ts* ts))]
|
||||
(% cset-meet (cgen/list context ts ts*) (cgen/list context ts* ts))]
|
||||
[((HeterogeneousVector: ts) (Sequence: (list t*)))
|
||||
(% cset-meet* (for/list/fail ([t (in-list ts)])
|
||||
(cg t t*)))]
|
||||
|
|
@ -567,7 +606,7 @@
|
|||
(and (subtype S t) t)))
|
||||
(% cg type t*)]
|
||||
[((Hashtable: k v) (Sequence: (list k* v*)))
|
||||
(cgen/list V X Y (list k v) (list k* v*))]
|
||||
(cgen/list context (list k v) (list k* v*))]
|
||||
[((Set: t) (Sequence: (list t*)))
|
||||
(cg t t*)]
|
||||
|
||||
|
|
@ -662,7 +701,7 @@
|
|||
(for/list/fail ([t-arr (in-list t-arr)])
|
||||
;; for each element of t-arr, we need to get at least one element of s-arr that works
|
||||
(let ([results (for*/list ([s-arr (in-list s-arr)]
|
||||
[v (in-value (cgen/arr V X Y s-arr t-arr))]
|
||||
[v (in-value (cgen/arr context s-arr t-arr))]
|
||||
#:when v)
|
||||
v)])
|
||||
;; ensure that something produces a constraint set
|
||||
|
|
@ -742,25 +781,22 @@
|
|||
(and entry (t-subst? entry))))
|
||||
(extend-idxs subst)))]))
|
||||
|
||||
;; V : a set of variables not to mention in the constraints
|
||||
;; X : the set of type variables to be constrained
|
||||
;; Y : the set of index variables to be constrained
|
||||
;; context : the context of what to infer/not infer
|
||||
;; S : a list of types to be the subtypes of T
|
||||
;; T : a list of types
|
||||
;; expected-cset : a cset representing the expected type, to meet early and
|
||||
;; keep the number of constraints in check. (empty by default)
|
||||
;; produces a cset which determines a substitution that makes the Ss subtypes of the Ts
|
||||
(define/cond-contract (cgen/list V X Y S T
|
||||
(define/cond-contract (cgen/list context S T
|
||||
#:expected-cset [expected-cset (empty-cset '() '())])
|
||||
(((listof symbol?) (listof symbol?) (listof symbol?) (listof Values/c) (listof Values/c))
|
||||
(#:expected-cset cset?) . ->* . (or/c cset? #f))
|
||||
((context? (listof Values/c) (listof Values/c)) (#:expected-cset cset?) . ->* . (or/c cset? #f))
|
||||
(and (= (length S) (length T))
|
||||
(% cset-meet*
|
||||
(for/list/fail ([s (in-list S)] [t (in-list T)])
|
||||
;; We meet early to prune the csets to a reasonable size.
|
||||
;; This weakens the inference a bit, but sometimes avoids
|
||||
;; constraint explosion.
|
||||
(% cset-meet (cgen V X Y s t) expected-cset)))))
|
||||
(% cset-meet (cgen context s t) expected-cset)))))
|
||||
|
||||
|
||||
|
||||
|
|
@ -780,13 +816,16 @@
|
|||
(or/c #f Values/c ValuesDots?))
|
||||
((or/c #f Values/c AnyValues? ValuesDots?))
|
||||
. ->* . (or/c boolean? substitution/c))
|
||||
(let* ([expected-cset (if expected
|
||||
(cgen null X Y R expected)
|
||||
(empty-cset '() '()))]
|
||||
[cs (and expected-cset
|
||||
(cgen/list null X Y S T #:expected-cset expected-cset))]
|
||||
[cs* (% cset-meet cs expected-cset)])
|
||||
(and cs* (if R (subst-gen cs* X Y R) #t))))
|
||||
(define ctx (context null X Y ))
|
||||
(define expected-cset
|
||||
(if expected
|
||||
(cgen ctx R expected)
|
||||
(empty-cset '() '())))
|
||||
(and expected-cset
|
||||
(let* ([cs (cgen/list ctx S T #:expected-cset expected-cset)]
|
||||
[cs* (% cset-meet cs expected-cset)])
|
||||
(and cs* (if R (subst-gen cs* X Y R) #t)))))
|
||||
;(trace infer)
|
||||
infer)) ;to export a variable binding and not syntax
|
||||
|
||||
;; like infer, but T-var is the vararg type:
|
||||
|
|
@ -801,16 +840,16 @@
|
|||
(early-return
|
||||
(define short-S (take S (length T)))
|
||||
(define rest-S (drop S (length T)))
|
||||
(define ctx (context null X (list dotted-var)))
|
||||
(define expected-cset (if expected
|
||||
(cgen null X (list dotted-var) R expected)
|
||||
(cgen ctx R expected)
|
||||
(empty-cset '() '())))
|
||||
#:return-unless expected-cset #f
|
||||
(define cs-short (cgen/list null X (list dotted-var) short-S T
|
||||
#:expected-cset expected-cset))
|
||||
(define cs-short (cgen/list ctx short-S T #:expected-cset expected-cset))
|
||||
#:return-unless cs-short #f
|
||||
(define-values (new-vars new-Ts)
|
||||
(generate-dbound-prefix dotted-var T-dotted (length rest-S) #f))
|
||||
(define cs-dotted (cgen/list null (append new-vars X) (list dotted-var) rest-S new-Ts
|
||||
(define cs-dotted (cgen/list (context-add-vars ctx new-vars) rest-S new-Ts
|
||||
#:expected-cset expected-cset))
|
||||
#:return-unless cs-dotted #f
|
||||
(define cs-dotted* (move-vars-to-dmap cs-dotted dotted-var new-vars))
|
||||
|
|
@ -822,3 +861,8 @@
|
|||
(subst-gen m X (list dotted-var) R)))
|
||||
|
||||
|
||||
;(trace subst-gen)
|
||||
;(trace cgen)
|
||||
;(trace cgen/list)
|
||||
;(trace cgen/arr)
|
||||
;(trace cgen/seq)
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user