Switch input from arities to sequences.
original commit: 03ad77afd4b3d2370dce572ff563bff4cfdaaf63
This commit is contained in:
Eric Dobson
parent
71f20a7863
commit
30f8b22021
|
|
@ -145,6 +145,15 @@
|
|||
[(dcon-exact null rest) rest]
|
||||
[_ (int-err "did not get a rest-only dcon when moving to the dmap")])))))
|
||||
|
||||
;; Represents a sequence of types. types are the fixed prefix, and end is the remaining types
|
||||
;; This is a unification of all of the dotted types that exist ListDots, ->..., and ValuesDots.
|
||||
;; This allows for one implementation of the cgen algorithm for dotted types to be shared across all
|
||||
;; of them.
|
||||
(struct seq (types end) #:transparent)
|
||||
(struct null-end () #:transparent)
|
||||
(struct uniform-end (type) #:transparent)
|
||||
(struct dotted-end (type bound) #:transparent)
|
||||
|
||||
|
||||
;; Maps dotted vars (combined with dotted types, to ensure global uniqueness)
|
||||
;; to "fresh" symbols.
|
||||
|
|
@ -201,30 +210,32 @@
|
|||
(define/cond-contract (cgen/arr V X Y s-arr t-arr)
|
||||
((listof symbol?) (listof symbol?) (listof symbol?) arr? arr? . -> . (or/c #f cset?))
|
||||
;; Loop does not handle the return type or the keywords as they are handled before
|
||||
(define (loop V X Y s-arr t-arr)
|
||||
;; Currently checks is t-seq <: s-seq. Which works because argument list are contravariant.
|
||||
(define (loop V X Y s-seq t-seq)
|
||||
(define (cg S T) (cgen V X Y S T))
|
||||
(match*/early (s-arr t-arr)
|
||||
;; the simplest case - no rests, drests, keywords
|
||||
[((arr: ss _ #f #f _)
|
||||
(arr: ts _ #f #f _))
|
||||
(cgen/list V X Y ts ss)] ;; contravariant
|
||||
;; just a rest arg, no drest, no keywords
|
||||
[((arr: ss _ s-rest #f _)
|
||||
(arr: ts _ t-rest #f _))
|
||||
(cond
|
||||
;; both rest args are present, so make them the same length
|
||||
[(and s-rest t-rest)
|
||||
(cgen/list V X Y
|
||||
(cons t-rest (extend ss ts t-rest))
|
||||
(cons s-rest (extend ts ss s-rest)))]
|
||||
;; no rest arg on the right, so just pad the left and forget the rest arg
|
||||
[(and s-rest (not t-rest) (<= (length ss) (length ts)))
|
||||
(cgen/list V X Y ts (extend ts ss s-rest))]
|
||||
;; no rest arg on the left, or wrong number = fail
|
||||
[else #f])]
|
||||
(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 ts ss)]
|
||||
;; One is null-end the other is uniform-end
|
||||
[((seq ss (null-end))
|
||||
(seq ts (uniform-end t-rest)))
|
||||
#f]
|
||||
[((seq ss (uniform-end s-rest))
|
||||
(seq ts (null-end)))
|
||||
(and
|
||||
(<= (length ss) (length ts)))
|
||||
(cgen/list V X Y ts (extend ts ss s-rest))]
|
||||
;; Both are uniform-end
|
||||
[((seq ss (uniform-end s-rest))
|
||||
(seq ts (uniform-end t-rest)))
|
||||
(cgen/list V X Y
|
||||
(cons t-rest (extend ss ts t-rest))
|
||||
(cons s-rest (extend ts ss s-rest)))]
|
||||
;; dotted on the left, nothing on the right
|
||||
[((arr: ss s #f (cons dty dbound) s-kws)
|
||||
(arr: ts _ #f #f _))
|
||||
[((seq ss (dotted-end dty dbound))
|
||||
(seq ts (null-end)))
|
||||
#:return-unless (memq dbound Y)
|
||||
#f
|
||||
#:return-unless (<= (length ss) (length ts))
|
||||
|
|
@ -232,12 +243,12 @@
|
|||
(let* ([vars (var-store-take dbound dty (- (length ts) (length ss)))]
|
||||
[new-tys (for/list ([var (in-list vars)])
|
||||
(substitute (make-F var) dbound dty))]
|
||||
[new-s-arr (make-arr (append ss new-tys) s #f #f s-kws)]
|
||||
[new-cset (loop V (append vars X) Y new-s-arr t-arr)])
|
||||
[new-s-seq (seq (append ss new-tys) (null-end))]
|
||||
[new-cset (loop V (append vars X) Y new-s-seq t-seq)])
|
||||
(% move-vars-to-dmap new-cset dbound vars))]
|
||||
;; dotted on the right, nothing on the left
|
||||
[((arr: ss _ #f #f _)
|
||||
(arr: ts t #f (cons dty dbound) t-kws))
|
||||
[((seq ss (null-end))
|
||||
(seq ts (dotted-end dty dbound)))
|
||||
#:return-unless (memq dbound Y)
|
||||
#f
|
||||
#:return-unless (<= (length ts) (length ss))
|
||||
|
|
@ -245,12 +256,12 @@
|
|||
(let* ([vars (var-store-take dbound dty (- (length ss) (length ts)))]
|
||||
[new-tys (for/list ([var (in-list vars)])
|
||||
(substitute (make-F var) dbound dty))]
|
||||
[new-t-arr (make-arr (append ts new-tys) t #f #f t-kws)]
|
||||
[new-cset (loop V (append vars X) Y s-arr new-t-arr)])
|
||||
[new-t-seq (seq (append ts new-tys) (null-end))]
|
||||
[new-cset (loop V (append vars X) Y s-seq new-t-seq)])
|
||||
(% move-vars-to-dmap new-cset dbound vars))]
|
||||
;; this case is just for constrainting other variables, not dbound
|
||||
[((arr: ss _ #f (cons s-dty dbound) _)
|
||||
(arr: ts _ #f (cons t-dty dbound) _))
|
||||
[((seq ss (dotted-end s-dty dbound))
|
||||
(seq ts (dotted-end t-dty dbound)))
|
||||
#:return-unless (= (length ss) (length ts))
|
||||
#f
|
||||
;; If we want to infer the dotted bound, then why is it in both types?
|
||||
|
|
@ -260,8 +271,8 @@
|
|||
[darg-mapping (cgen V X Y t-dty s-dty)])
|
||||
(% cset-meet arg-mapping darg-mapping))]
|
||||
;; bounds are different
|
||||
[((arr: ss _ #f (cons s-dty (? (λ (db) (memq db Y)) dbound)) _)
|
||||
(arr: ts _ #f (cons t-dty dbound*) _))
|
||||
[((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
|
||||
(let* ([arg-mapping (cgen/list V X Y ts ss)]
|
||||
|
|
@ -270,8 +281,8 @@
|
|||
(extend-tvars (list dbound*)
|
||||
(% move-dotted-rest-to-dmap (cgen V (cons dbound X) Y t-dty s-dty) dbound dbound*))])
|
||||
(% cset-meet arg-mapping darg-mapping))]
|
||||
[((arr: ss _ #f (cons s-dty dbound) _)
|
||||
(arr: ts _ #f (cons t-dty (? (λ (db) (memq db Y)) dbound*)) _))
|
||||
[((seq ss (dotted-end s-dty dbound))
|
||||
(seq ts (dotted-end t-dty (? (λ (db) (memq db Y)) dbound*))))
|
||||
#:return-unless (= (length ss) (length ts)) #f
|
||||
(let* ([arg-mapping (cgen/list V X Y ts ss)]
|
||||
;; just add dbound as something that can be constrained
|
||||
|
|
@ -280,8 +291,8 @@
|
|||
(% move-dotted-rest-to-dmap (cgen V (cons dbound* X) Y t-dty s-dty) dbound* dbound))])
|
||||
(% cset-meet arg-mapping darg-mapping))]
|
||||
;; * <: ...
|
||||
[((arr: ss _ s-rest #f _)
|
||||
(arr: ts t #f (cons t-dty dbound) t-kws))
|
||||
[((seq ss (uniform-end s-rest))
|
||||
(seq ts (dotted-end t-dty dbound)))
|
||||
#:return-unless (memq dbound Y)
|
||||
#f
|
||||
(if (<= (length ss) (length ts))
|
||||
|
|
@ -294,12 +305,12 @@
|
|||
(let* ([vars (var-store-take dbound t-dty (- (length ss) (length ts)))]
|
||||
[new-tys (for/list ([var (in-list vars)])
|
||||
(substitute (make-F var) dbound t-dty))]
|
||||
[new-t-arr (make-arr (append ts new-tys) t #f (cons t-dty dbound) t-kws)]
|
||||
[new-cset (loop V (append vars X) Y s-arr new-t-arr)])
|
||||
[new-t-seq (seq (append ts new-tys) (dotted-end t-dty dbound))]
|
||||
[new-cset (loop V (append vars X) Y s-seq new-t-seq)])
|
||||
(% move-vars+rest-to-dmap new-cset dbound vars)))]
|
||||
;; If dotted <: starred is correct, add it below. Not sure it is.
|
||||
[((arr: ss s #f (cons s-dty dbound) s-kws)
|
||||
(arr: ts _ t-rest #f _))
|
||||
[((seq ss (dotted-end s-dty dbound))
|
||||
(seq ts (uniform-end t-rest)))
|
||||
#:return-unless (memq dbound Y)
|
||||
#f
|
||||
(cond [(< (length ss) (length ts))
|
||||
|
|
@ -307,8 +318,8 @@
|
|||
(let* ([vars (var-store-take dbound s-dty (- (length ts) (length ss)))]
|
||||
[new-tys (for/list ([var (in-list vars)])
|
||||
(substitute (make-F var) dbound s-dty))]
|
||||
[new-s-arr (make-arr (append ss new-tys) s #f (cons s-dty dbound) s-kws)]
|
||||
[new-cset (loop V (append vars X) Y new-s-arr t-arr)])
|
||||
[new-s-seq (make-arr (append ss new-tys) (dotted-end s-dty dbound))]
|
||||
[new-cset (loop V (append vars X) Y new-s-seq t-seq)])
|
||||
(% move-vars+rest-to-dmap new-cset dbound vars #:exact #t))]
|
||||
[(= (length ss) (length ts))
|
||||
;; the simple case
|
||||
|
|
@ -316,15 +327,23 @@
|
|||
[rest-mapping (cgen V (cons dbound X) Y t-rest s-dty)]
|
||||
[darg-mapping (% move-rest-to-dmap rest-mapping dbound #:exact #t)])
|
||||
(% cset-meet arg-mapping darg-mapping))]
|
||||
[else #f])]
|
||||
[(_ _) #f]))
|
||||
[else #f])]))
|
||||
|
||||
(match* (s-arr t-arr)
|
||||
[((arr: _ s _ _ s-kws) (arr: _ t _ _ t-kws))
|
||||
[((arr: ss s s-rest s-drest s-kws) (arr: ts t t-rest t-drest t-kws))
|
||||
(define (rest->end rest drest)
|
||||
(cond
|
||||
[rest (uniform-end rest)]
|
||||
[drest (dotted-end (car drest) (cdr drest))]
|
||||
[else (null-end)]))
|
||||
|
||||
(define s-seq (seq ss (rest->end s-rest s-drest)))
|
||||
(define t-seq (seq ts (rest->end t-rest t-drest)))
|
||||
(and (null? s-kws)
|
||||
(null? t-kws)
|
||||
(% cset-meet
|
||||
(cgen V X Y s t)
|
||||
(loop V X Y s-arr t-arr)))]))
|
||||
(loop V X Y s-seq t-seq)))]))
|
||||
|
||||
(define/cond-contract (cgen/flds V X Y flds-s flds-t)
|
||||
((listof symbol?) (listof symbol?) (listof symbol?) (listof fld?) (listof fld?)
|
||||
|
|
|
|||
|
|
@ -159,6 +159,7 @@
|
|||
[i2-t (-lst (-v a)) (-lst* N B) ('a (Un N B))]
|
||||
[i2-t Univ (Un N B)]
|
||||
[i2-t ((-v a) . -> . (-v b)) (-> N N) ('b N) ('a (Un))]
|
||||
[i2-t (-> (-v a) (-v a)) (->* null B B) ('a B)]
|
||||
|
||||
|
||||
[i2-l (list (-v a) (-v a) (-v b))
|
||||
|
|
@ -175,6 +176,7 @@
|
|||
'(a) ('a (Un N B))]
|
||||
;; error tests
|
||||
[i2-f (-lst (-v a)) Univ]
|
||||
[i2-f (->* null B B) (-> (-v a) (-v b))]
|
||||
))
|
||||
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user