Stop using eq? for types.
More contracts. Fix some contract errors. svn: r17943 original commit: 9939f4b6194f61ff1bbed48ef3b36c7dba41363d
This commit is contained in:
parent
cec76e7ad4
commit
b1a442d1f0
|
@ -13,7 +13,7 @@
|
|||
|
||||
|
||||
(define-values (fail-sym exn:infer?)
|
||||
(let ([sym (gensym)])
|
||||
(let ([sym (gensym 'infer-fail)])
|
||||
(values sym (lambda (s) (eq? s sym)))))
|
||||
|
||||
;; why does this have to be duplicated?
|
||||
|
|
|
@ -12,7 +12,7 @@
|
|||
scheme/match
|
||||
mzlib/etc
|
||||
mzlib/trace
|
||||
unstable/sequence unstable/list
|
||||
unstable/sequence unstable/list unstable/debug
|
||||
scheme/list)
|
||||
|
||||
(import dmap^ constraints^ promote-demote^)
|
||||
|
@ -254,7 +254,7 @@
|
|||
(insert empty X S T))
|
||||
(if (seen? S T)
|
||||
empty
|
||||
(parameterize ([match-equality-test type-equal?]
|
||||
(parameterize ([match-equality-test (lambda (a b) (if (and (Rep? a) (Rep? b)) (type-equal? a b) (equal? a b)))]
|
||||
[current-seen (remember S T (current-seen))])
|
||||
(match*
|
||||
(S T)
|
||||
|
|
|
@ -246,7 +246,7 @@
|
|||
[Rep-free-vars free-vars*]
|
||||
[Rep-free-idxs free-idxs*]))
|
||||
|
||||
(p/c (struct Rep ([seq integer?]
|
||||
(p/c (struct Rep ([seq exact-nonnegative-integer?]
|
||||
[free-vars (hash/c symbol? variance?)]
|
||||
[free-idxs (hash/c exact-nonnegative-integer? variance?)]
|
||||
[stx (or/c #f syntax?)])))
|
||||
|
|
|
@ -230,25 +230,24 @@
|
|||
;; elems : Listof[Type]
|
||||
(dt Union ([elems (and/c (listof Type/c)
|
||||
(lambda (es)
|
||||
(let-values ([(sorted? k)
|
||||
(for/fold ([sorted? #t]
|
||||
[last -1])
|
||||
([e es])
|
||||
(let ([seq (Rep-seq e)])
|
||||
(values
|
||||
(and sorted?
|
||||
(< last seq))
|
||||
seq)))])
|
||||
sorted?)))])
|
||||
(or (null? es)
|
||||
(let-values ([(sorted? k)
|
||||
(for/fold ([sorted? #t]
|
||||
[last (car es)])
|
||||
([e (cdr es)])
|
||||
(values
|
||||
(and sorted? (type<? last e))
|
||||
e))])
|
||||
sorted?))))])
|
||||
[#:frees (combine-frees (map free-vars* elems))
|
||||
(combine-frees (map free-idxs* elems))]
|
||||
[#:fold-rhs ((get-union-maker) (map type-rec-id elems))]
|
||||
[#:key (let loop ([res null] [ts elems])
|
||||
(if (null? ts) res
|
||||
(let ([k (Type-key (car ts))])
|
||||
(cond [(pair? k) (loop (append k res) (cdr ts))]
|
||||
[k (loop (cons k res) (cdr ts))]
|
||||
[else #f]))))])
|
||||
(if (null? ts) res
|
||||
(let ([k (Type-key (car ts))])
|
||||
(cond [(pair? k) (loop (append k res) (cdr ts))]
|
||||
[k (loop (cons k res) (cdr ts))]
|
||||
[else #f]))))])
|
||||
|
||||
(dt Univ () [#:frees #f] [#:fold-rhs #:base])
|
||||
|
||||
|
@ -319,7 +318,8 @@
|
|||
|
||||
;; remove-dups: List[Type] -> List[Type]
|
||||
;; removes duplicate types from a SORTED list
|
||||
(define (remove-dups types)
|
||||
(d/c (remove-dups types)
|
||||
((listof Rep?) . -> . (listof Rep?))
|
||||
(cond [(null? types) types]
|
||||
[(null? (cdr types)) types]
|
||||
[(type-equal? (car types) (cadr types)) (remove-dups (cdr types))]
|
||||
|
@ -341,15 +341,16 @@
|
|||
[_ (int-err "Tried to remove too many scopes: ~a" sc)])))
|
||||
|
||||
;; type equality
|
||||
(define type-equal? eq?)
|
||||
(d/c (type-equal? s t) (Rep? Rep? . -> . boolean?) (eq? (Rep-seq s) (Rep-seq t)))
|
||||
|
||||
;; inequality - good
|
||||
(d/c (type<? s t)
|
||||
(Rep? Rep? . -> . boolean?)
|
||||
(< (Rep-seq s) (Rep-seq t)))
|
||||
|
||||
(define (type<? s t)
|
||||
(< (Type-seq s) (Type-seq t)))
|
||||
|
||||
(define (type-compare s t)
|
||||
(cond [(eq? s t) 0]
|
||||
(d/c (type-compare s t)
|
||||
(Rep? Rep? . -> . (or/c -1 0 1))
|
||||
(cond [(type-equal? s t) 0]
|
||||
[(type<? s t) 1]
|
||||
[else -1]))
|
||||
|
||||
|
@ -606,7 +607,7 @@
|
|||
Poly-n
|
||||
PolyDots-n
|
||||
free-vars*
|
||||
type-equal? type-compare type<?
|
||||
type-compare type<?
|
||||
remove-dups
|
||||
sub-lf sub-lo sub-pe
|
||||
Values: Values? Values-rs
|
||||
|
@ -620,4 +621,6 @@
|
|||
[Poly-body* Poly-body]
|
||||
[PolyDots-body* PolyDots-body]))
|
||||
|
||||
(p/c [type-equal? (Rep? Rep? . -> . boolean?)])
|
||||
|
||||
;(trace unfold)
|
||||
|
|
|
@ -3,7 +3,7 @@
|
|||
(require "../utils/utils.ss"
|
||||
syntax/kerncase
|
||||
syntax/parse
|
||||
scheme/match
|
||||
scheme/match unstable/debug
|
||||
"signatures.ss" "tc-metafunctions.ss"
|
||||
(types utils convenience union subtype)
|
||||
(utils tc-utils)
|
||||
|
@ -14,7 +14,7 @@
|
|||
|
||||
;; find the subexpressions that need to be typechecked in an ignored form
|
||||
;; syntax -> any
|
||||
(define (check-subforms/with-handlers form)
|
||||
(define (check-subforms/with-handlers form [expected #f])
|
||||
(define handler-tys '())
|
||||
(define body-ty #f)
|
||||
(define (get-result-ty t)
|
||||
|
|
|
@ -677,7 +677,6 @@
|
|||
(and vars (list fixed-vars ... dotted-var))
|
||||
(Function: (list (and arrs (arr: doms rngs rests drests (list (Keyword: _ _ #f) ...))) ...)))))
|
||||
(list (tc-result1: argtys-t) ...))
|
||||
(printf "poly clause 1~n")
|
||||
(handle-clauses (doms rngs rests drests arrs) f-stx args-stx
|
||||
;; only try inference if the argument lengths are appropriate
|
||||
(lambda (dom _ rest drest a)
|
||||
|
|
|
@ -79,9 +79,12 @@
|
|||
[(ImpFilter: as cs)
|
||||
(let ([a* (apply append (for/list ([f as]) (abo xs idxs f)))]
|
||||
[c* (apply append (for/list ([f cs]) (abo xs idxs f)))])
|
||||
(if (< (length a*) (length as)) ;; if we removed some things, we can't be sure
|
||||
null
|
||||
(list (make-LImpFilter a* c*))))]
|
||||
(cond [(< (length a*) (length as)) ;; if we removed some things, we can't be sure
|
||||
null]
|
||||
[(null? c*) ;; this clause is now useless
|
||||
null]
|
||||
[else
|
||||
(list (make-LImpFilter a* c*))]))]
|
||||
[_ null]))
|
||||
|
||||
(define (merge-filter-sets fs)
|
||||
|
@ -118,8 +121,8 @@
|
|||
(define (idx= lf)
|
||||
(match lf
|
||||
[(LBot:) #t]
|
||||
[(LNotTypeFilter: _ _ idx*) (type-equal? idx* idx)]
|
||||
[(LTypeFilter: _ _ idx*) (type-equal? idx* idx)]))
|
||||
[(LNotTypeFilter: _ _ idx*) (= idx* idx)]
|
||||
[(LTypeFilter: _ _ idx*) (= idx* idx)]))
|
||||
(match lf
|
||||
[(LFilterSet: lf+ lf-)
|
||||
(make-LFilterSet (filter idx= lf+) (filter idx= lf-))]))
|
||||
|
|
|
@ -66,8 +66,10 @@
|
|||
(make-Result t f o))
|
||||
|
||||
(d/c (-values args)
|
||||
(c:-> (listof Type/c) Values?)
|
||||
(make-Values (for/list ([i args]) (-result i))))
|
||||
(c:-> (listof Type/c) (or/c Type/c Values?))
|
||||
(match args
|
||||
;[(list t) t]
|
||||
[_ (make-Values (for/list ([i args]) (-result i)))]))
|
||||
|
||||
;; basic types
|
||||
|
||||
|
|
|
@ -200,7 +200,7 @@
|
|||
;; potentially raises exn:subtype, when the algorithm fails
|
||||
;; is s a subtype of t, taking into account constraints A
|
||||
(define (subtype* A s t)
|
||||
(parameterize ([match-equality-test type-equal?]
|
||||
(parameterize ([match-equality-test (lambda (a b) (if (and (Rep? a) (Rep? b)) (type-equal? a b) (equal? a b)))]
|
||||
[current-seen A])
|
||||
(let ([ks (Type-key s)] [kt (Type-key t)])
|
||||
(cond
|
||||
|
|
|
@ -19,7 +19,9 @@
|
|||
(define (flat t)
|
||||
(match t
|
||||
[(Union: es) es]
|
||||
[_ (list t)]))
|
||||
[(Values: (list (Result: (Union: es) _ _))) es]
|
||||
[(Values: (list (Result: t _ _))) (list t)]
|
||||
[_ (list t)]))
|
||||
|
||||
(define (remove-subtypes ts)
|
||||
(let loop ([ts* ts] [result '()])
|
||||
|
@ -44,7 +46,7 @@
|
|||
(cond
|
||||
[(null? types) (make-union* null)]
|
||||
[(null? (cdr types)) (car types)]
|
||||
[else (make-union* (foldr union2 '() (remove-subtypes types)))]))]))
|
||||
[else (make-union* (sort (foldr union2 '() (remove-subtypes types)) type<?))]))]))
|
||||
|
||||
(define (u-maker args) (apply Un args))
|
||||
|
||||
|
|
Loading…
Reference in New Issue
Block a user