relocate object subst code, work on fixing for indexes
original commit: 7b875d58a974a959a38a84197b413f91de83b5d1
This commit is contained in:
Sam Tobin-Hochstadt
parent
8f93f965fc
commit
686171190a
|
|
@ -3,6 +3,7 @@
|
|||
(require (rename-in "../utils/utils.ss" [infer r:infer])
|
||||
"signatures.ss" "tc-metafunctions.ss"
|
||||
"tc-app-helper.ss" "find-annotation.ss"
|
||||
"tc-subst.ss"
|
||||
syntax/parse scheme/match mzlib/trace scheme/list
|
||||
unstable/sequence
|
||||
;; fixme - don't need to be bound in this phase - only to make syntax/parse happy
|
||||
|
|
@ -731,7 +732,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) ...))
|
||||
[((arr: dom (Values: (and results (list (Result: t-r f-r o-r) ...))) rest #f (and kws (list (Keyword: _ _ #f) ...)))
|
||||
(list (tc-result1: t-a phi-a o-a) ...))
|
||||
;(printf "got to here 1~a~n" args-stx)
|
||||
(when check?
|
||||
|
|
@ -746,21 +747,16 @@
|
|||
[arg-t (in-list t-a)])
|
||||
(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 nm) (in-indexed (in-list dom))]
|
||||
[oa (in-list o-a)])
|
||||
(values nm oa))])
|
||||
;(printf "got to here 3~a~n" args-stx)
|
||||
(let* (;; Listof[FilterSet]
|
||||
[f-r (for/list ([f f-r])
|
||||
(apply-filter f names o-a))]
|
||||
;; Listof[Object]
|
||||
[o-r (for/list ([o o-r])
|
||||
(apply-object o names o-a))]
|
||||
;; Listof[Type]
|
||||
[t-r (for/list ([t t-r])
|
||||
(apply-type t names o-a))])
|
||||
(ret t-r f-r o-r)))]
|
||||
(let* ([dom-count (length dom)]
|
||||
[arg-count (+ dom-count (if rest 1 0) (length kws))]
|
||||
[o-a (for/list ([nm (in-range arg-count)]
|
||||
[oa (in-sequence-forever (in-list o-a) (make-Empty))])
|
||||
(if (>= nm dom-count) (make-Empty) oa))])
|
||||
(define-values (t-r f-r o-r)
|
||||
(for/lists (t-r f-r o-r)
|
||||
([r (in-list results)])
|
||||
(open-Result r o-a)))
|
||||
(ret t-r f-r o-r))]
|
||||
[((arr: _ _ _ drest '()) _)
|
||||
(int-err "funapp with drest args NYI")]
|
||||
[((arr: _ _ _ _ kws) _)
|
||||
|
|
|
|||
|
|
@ -30,6 +30,9 @@
|
|||
[((Bot:) _) (-FS -bot -top)]
|
||||
[(_ _) (-FS l1 l2)]))
|
||||
|
||||
(provide combine)
|
||||
|
||||
|
||||
(d/c/p (abstract-filters results)
|
||||
(tc-results? . -> . (or/c Values? ValuesDots?))
|
||||
(match results
|
||||
|
|
@ -83,111 +86,7 @@
|
|||
[(list (FilterSet: f+ f-) ...)
|
||||
(make-FilterSet (make-AndFilter f+) (make-AndFilter f-))]))
|
||||
|
||||
(d/c/p (apply-filter fs ids os [polarity #t])
|
||||
(->* (FilterSet/c (listof identifier?) (listof Object?)) (boolean?) FilterSet/c)
|
||||
(match fs
|
||||
[(FilterSet: f+ f-)
|
||||
(combine (subst-filter* f+ ids os polarity)
|
||||
(subst-filter* f- ids os polarity))]))
|
||||
|
||||
(d/c/p (apply-type t ids os [polarity #t])
|
||||
(->* (Type/c (listof identifier?) (listof Object?)) (boolean?) Type/c)
|
||||
(for/fold ([t t]) ([i (in-list ids)] [o (in-list os)])
|
||||
(subst-type t i o polarity)))
|
||||
|
||||
(d/c/p (apply-object t ids os [polarity #t])
|
||||
(->* (Object? (listof identifier?) (listof Object?)) (boolean?) Object?)
|
||||
(for/fold ([t t]) ([i (in-list ids)] [o (in-list os)])
|
||||
(subst-object t i o polarity)))
|
||||
|
||||
(define (subst-filter* f ids os polarity)
|
||||
(-> Filter/c (listof identifier?) (listof Object?) boolean? Filter/c)
|
||||
(for/fold ([f f]) ([i (in-list ids)] [o (in-list os)])
|
||||
(subst-filter f i o polarity)))
|
||||
|
||||
(d/c/p (subst-filter-set fs id o polarity)
|
||||
(-> FilterSet? identifier? Object? boolean? FilterSet?)
|
||||
(match fs
|
||||
[(FilterSet: f+ f-)
|
||||
(combine (subst-filter f+ id o polarity)
|
||||
(subst-filter f- id o polarity))]))
|
||||
|
||||
(define (subst-type t id o polarity)
|
||||
(define (st t) (subst-type t id o polarity))
|
||||
(d/c (sf fs) (FilterSet? . -> . FilterSet?) (subst-filter-set fs id o polarity))
|
||||
(type-case (#:Type st
|
||||
#:Filter sf
|
||||
#:Object (lambda (f) (subst-object f id o polarity)))
|
||||
t))
|
||||
|
||||
(define (subst-object t id o polarity)
|
||||
(match t
|
||||
[(NoObject:) t]
|
||||
[(Empty:) t]
|
||||
[(Path: p i)
|
||||
(if (free-identifier=? i id)
|
||||
(match o
|
||||
[(Empty:) (make-Empty)]
|
||||
;; the result is not from an annotation, so it isn't a NoObject
|
||||
[(NoObject:) (make-Empty)]
|
||||
[(Path: p* i*) (make-Path (append p p*) i*)])
|
||||
t)]))
|
||||
|
||||
;; this is the substitution metafunction
|
||||
(d/c/p (subst-filter f id o polarity)
|
||||
(-> Filter/c identifier? Object? boolean? Filter/c)
|
||||
(define (ap f) (subst-filter f o polarity))
|
||||
(define (tf-matcher t p i id o polarity maker)
|
||||
(match o
|
||||
[(or (Empty:) (NoObject:)) (if polarity -top -bot)]
|
||||
[(Path: p* i*)
|
||||
(cond [(free-identifier=? i id)
|
||||
(maker
|
||||
(subst-type t id o polarity)
|
||||
(append p p*)
|
||||
i*)]
|
||||
[(id-free-in? id t) (if polarity -top -bot)]
|
||||
[else f])]))
|
||||
(match f
|
||||
[(ImpFilter: ant consq)
|
||||
(make-ImpFilter (subst-filter ant id o (not polarity)) (ap consq))]
|
||||
[(AndFilter: fs) (make-AndFilter (map ap fs))]
|
||||
[(OrFilter: fs) (make-OrFilter (map ap fs))]
|
||||
[(Bot:) -bot]
|
||||
[(Top:) -top]
|
||||
[(TypeFilter: t p i)
|
||||
(tf-matcher t p i id o polarity make-TypeFilter)]
|
||||
[(NotTypeFilter: t p i)
|
||||
(tf-matcher t p i id o polarity make-NotTypeFilter)]))
|
||||
|
||||
(define (id-free-in? id type)
|
||||
(let/ec
|
||||
return
|
||||
(define (for-object o)
|
||||
(object-case (#:Type for-type)
|
||||
o
|
||||
[#:Path p i
|
||||
(if (free-identifier=? i id)
|
||||
(return #t)
|
||||
o)]))
|
||||
(define (for-filter o)
|
||||
(filter-case (#:Type for-type
|
||||
#:Filter for-filter)
|
||||
o
|
||||
[#:NotTypeFilter t p i
|
||||
(if (free-identifier=? i id)
|
||||
(return #t)
|
||||
o)]
|
||||
[#:TypeFilter t p i
|
||||
(if (free-identifier=? i id)
|
||||
(return #t)
|
||||
o)]))
|
||||
(define (for-type t)
|
||||
(type-case (#:Type for-type
|
||||
#:Filter for-filter
|
||||
#:Object for-object)
|
||||
t))
|
||||
(for-type type)))
|
||||
|
||||
#|
|
||||
#;
|
||||
|
|
@ -253,7 +152,7 @@
|
|||
(match tc
|
||||
[(tc-results: ts) (-values ts)]))
|
||||
|
||||
(provide combine-props tc-results->values subst-object subst-type)
|
||||
(provide combine-props tc-results->values)
|
||||
|
||||
(define (combine-props new-props old-props)
|
||||
(define-values (new-atoms new-formulas)
|
||||
|
|
|
|||
131
collects/typed-scheme/typecheck/tc-subst.ss
Normal file
131
collects/typed-scheme/typecheck/tc-subst.ss
Normal file
|
|
@ -0,0 +1,131 @@
|
|||
#lang scheme/base
|
||||
|
||||
(require "../utils/utils.ss")
|
||||
(require (rename-in (types subtype convenience remove-intersect union utils)
|
||||
[-> -->]
|
||||
[->* -->*]
|
||||
[one-of/c -one-of/c])
|
||||
(rep type-rep filter-rep rep-utils) scheme/list
|
||||
scheme/contract scheme/match unstable/match
|
||||
(for-syntax scheme/base)
|
||||
"tc-metafunctions.ss")
|
||||
|
||||
;(provide (all-defined-out))
|
||||
|
||||
(define-syntax-rule (d/c/p (name . args) c . body)
|
||||
(begin (d/c (name . args) c . body)
|
||||
(p/c [name c])))
|
||||
|
||||
(d/c/p (open-Result r objs)
|
||||
(-> Result? (listof Object?) Result?)
|
||||
(for/fold ([r r])
|
||||
([(o k) (in-indexed (in-list objs))])
|
||||
(match r
|
||||
[(Result: t fs old-obj)
|
||||
(make-Result (subst-type t k o #t)
|
||||
(subst-filter-set t fs o #t)
|
||||
(subst-object t old-obj o #t))])))
|
||||
|
||||
(d/c/p (subst-filter-set fs k o polarity)
|
||||
(-> FilterSet? integer? Object? boolean? FilterSet?)
|
||||
(match fs
|
||||
[(FilterSet: f+ f-)
|
||||
(combine (subst-filter f+ k o polarity)
|
||||
(subst-filter f- k o polarity))]))
|
||||
|
||||
(d/c (subst-type t k o polarity)
|
||||
(-> Type/c integer? Object? boolean? Type/c)
|
||||
(define (st t) (subst-type t k o polarity))
|
||||
(d/c (sf fs) (FilterSet? . -> . FilterSet?) (subst-filter-set fs k o polarity))
|
||||
(type-case (#:Type st
|
||||
#:Filter sf
|
||||
#:Object (lambda (f) (subst-object f k o polarity)))
|
||||
t
|
||||
[#:arr dom rng rest drest kws
|
||||
;; here we have to increment the count for the domain, where the new bindings are in scope
|
||||
(let* ([arg-count (+ (length dom) (if rest 1 0) (if drest 1 0) (length kws))]
|
||||
[st* (lambda (t) (subst-type t (+ arg-count k) o polarity))])
|
||||
(make-arr (map st dom)
|
||||
(st* rng)
|
||||
(and rest (st rest))
|
||||
(and drest (cons (st (car drest)) (cdr drest)))
|
||||
(map st kws)))]))
|
||||
|
||||
(d/c (subst-object t k o polarity)
|
||||
(-> Object? integer? Object? boolean? Object?)
|
||||
(match t
|
||||
[(NoObject:) t]
|
||||
[(Empty:) t]
|
||||
[(Path: p i)
|
||||
(if (eq? i k)
|
||||
(match o
|
||||
[(Empty:) (make-Empty)]
|
||||
;; the result is not from an annotation, so it isn't a NoObject
|
||||
[(NoObject:) (make-Empty)]
|
||||
[(Path: p* i*) (make-Path (append p p*) i*)])
|
||||
t)]))
|
||||
|
||||
;; this is the substitution metafunction
|
||||
(d/c/p (subst-filter f k o polarity)
|
||||
(-> Filter/c integer? Object? boolean? Filter/c)
|
||||
(define (ap f) (subst-filter f o polarity))
|
||||
(define (tf-matcher t p i k o polarity maker)
|
||||
(match o
|
||||
[(or (Empty:) (NoObject:)) (if polarity -top -bot)]
|
||||
[(Path: p* i*)
|
||||
(cond [(eq? i k)
|
||||
(maker
|
||||
(subst-type t k o polarity)
|
||||
(append p p*)
|
||||
i*)]
|
||||
[(index-free-in? k t) (if polarity -top -bot)]
|
||||
[else f])]))
|
||||
(match f
|
||||
[(ImpFilter: ant consq)
|
||||
(make-ImpFilter (subst-filter ant k o (not polarity)) (ap consq))]
|
||||
[(AndFilter: fs) (make-AndFilter (map ap fs))]
|
||||
[(OrFilter: fs) (make-OrFilter (map ap fs))]
|
||||
[(Bot:) -bot]
|
||||
[(Top:) -top]
|
||||
[(TypeFilter: t p i)
|
||||
(tf-matcher t p i k o polarity make-TypeFilter)]
|
||||
[(NotTypeFilter: t p i)
|
||||
(tf-matcher t p i k o polarity make-NotTypeFilter)]))
|
||||
|
||||
(define (index-free-in? k type)
|
||||
(let/ec
|
||||
return
|
||||
(define (for-object o)
|
||||
(object-case (#:Type for-type)
|
||||
o
|
||||
[#:Path p i
|
||||
(if (eq? i k)
|
||||
(return #t)
|
||||
o)]))
|
||||
(define (for-filter o)
|
||||
(filter-case (#:Type for-type
|
||||
#:Filter for-filter)
|
||||
o
|
||||
[#:NotTypeFilter t p i
|
||||
(if (eq? i k)
|
||||
(return #t)
|
||||
o)]
|
||||
[#:TypeFilter t p i
|
||||
(if (eq? i k)
|
||||
(return #t)
|
||||
o)]))
|
||||
(define (for-type t)
|
||||
(type-case (#:Type for-type
|
||||
#:Filter for-filter
|
||||
#:Object for-object)
|
||||
t
|
||||
[#:arr dom rng rest drest kws
|
||||
;; here we have to increment the count for the domain, where the new bindings are in scope
|
||||
(let* ([arg-count (+ (length dom) (if rest 1 0) (if drest 1 0) (length kws))]
|
||||
[st* (lambda (t) (for-type (+ arg-count k) t))])
|
||||
(make-arr (map for-type dom)
|
||||
(st* rng)
|
||||
(and rest (for-type rest))
|
||||
(and drest (cons (for-type (car drest)) (cdr drest)))
|
||||
(map for-type kws)))]))
|
||||
(for-type type)))
|
||||
Loading…
Reference in New Issue
Block a user