Stars and dots living together, mass hysteria.
This commit is contained in:
Stevie Strickland
parent
1a7629ea3b
commit
9e78f5d0c0
34
collects/typed-scheme/private/constraint-structs.ss
Normal file
34
collects/typed-scheme/private/constraint-structs.ss
Normal file
|
|
@ -0,0 +1,34 @@
|
|||
#lang scheme/base
|
||||
|
||||
(require "type-rep.ss"
|
||||
scheme/contract)
|
||||
|
||||
;; S, T types
|
||||
;; X a var
|
||||
(define-struct c (S X T) #:prefab)
|
||||
|
||||
;; fixed : Listof[c]
|
||||
;; rest : option[c]
|
||||
(define-struct dcon (fixed rest) #:prefab)
|
||||
|
||||
;; map : hash mapping variable to dcon
|
||||
(define-struct dmap (map) #:prefab)
|
||||
|
||||
;; maps is a list of pairs of
|
||||
;; - functional maps from vars to c's
|
||||
;; - dmaps (see dmap.ss)
|
||||
;; we need a bunch of mappings for each cset to handle case-lambda
|
||||
;; because case-lambda can generate multiple possible solutions, and we
|
||||
;; don't want to rule them out too early
|
||||
(define-struct cset (maps) #:prefab)
|
||||
|
||||
(define (hashof k/c v/c)
|
||||
(lambda (h)
|
||||
(and (hash? h)
|
||||
(for/and ([(k v) h])
|
||||
(and (k/c k) (v/c v))))))
|
||||
|
||||
(provide/contract (struct c ([S Type?] [X symbol?] [T Type?]))
|
||||
(struct dcon ([fixed (listof c?)] [rest (or/c c? false/c)]))
|
||||
(struct dmap ([map (hashof symbol? dcon?)]))
|
||||
(struct cset ([maps (listof (cons/c (hashof symbol? c?) dmap?))])))
|
||||
|
|
@ -3,7 +3,7 @@
|
|||
(require "type-effect-convenience.ss" "type-rep.ss"
|
||||
"type-utils.ss" "union.ss" "tc-utils.ss"
|
||||
"subtype.ss" "utils.ss"
|
||||
"signatures.ss"
|
||||
"signatures.ss" "constraint-structs.ss"
|
||||
scheme/match)
|
||||
|
||||
(import restrict^ dmap^)
|
||||
|
|
@ -20,27 +20,13 @@
|
|||
(syntax-rules ()
|
||||
[(_ s t) (raise fail-sym)]))
|
||||
|
||||
|
||||
;; S, T types
|
||||
;; X a var
|
||||
(define-struct c (S X T) #:prefab)
|
||||
|
||||
;; maps is a list of pairs of
|
||||
;; - functional maps from vars to c's
|
||||
;; - dmaps (see dmap.ss)
|
||||
;; we need a bunch of mappings for each cset to handle case-lambda
|
||||
;; because case-lambda can generate multiple possible solutions, and we
|
||||
;; don't want to rule them out too early
|
||||
(define-struct cset (maps) #:prefab)
|
||||
|
||||
;; Widest constraint possible
|
||||
(define (no-constraint v)
|
||||
(make-c (Un) v Univ))
|
||||
|
||||
(define (empty-cset X)
|
||||
(make-cset (list (cons (for/hash ([x X]) (values x (no-constraint x)))
|
||||
(make-immutable-hash null)))))
|
||||
|
||||
(make-dmap (make-immutable-hash null))))))
|
||||
|
||||
#;
|
||||
(define (lookup cset var)
|
||||
|
|
@ -94,14 +80,15 @@
|
|||
(dmap-meet dmap1 dmap2)))))])
|
||||
(when (null? maps)
|
||||
(fail! maps1 maps2))
|
||||
(make-cset maps))]))
|
||||
(make-cset maps))]
|
||||
[(_ _) (int-err "Got non-cset: ~a ~a" x y)]))
|
||||
|
||||
(define (cset-meet* args)
|
||||
(for/fold ([c (make-immutable-hash null)])
|
||||
(for/fold ([c (make-cset (list (cons (make-immutable-hash null)
|
||||
(make-dmap (make-immutable-hash null)))))])
|
||||
([a args])
|
||||
(cset-meet a c)))
|
||||
|
||||
|
||||
(define (cset-combine l)
|
||||
(let ([mapss (map cset-maps l)])
|
||||
(make-cset (apply append mapss))))
|
||||
|
|
|
|||
|
|
@ -1,17 +1,11 @@
|
|||
#lang scheme/unit
|
||||
|
||||
(require "signatures.ss" "utils.ss" "tc-utils.ss" scheme/match)
|
||||
(require "signatures.ss" "utils.ss" "tc-utils.ss" "constraint-structs.ss"
|
||||
scheme/match)
|
||||
|
||||
(import constraints^)
|
||||
(export dmap^)
|
||||
|
||||
;; map : hash mapping variable to dcon
|
||||
(define-struct dmap (map))
|
||||
|
||||
;; fixed : Listof[c]
|
||||
;; rest : option[c]
|
||||
(define-struct dcon (fixed rest))
|
||||
|
||||
;; dcon-meet : dcon dcon -> dcon
|
||||
(define (dcon-meet dc1 dc2)
|
||||
(match* (dc1 dc2)
|
||||
|
|
@ -42,9 +36,10 @@
|
|||
(for/list ([c1 longer]
|
||||
[c2 (in-list-forever shorter srest)])
|
||||
(c-meet c1 c2 (c-X c1)))
|
||||
(c-meet lrest srest (c-X lrest))))]))
|
||||
(c-meet lrest srest (c-X lrest))))]
|
||||
[(_ _) (int-err "Got non-dcons: ~a ~a" dc1 dc2)]))
|
||||
|
||||
(define (dmap-meet dm1 dm2)
|
||||
(hash-union dm1 dm2
|
||||
(lambda (k dc1 dc2) (dcon-meet dc1 dc2))))
|
||||
|
||||
(make-dmap
|
||||
(hash-union (dmap-map dm1) (dmap-map dm2)
|
||||
(lambda (k dc1 dc2) (dcon-meet dc1 dc2)))))
|
||||
|
|
@ -3,12 +3,13 @@
|
|||
(require "type-effect-convenience.ss" "type-rep.ss" "effect-rep.ss" "rep-utils.ss"
|
||||
"free-variance.ss" "type-utils.ss" "union.ss" "tc-utils.ss" "type-name-env.ss"
|
||||
"subtype.ss" "remove-intersect.ss" "signatures.ss" "utils.ss"
|
||||
"constraint-structs.ss"
|
||||
scheme/match
|
||||
mzlib/etc
|
||||
mzlib/trace
|
||||
scheme/list)
|
||||
|
||||
(import constraints^ promote-demote^)
|
||||
(import dmap^ constraints^ promote-demote^)
|
||||
(export infer^)
|
||||
|
||||
(define (empty-set) '())
|
||||
|
|
@ -19,9 +20,45 @@
|
|||
(define (remember s t A) (cons (seen-before s t) A))
|
||||
(define (seen? s t) (member (seen-before s t) (current-seen)))
|
||||
|
||||
(define (add-var-mapping cset dbound vars)
|
||||
(make-cset (for/list ([(cs vs) (in-pairs (cset-maps cset))])
|
||||
(cons cs (hash-set vs dbound vars)))))
|
||||
|
||||
(define (dmap-constraint dmap dbound v)
|
||||
(let ([dc (hash-ref dmap dbound #f)])
|
||||
(match dc
|
||||
[(struct dcon (fixed #f))
|
||||
(if (eq? dbound v)
|
||||
(no-constraint v)
|
||||
(hash-ref fixed v (no-constraint v)))]
|
||||
[(struct dcon (fixed rest))
|
||||
(if (eq? dbound v)
|
||||
rest
|
||||
(hash-ref fixed v (no-constraint v)))]
|
||||
[_ (no-constraint v)])))
|
||||
|
||||
(define (move-vars-to-dmap cset dbound vars)
|
||||
(make-cset (for/list ([(cmap dmap) (in-pairs (cset-maps cset))])
|
||||
(cons (foldl (lambda (v cmap)
|
||||
(hash-remove cmap v))
|
||||
cmap vars)
|
||||
(dmap-meet (make-dmap
|
||||
(make-immutable-hash
|
||||
(list (cons dbound
|
||||
(make-dcon (for/list ([v vars])
|
||||
(hash-ref cmap v
|
||||
(lambda () (int-err "No constraint for new var ~a" v))))
|
||||
#f)))))
|
||||
dmap)))))
|
||||
|
||||
(define (move-rest-to-dmap cset dbound)
|
||||
(make-cset (for/list ([(cmap dmap) (in-pairs (cset-maps cset))])
|
||||
(cons (hash-remove cmap dbound)
|
||||
(dmap-meet (make-dmap
|
||||
(make-immutable-hash
|
||||
(list (cons dbound
|
||||
(make-dcon null
|
||||
(hash-ref cmap dbound
|
||||
(lambda () (int-err "No constraint for bound ~a" dbound))))))))
|
||||
dmap)))))
|
||||
|
||||
|
||||
;; ss and ts have the same length
|
||||
(define (cgen-union V X ss ts)
|
||||
|
|
@ -64,7 +101,7 @@
|
|||
[new-tys (for/list ([var vars])
|
||||
(substitute (make-F var) dbound dty))]
|
||||
[new-cset (cgen/arr V (append vars X) (make-arr (append ts new-tys) t #f #f t-thn-eff t-els-eff) s-arr)])
|
||||
(add-var-mapping new-cset dbound vars))]
|
||||
(move-vars-to-dmap new-cset dbound vars))]
|
||||
[((arr: ts t #f #f t-thn-eff t-els-eff)
|
||||
(arr: ss s #f (cons dty dbound) s-thn-eff s-els-eff))
|
||||
(unless (memq dbound X)
|
||||
|
|
@ -77,8 +114,7 @@
|
|||
[new-tys (for/list ([var vars])
|
||||
(substitute (make-F var) dbound dty))]
|
||||
[new-cset (cgen/arr V (append vars X) t-arr (make-arr (append ss new-tys) s #f #f s-thn-eff s-els-eff))])
|
||||
(make-cset (for/list ([(cs vs) (in-pairs (cset-maps new-cset))])
|
||||
(cons cs (hash-set vs dbound vars)))))]
|
||||
(move-vars-to-dmap new-cset dbound vars))]
|
||||
[((arr: ts t #f (cons t-dty dbound) t-thn-eff t-els-eff)
|
||||
(arr: ss s #f (cons s-dty dbound) s-thn-eff s-els-eff))
|
||||
(unless (= (length ts) (length ss))
|
||||
|
|
@ -92,37 +128,23 @@
|
|||
(cset-meet* (list arg-mapping darg-mapping ret-mapping)))]
|
||||
[((arr: ts t t-rest #f t-thn-eff t-els-eff)
|
||||
(arr: ss s #f (cons s-dty dbound) s-thn-eff s-els-eff))
|
||||
(unless (memq dbound X)
|
||||
(fail! S T))
|
||||
(unless (<= (length ts) (length ss))
|
||||
(fail! S T))
|
||||
(let* ([arg-mapping (cgen/list X V ss (extend ss ts t-rest))]
|
||||
[darg-mapping (cgen (cons dbound V) X s-dty t-rest)]
|
||||
[darg-mapping (move-rest-to-dmap (cgen (cons dbound V) X s-dty t-rest) dbound)]
|
||||
[ret-mapping (cg t s)])
|
||||
(let-values ([(darg-mapping* dbound-constraint)
|
||||
(split-mapping darg-mapping dbound)])
|
||||
(add-var-mapping (cset-meet* (list arg-mapping darg-mapping* ret-mapping))
|
||||
dbound
|
||||
dbound-constraint)))]
|
||||
(cset-meet* (list arg-mapping darg-mapping ret-mapping)))]
|
||||
;; If dotted <: starred is correct, add it below. Not sure it is.
|
||||
[(_ _) (fail! S T)]))
|
||||
|
||||
;; split-mapping : cset symbol -> (values cset clist)
|
||||
(define (split-mapping mapping var)
|
||||
(let-values ([(mappings cs)
|
||||
(for/fold ([mapping null]
|
||||
[constraints null])
|
||||
([(map dmap) (in-pairs (cset-maps mapping))])
|
||||
(when (hash-ref dmap var #f)
|
||||
(int-err "Got constraints for var ~a: ~a" var (hash-ref dmap var #f)))
|
||||
(values (cons (cons (hash-remove map var) dmap) mapping)
|
||||
(let ([var-c (hash-ref map var #f)])
|
||||
(if var-c (cons var-c constraints) constraints))))])
|
||||
(values (make-cset mappings) (make-clist cs))))
|
||||
|
||||
(define (singleton S X T)
|
||||
(insert (empty-cset X) X S T))
|
||||
|
||||
(define (cgen V X S T)
|
||||
(define (cg S T) (cgen V X S T))
|
||||
(define empty (empty-cset X))
|
||||
(define (singleton S X T)
|
||||
(insert empty X S T))
|
||||
#;(printf "In cgen: ~a ~a~n" S T)
|
||||
(if (seen? S T)
|
||||
empty
|
||||
(parameterize ([match-equality-test type-equal?]
|
||||
|
|
@ -271,7 +293,7 @@
|
|||
[new-Ts (for/list ([v new-vars])
|
||||
(substitute (make-F v) dotted-var T-dotted))]
|
||||
[cs-dotted (cgen/list (append new-vars X) null rest-S new-Ts)]
|
||||
[cs-dotted* (add-var-mapping cs-dotted dotted-var new-vars)]
|
||||
[cs-dotted* (move-vars-to-dmap cs-dotted dotted-var new-vars)]
|
||||
[cs (cset-meet cs-short cs-dotted*)])
|
||||
(if (not expected)
|
||||
(subst-gen cs R)
|
||||
|
|
|
|||
|
|
@ -3,28 +3,24 @@
|
|||
(provide (all-defined-out))
|
||||
|
||||
(define-signature dmap^
|
||||
((struct dmap (map))
|
||||
(struct dcon (fixed rest))
|
||||
dmap-meet))
|
||||
(dmap-meet))
|
||||
|
||||
(define-signature promote-demote^
|
||||
(var-promote var-demote))
|
||||
|
||||
(define-signature constraints^
|
||||
((struct cset (maps))
|
||||
exn:infer?
|
||||
(exn:infer?
|
||||
fail-sym
|
||||
;; inference failure - masked before it gets to the user program
|
||||
(define-syntaxes (fail!)
|
||||
(syntax-rules ()
|
||||
[(_ s t) (raise fail-sym)]))
|
||||
cset-meet cset-meet*
|
||||
(struct clist (cs))
|
||||
no-constraint
|
||||
empty-cset
|
||||
insert
|
||||
cset-combine
|
||||
c-meet
|
||||
(struct c (S X T))))
|
||||
c-meet))
|
||||
|
||||
(define-signature restrict^
|
||||
(restrict))
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user