remove obselete code
svn: r14941
This commit is contained in:
Sam Tobin-Hochstadt
parent
a8ee2dc161
commit
2a55bec335
|
|
@ -1,834 +0,0 @@
|
|||
#lang scheme/unit
|
||||
|
||||
(require (only-in "../utils/utils.ss" debug in-syntax printf/log in-pairs rep utils private env [infer r:infer]))
|
||||
(require "signatures.ss"
|
||||
stxclass
|
||||
(for-syntax stxclass)
|
||||
(rep type-rep effect-rep)
|
||||
(utils tc-utils)
|
||||
(private subtype type-utils union type-effect-convenience type-effect-printer resolve-type
|
||||
type-annotation)
|
||||
(r:infer infer)
|
||||
(env type-environments)
|
||||
(only-in srfi/1 alist-delete)
|
||||
(only-in scheme/private/class-internal make-object do-make-object)
|
||||
mzlib/trace mzlib/pretty syntax/kerncase scheme/match
|
||||
(prefix-in c: scheme/contract)
|
||||
(for-syntax scheme/base)
|
||||
(for-template
|
||||
(only-in '#%kernel [apply k:apply])
|
||||
"internal-forms.ss" scheme/base
|
||||
(only-in scheme/private/class-internal make-object do-make-object)))
|
||||
(require (r:infer constraint-structs))
|
||||
|
||||
(import tc-expr^ tc-lambda^ tc-dots^ tc-let^)
|
||||
(export tc-app^)
|
||||
|
||||
;; comparators that inform the type system
|
||||
(define (comparator? i)
|
||||
(or (free-identifier=? i #'eq?)
|
||||
(free-identifier=? i #'equal?)
|
||||
(free-identifier=? i #'eqv?)
|
||||
(free-identifier=? i #'=)
|
||||
(free-identifier=? i #'string=?)))
|
||||
|
||||
;; typecheck eq? applications
|
||||
;; identifier identifier expression expression expression
|
||||
;; identifier expr expr expr expr -> tc-result
|
||||
(define (tc/eq comparator v1 v2)
|
||||
(define (e? i) (free-identifier=? i comparator))
|
||||
(define (do id val)
|
||||
(define-syntax alt (syntax-rules () [(_ nm pred ...)
|
||||
(and (e? #'nm) (or (pred val) ...))]))
|
||||
(if (or (alt symbol=? symbol?)
|
||||
(alt string=? string?)
|
||||
(alt = number?)
|
||||
(alt eq? boolean? keyword? symbol?)
|
||||
(alt eqv? boolean? keyword? symbol? number?)
|
||||
(alt equal? (lambda (x) #t)))
|
||||
(values (list (make-Restrict-Effect (-val val) id))
|
||||
(list (make-Remove-Effect (-val val) id)))
|
||||
(values (list) (list))))
|
||||
(match (list (tc-expr v1) (tc-expr v2))
|
||||
[(list (tc-result: id-t (list (Var-True-Effect: id1)) (list (Var-False-Effect: id2))) (tc-result: (Value: val)))
|
||||
(do id1 val)]
|
||||
[(list (tc-result: (Value: val)) (tc-result: id-t (list (Var-True-Effect: id1)) (list (Var-False-Effect: id2))))
|
||||
(do id1 val)]
|
||||
[_ (values (list) (list))]))
|
||||
|
||||
|
||||
;; typecheck an application:
|
||||
;; arg-types: the types of the actual parameters
|
||||
;; arg-effs: the effects of the arguments
|
||||
;; dom-types: the types of the function's fixed arguments
|
||||
;; rest-type: the type of the functions's rest parameter, or #f
|
||||
;; latent-eff: the latent effect of the function
|
||||
;; arg-stxs: the syntax for each actual parameter, for error reporting
|
||||
;; [Type] [Type] Maybe[Type] [Syntax] -> (values Listof[Effect] Listof[Effect])
|
||||
(define (tc-args arg-types arg-thn-effs arg-els-effs dom-types rest-type latent-thn-eff latent-els-eff arg-stxs)
|
||||
(define (var-true-effect-v e) (match e
|
||||
[(Var-True-Effect: v) v]))
|
||||
(define (var-false-effect-v e) (match e
|
||||
[(Var-False-Effect: v) v]))
|
||||
;; special case for predicates:
|
||||
(if (and (not (null? latent-thn-eff))
|
||||
(not (null? latent-els-eff))
|
||||
(not rest-type)
|
||||
;(printf "got to =~n")
|
||||
(= (length arg-types) (length dom-types) 1)
|
||||
;(printf "got to var preds~n")
|
||||
(= (length (car arg-thn-effs)) (length (car arg-els-effs)) 1)
|
||||
(Var-True-Effect? (caar arg-thn-effs)) ;; thn-effs is a list for each arg
|
||||
(Var-False-Effect? (caar arg-els-effs)) ;; same with els-effs
|
||||
(free-identifier=? (var-true-effect-v (caar arg-thn-effs))
|
||||
(var-false-effect-v (caar arg-els-effs)))
|
||||
(subtype (car arg-types) (car dom-types)))
|
||||
;; then this was a predicate application, so we construct the appropriate type effect
|
||||
(values (map (add-var (var-true-effect-v (caar arg-thn-effs))) latent-thn-eff)
|
||||
(map (add-var (var-true-effect-v (caar arg-thn-effs))) latent-els-eff))
|
||||
;; otherwise, we just ignore the effects.
|
||||
(let loop ([args arg-types] [doms dom-types] [stxs arg-stxs] [arg-count 1])
|
||||
(cond
|
||||
[(and (null? args) (null? doms)) (values null null)] ;; here, we just return the empty effect
|
||||
[(null? args)
|
||||
(tc-error/delayed
|
||||
"Insufficient arguments to function application, expected ~a, got ~a"
|
||||
(length dom-types) (length arg-types))
|
||||
(values null null)]
|
||||
[(and (null? doms) rest-type)
|
||||
(if (subtype (car args) rest-type)
|
||||
(loop (cdr args) doms (cdr stxs) (add1 arg-count))
|
||||
(begin
|
||||
(tc-error/delayed #:stx (car stxs)
|
||||
"Rest argument had wrong type, expected: ~a and got: ~a"
|
||||
rest-type (car args))
|
||||
(values null null)))]
|
||||
[(null? doms)
|
||||
(tc-error/delayed "Too many arguments to function, expected ~a, got ~a" (length dom-types) (length arg-types))
|
||||
(values null null)]
|
||||
[(subtype (car args) (car doms))
|
||||
(loop (cdr args) (cdr doms) (cdr stxs) (add1 arg-count))]
|
||||
[else
|
||||
(tc-error/delayed
|
||||
#:stx (car stxs)
|
||||
"Wrong function argument type, expected ~a, got ~a for argument ~a"
|
||||
(car doms) (car args) arg-count)
|
||||
(loop (cdr args) (cdr doms) (cdr stxs) (add1 arg-count))]))))
|
||||
|
||||
|
||||
;(trace tc-args)
|
||||
|
||||
(define (stringify-domain dom rst drst [rng #f])
|
||||
(let ([doms-string (if (null? dom) "" (string-append (stringify dom) " "))]
|
||||
[rng-string (if rng (format " -> ~a" rng) "")])
|
||||
(cond [drst
|
||||
(format "~a~a ... ~a~a" doms-string (car drst) (cdr drst) rng-string)]
|
||||
[rst
|
||||
(format "~a~a *~a" doms-string rst rng-string)]
|
||||
[else (string-append (stringify dom) rng-string)])))
|
||||
|
||||
(define (domain-mismatches ty doms rests drests rngs arg-tys tail-ty tail-bound #:expected [expected #f])
|
||||
(define arguments-str
|
||||
(stringify-domain arg-tys (if (not tail-bound) tail-ty #f) (if tail-bound (cons tail-ty tail-bound) #f)))
|
||||
(cond
|
||||
[(null? doms)
|
||||
(int-err "How could doms be null: ~a ~a" ty)]
|
||||
[(= 1 (length doms))
|
||||
(format "Domain: ~a~nArguments: ~a~n~a"
|
||||
(stringify-domain (car doms) (car rests) (car drests))
|
||||
arguments-str
|
||||
(if expected
|
||||
(format "Result type: ~a~nExpected result: ~a~n"
|
||||
(car rngs) expected)
|
||||
""))]
|
||||
[else
|
||||
(format "~a: ~a~nArguments: ~a~n~a"
|
||||
(if expected "Types" "Domains")
|
||||
(stringify (if expected
|
||||
(map stringify-domain doms rests drests rngs)
|
||||
(map stringify-domain doms rests drests))
|
||||
"~n\t")
|
||||
arguments-str
|
||||
(if expected
|
||||
(format "Expected result: ~a~n" expected)
|
||||
""))]))
|
||||
|
||||
(define (do-apply-log subst fun arg)
|
||||
(match* (fun arg)
|
||||
[('star 'list) (printf/log "Polymorphic apply called with uniform rest arg, list argument\n")]
|
||||
[('star 'dots) (printf/log "Polymorphic apply called with uniform rest arg, dotted argument\n")]
|
||||
[('dots 'dots) (printf/log "Polymorphic apply called with non-uniform rest arg, dotted argument\n")])
|
||||
(log-result subst))
|
||||
|
||||
(define (tc/apply f args)
|
||||
(define f-ty (tc-expr f))
|
||||
;; produces the first n-1 elements of the list, and the last element
|
||||
(define (split l)
|
||||
(let loop ([l l] [acc '()])
|
||||
(if (null? (cdr l))
|
||||
(values (reverse acc) (car l))
|
||||
(loop (cdr l) (cons (car l) acc)))))
|
||||
(define-values (fixed-args tail) (split (syntax->list args)))
|
||||
|
||||
(match f-ty
|
||||
[(tc-result: (Function: (list (arr: doms rngs rests drests '() thn-effs els-effs) ...)))
|
||||
(when (null? doms)
|
||||
(tc-error/expr #:return (ret (Un))
|
||||
"empty case-lambda given as argument to apply"))
|
||||
(let ([arg-tys (map tc-expr/t fixed-args)])
|
||||
(let loop ([doms* doms] [rngs* rngs] [rests* rests] [drests* drests])
|
||||
(cond [(null? doms*)
|
||||
(let-values ([(tail-ty tail-bound)
|
||||
(with-handlers ([exn:fail? (lambda _ (values (tc-expr/t tail) #f))])
|
||||
(tc/dots tail))])
|
||||
(tc-error/expr #:return (ret (Un))
|
||||
(string-append
|
||||
"Bad arguments to function in apply:~n"
|
||||
(domain-mismatches f-ty doms rests drests rngs arg-tys tail-ty tail-bound))))]
|
||||
[(and (car rests*)
|
||||
(let-values ([(tail-ty tail-bound)
|
||||
(with-handlers ([exn:fail? (lambda _ (values #f #f))])
|
||||
(tc/dots tail))])
|
||||
(and tail-ty
|
||||
(subtype (apply -lst* arg-tys #:tail (make-Listof tail-ty))
|
||||
(apply -lst* (car doms*) #:tail (make-Listof (car rests*)))))))
|
||||
(printf/log "Non-poly apply, ... arg\n")
|
||||
(ret (car rngs*))]
|
||||
[(and (car rests*)
|
||||
(let ([tail-ty (with-handlers ([exn:fail? (lambda _ #f)])
|
||||
(tc-expr/t tail))])
|
||||
(and tail-ty
|
||||
(subtype (apply -lst* arg-tys #:tail tail-ty)
|
||||
(apply -lst* (car doms*) #:tail (make-Listof (car rests*)))))))
|
||||
|
||||
(printf/log (if (memq (syntax->datum f) '(+ - * / max min))
|
||||
"Simple arithmetic non-poly apply\n"
|
||||
"Simple non-poly apply\n"))
|
||||
(ret (car rngs*))]
|
||||
[(and (car drests*)
|
||||
(let-values ([(tail-ty tail-bound)
|
||||
(with-handlers ([exn:fail? (lambda _ (values #f #f))])
|
||||
(tc/dots tail))])
|
||||
(and tail-ty
|
||||
(eq? (cdr (car drests*)) tail-bound)
|
||||
(subtypes arg-tys (car doms*))
|
||||
(subtype tail-ty (car (car drests*))))))
|
||||
(printf/log "Non-poly apply, ... arg\n")
|
||||
(ret (car rngs*))]
|
||||
[else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))]
|
||||
[(tc-result: (Poly: vars (Function: (list (arr: doms rngs rests drests '() thn-effs els-effs) ..1))))
|
||||
(let*-values ([(arg-tys) (map tc-expr/t fixed-args)]
|
||||
[(tail-ty tail-bound) (with-handlers ([exn:fail:syntax? (lambda _ (values (tc-expr/t tail) #f))])
|
||||
(tc/dots tail))])
|
||||
#;(for-each (lambda (x) (unless (not (Poly? x))
|
||||
(tc-error "Polymorphic argument of type ~a to polymorphic function in apply not allowed" x)))
|
||||
(cons tail-ty arg-tys))
|
||||
(let loop ([doms* doms] [rngs* rngs] [rests* rests] [drests* drests])
|
||||
(cond [(null? doms*)
|
||||
(match f-ty
|
||||
[(tc-result: (Poly-names: _ (Function: (list (arr: doms rngs rests drests '() _ _) ..1))))
|
||||
(tc-error/expr #:return (ret (Un))
|
||||
(string-append
|
||||
"Bad arguments to polymorphic function in apply:~n"
|
||||
(domain-mismatches f-ty doms rests drests rngs arg-tys tail-ty tail-bound)))])]
|
||||
;; the actual work, when we have a * function and a list final argument
|
||||
[(and (car rests*)
|
||||
(not tail-bound)
|
||||
(<= (length (car doms*))
|
||||
(length arg-tys))
|
||||
(infer/vararg vars
|
||||
(cons tail-ty arg-tys)
|
||||
(cons (make-Listof (car rests*))
|
||||
(car doms*))
|
||||
(car rests*)
|
||||
(car rngs*)
|
||||
(fv (car rngs*))))
|
||||
=> (lambda (substitution) (ret (subst-all substitution (car rngs*))))]
|
||||
;; actual work, when we have a * function and ... final arg
|
||||
[(and (car rests*)
|
||||
tail-bound
|
||||
(<= (length (car doms*))
|
||||
(length arg-tys))
|
||||
(infer/vararg vars
|
||||
(cons (make-Listof tail-ty) arg-tys)
|
||||
(cons (make-Listof (car rests*))
|
||||
(car doms*))
|
||||
(car rests*)
|
||||
(car rngs*)
|
||||
(fv (car rngs*))))
|
||||
=> (lambda (substitution) (ret (subst-all substitution (car rngs*))))]
|
||||
;; ... function, ... arg
|
||||
[(and (car drests*)
|
||||
tail-bound
|
||||
(eq? tail-bound (cdr (car drests*)))
|
||||
(= (length (car doms*))
|
||||
(length arg-tys))
|
||||
(infer vars (cons tail-ty arg-tys) (cons (car (car drests*)) (car doms*)) (car rngs*) (fv (car rngs*))))
|
||||
=> (lambda (substitution) (ret (subst-all substitution (car rngs*))))]
|
||||
;; if nothing matches, around the loop again
|
||||
[else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))]
|
||||
[(tc-result: (Poly: vars (Function: '())))
|
||||
(tc-error/expr #:return (ret (Un))
|
||||
"Function has no cases")]
|
||||
[(tc-result: (PolyDots: (and vars (list fixed-vars ... dotted-var))
|
||||
(Function: (list (arr: doms rngs rests drests '() thn-effs els-effs) ..1))))
|
||||
(let*-values ([(arg-tys) (map tc-expr/t fixed-args)]
|
||||
[(tail-ty tail-bound) (with-handlers ([exn:fail:syntax? (lambda _ (values (tc-expr/t tail) #f))])
|
||||
(tc/dots tail))])
|
||||
(let loop ([doms* doms] [rngs* rngs] [rests* rests] [drests* drests])
|
||||
(cond [(null? doms*)
|
||||
(match f-ty
|
||||
[(tc-result: (PolyDots-names: _ (Function: (list (arr: doms rngs rests drests '() _ _) ..1))))
|
||||
(tc-error/expr #:return (ret (Un))
|
||||
(string-append
|
||||
"Bad arguments to polymorphic function in apply:~n"
|
||||
(domain-mismatches f-ty doms rests drests rngs arg-tys tail-ty tail-bound)))])]
|
||||
;; the actual work, when we have a * function and a list final argument
|
||||
[(and (car rests*)
|
||||
(not tail-bound)
|
||||
(<= (length (car doms*))
|
||||
(length arg-tys))
|
||||
(infer/vararg vars
|
||||
(cons tail-ty arg-tys)
|
||||
(cons (make-Listof (car rests*))
|
||||
(car doms*))
|
||||
(car rests*)
|
||||
(car rngs*)
|
||||
(fv (car rngs*))))
|
||||
=> (lambda (substitution)
|
||||
(do-apply-log substitution 'star 'list)
|
||||
(ret (subst-all substitution (car rngs*))))]
|
||||
;; actual work, when we have a * function and ... final arg
|
||||
[(and (car rests*)
|
||||
tail-bound
|
||||
(<= (length (car doms*))
|
||||
(length arg-tys))
|
||||
(infer/vararg vars
|
||||
(cons (make-Listof tail-ty) arg-tys)
|
||||
(cons (make-Listof (car rests*))
|
||||
(car doms*))
|
||||
(car rests*)
|
||||
(car rngs*)
|
||||
(fv (car rngs*))))
|
||||
=> (lambda (substitution)
|
||||
(do-apply-log substitution 'star 'dots)
|
||||
(ret (subst-all substitution (car rngs*))))]
|
||||
;; ... function, ... arg, same bound on ...
|
||||
[(and (car drests*)
|
||||
tail-bound
|
||||
(eq? tail-bound (cdr (car drests*)))
|
||||
(= (length (car doms*))
|
||||
(length arg-tys))
|
||||
(infer vars (cons tail-ty arg-tys) (cons (car (car drests*)) (car doms*)) (car rngs*) (fv (car rngs*))))
|
||||
=> (lambda (substitution)
|
||||
(do-apply-log substitution 'dots 'dots)
|
||||
(ret (subst-all substitution (car rngs*))))]
|
||||
;; ... function, ... arg, different bound on ...
|
||||
[(and (car drests*)
|
||||
tail-bound
|
||||
(not (eq? tail-bound (cdr (car drests*))))
|
||||
(= (length (car doms*))
|
||||
(length arg-tys))
|
||||
(parameterize ([current-tvars (extend-env (list tail-bound (cdr (car drests*)))
|
||||
(list (make-DottedBoth (make-F tail-bound))
|
||||
(make-DottedBoth (make-F (cdr (car drests*)))))
|
||||
(current-tvars))])
|
||||
(infer vars (cons tail-ty arg-tys) (cons (car (car drests*)) (car doms*)) (car rngs*) (fv (car rngs*)))))
|
||||
=> (lambda (substitution)
|
||||
(define drest-bound (cdr (car drests*)))
|
||||
(do-apply-log substitution 'dots 'dots)
|
||||
(ret (substitute-dotted (cadr (assq drest-bound substitution))
|
||||
tail-bound
|
||||
drest-bound
|
||||
(subst-all (alist-delete drest-bound substitution eq?)
|
||||
(car rngs*)))))]
|
||||
;; ... function, (List A B C etc) arg
|
||||
[(and (car drests*)
|
||||
(not tail-bound)
|
||||
(eq? (cdr (car drests*)) dotted-var)
|
||||
(= (length (car doms*))
|
||||
(length arg-tys))
|
||||
(untuple tail-ty)
|
||||
(infer/dots fixed-vars dotted-var (append arg-tys (untuple tail-ty)) (car doms*)
|
||||
(car (car drests*)) (car rngs*) (fv (car rngs*))))
|
||||
=> (lambda (substitution)
|
||||
(define drest-bound (cdr (car drests*)))
|
||||
(do-apply-log substitution 'dots 'dots)
|
||||
(ret (subst-all substitution (car rngs*))))]
|
||||
;; if nothing matches, around the loop again
|
||||
[else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))]
|
||||
[(tc-result: (PolyDots: vars (Function: '())))
|
||||
(tc-error/expr #:return (ret (Un))
|
||||
"Function has no cases")]
|
||||
[(tc-result: f-ty) (tc-error/expr #:return (ret (Un))
|
||||
"Type of argument to apply is not a function type: ~n~a" f-ty)]))
|
||||
|
||||
|
||||
|
||||
(define (log-result subst)
|
||||
(define (dmap-length d)
|
||||
(match d
|
||||
[(struct dcon (fixed rest)) (length fixed)]
|
||||
[(struct dcon-exact (fixed rest)) (length fixed)]))
|
||||
(define (dmap-rest? d)
|
||||
(match d
|
||||
[(struct dcon (fixed rest)) rest]
|
||||
[(struct dcon-exact (fixed rest)) rest]))
|
||||
(if (list? subst)
|
||||
(for ([s subst])
|
||||
(match s
|
||||
[(list v (list imgs ...) starred)
|
||||
(printf/log "Instantiated ... variable ~a with ~a types\n" v (length imgs))]
|
||||
[_ (void)]))
|
||||
(for* ([(cmap dmap) (in-pairs (cset-maps subst))]
|
||||
[(k v) (dmap-map dmap)])
|
||||
(printf/log "Instantiated ... variable ~a with ~a types~a\n" k (dmap-length v)
|
||||
(if (dmap-rest? v)
|
||||
" and a starred type"
|
||||
"")))))
|
||||
|
||||
(define-syntax (handle-clauses stx)
|
||||
(syntax-parse stx
|
||||
[(_ (lsts ... rngs) f-stx pred infer t argtypes expected)
|
||||
(with-syntax ([(vars ... rng) (generate-temporaries #'(lsts ... rngs))])
|
||||
(syntax/loc stx
|
||||
(or (for/or ([vars lsts] ... [rng rngs]
|
||||
#:when (pred vars ... rng))
|
||||
(let ([substitution (infer vars ... rng)])
|
||||
(and substitution
|
||||
(log-result substitution)
|
||||
(ret (or expected
|
||||
(subst-all substitution rng))))))
|
||||
(poly-fail t argtypes #:name (and (identifier? f-stx) f-stx) #:expected expected))))]))
|
||||
|
||||
(define (poly-fail t argtypes #:name [name #f] #:expected [expected #f])
|
||||
(match t
|
||||
[(or (Poly-names: msg-vars (Function: (list (arr: msg-doms msg-rngs msg-rests msg-drests '() _ _) ...)))
|
||||
(PolyDots-names: msg-vars (Function: (list (arr: msg-doms msg-rngs msg-rests msg-drests '() _ _) ...))))
|
||||
(let ([fcn-string (if name
|
||||
(format "function ~a" (syntax->datum name))
|
||||
"function")])
|
||||
(if (and (andmap null? msg-doms)
|
||||
(null? argtypes))
|
||||
(tc-error/expr #:return (ret (Un))
|
||||
(string-append
|
||||
"Could not infer types for applying polymorphic "
|
||||
fcn-string
|
||||
"\n"))
|
||||
(tc-error/expr #:return (ret (Un))
|
||||
(string-append
|
||||
"Polymorphic " fcn-string " could not be applied to arguments:~n"
|
||||
(domain-mismatches t msg-doms msg-rests msg-drests msg-rngs argtypes #f #f #:expected expected)
|
||||
(if (not (for/and ([t (apply append (map fv/list msg-doms))]) (memq t msg-vars)))
|
||||
(string-append "Type Variables: " (stringify msg-vars) "\n")
|
||||
"")))))]))
|
||||
|
||||
|
||||
(define (tc/funapp f-stx args-stx ftype0 argtys expected)
|
||||
(match-let* ([(list (tc-result: argtypes arg-thn-effs arg-els-effs) ...) argtys])
|
||||
(let outer-loop ([ftype ftype0]
|
||||
[argtypes argtypes]
|
||||
[arg-thn-effs arg-thn-effs]
|
||||
[arg-els-effs arg-els-effs]
|
||||
[args args-stx])
|
||||
(match ftype
|
||||
;; procedural structs
|
||||
[(tc-result: (and sty (Struct: _ _ _ (? Type? proc-ty) _ _ _)) thn-eff els-eff)
|
||||
(outer-loop (ret proc-ty thn-eff els-eff)
|
||||
(cons (tc-result-t ftype0) argtypes)
|
||||
(cons (list) arg-thn-effs)
|
||||
(cons (list) arg-els-effs)
|
||||
#`(#,(syntax/loc f-stx dummy) #,@args))]
|
||||
;; mu types, etc
|
||||
[(tc-result: (? needs-resolving? t) thn-eff els-eff)
|
||||
(outer-loop (ret (resolve-once t) thn-eff els-eff) argtypes arg-thn-effs arg-els-effs args)]
|
||||
;; parameters
|
||||
[(tc-result: (Param: in out))
|
||||
(match argtypes
|
||||
[(list) (ret out)]
|
||||
[(list t)
|
||||
(if (subtype t in)
|
||||
(ret -Void)
|
||||
(tc-error/expr #:return (ret (Un))
|
||||
"Wrong argument to parameter - expected ~a and got ~a" in t))]
|
||||
[_ (tc-error/expr #:return (ret (Un))
|
||||
"Wrong number of arguments to parameter - expected 0 or 1, got ~a"
|
||||
(length argtypes))])]
|
||||
;; single clause functions
|
||||
;; FIXME - error on non-optional keywords
|
||||
[(tc-result: (and t (Function: (list (arr: dom rng rest #f _ latent-thn-effs latent-els-effs))))
|
||||
thn-eff els-eff)
|
||||
(let-values ([(thn-eff els-eff)
|
||||
(tc-args argtypes arg-thn-effs arg-els-effs dom rest
|
||||
latent-thn-effs latent-els-effs
|
||||
(syntax->list args))])
|
||||
(ret rng thn-eff els-eff))]
|
||||
;; non-polymorphic case-lambda functions
|
||||
[(tc-result: (and t (Function: (list (arr: doms rngs rests (and drests #f) '() latent-thn-effs latent-els-effs) ..1)))
|
||||
thn-eff els-eff)
|
||||
(let loop ([doms* doms] [rngs rngs] [rests* rests])
|
||||
(cond [(null? doms*)
|
||||
(tc-error/expr
|
||||
#:return (ret (Un))
|
||||
(string-append "No function domains matched in function application:\n"
|
||||
(domain-mismatches t doms rests drests rngs argtypes #f #f)))]
|
||||
[(subtypes/varargs argtypes (car doms*) (car rests*))
|
||||
(when (car rests*)
|
||||
(printf/log "Simple varargs function application (~a)\n" (syntax->datum f-stx)))
|
||||
(ret (car rngs))]
|
||||
[else (loop (cdr doms*) (cdr rngs) (cdr rests*))]))]
|
||||
;; simple polymorphic functions, no rest arguments
|
||||
[(tc-result: (and t
|
||||
(or (Poly: vars
|
||||
(Function: (list (arr: doms rngs (and rests #f) (and drests #f) '() thn-effs els-effs) ...)))
|
||||
(PolyDots: (list vars ...)
|
||||
(Function: (list (arr: doms rngs (and rests #f) (and drests #f) '() thn-effs els-effs) ...))))))
|
||||
(handle-clauses (doms rngs) f-stx
|
||||
(lambda (dom _) (= (length dom) (length argtypes)))
|
||||
(lambda (dom rng) (infer vars argtypes dom rng (fv rng) expected))
|
||||
t argtypes expected)]
|
||||
;; polymorphic varargs
|
||||
[(tc-result: (and t
|
||||
(or (Poly: vars (Function: (list (arr: doms rngs rests (and drests #f) '() thn-effs els-effs) ...)))
|
||||
;; we want to infer the dotted-var here as well, and we don't use these separately
|
||||
;; so we can just use "vars" instead of (list fixed-vars ... dotted-var)
|
||||
(PolyDots: vars (Function: (list (arr: doms rngs rests (and drests #f) '() thn-effs els-effs) ...))))))
|
||||
(printf/log "Polymorphic varargs function application (~a)\n" (syntax->datum f-stx))
|
||||
(handle-clauses (doms rests rngs) f-stx
|
||||
(lambda (dom rest rng) (<= (length dom) (length argtypes)))
|
||||
(lambda (dom rest rng) (infer/vararg vars argtypes dom rest rng (fv rng) expected))
|
||||
t argtypes expected)]
|
||||
;; polymorphic ... type
|
||||
[(tc-result: (and t (PolyDots:
|
||||
(and vars (list fixed-vars ... dotted-var))
|
||||
(Function: (list (arr: doms rngs (and #f rests) (cons dtys dbounds) '() thn-effs els-effs) ...)))))
|
||||
(printf/log "Polymorphic ... function application (~a)\n" (syntax->datum f-stx))
|
||||
(handle-clauses (doms dtys dbounds rngs) f-stx
|
||||
(lambda (dom dty dbound rng) (and (<= (length dom) (length argtypes))
|
||||
(eq? dotted-var dbound)))
|
||||
(lambda (dom dty dbound rng)
|
||||
(infer/dots fixed-vars dotted-var argtypes dom dty rng (fv rng) #:expected expected))
|
||||
t argtypes expected)]
|
||||
;; Union of function types works if we can apply all of them
|
||||
[(tc-result: (Union: (list (and fs (Function: _)) ...)) e1 e2)
|
||||
(match-let ([(list (tc-result: ts) ...) (map (lambda (f) (outer-loop
|
||||
(ret f e1 e2) argtypes arg-thn-effs arg-els-effs args)) fs)])
|
||||
(ret (apply Un ts)))]
|
||||
;; error type is a perfectly good fcn type
|
||||
[(tc-result: (Error:)) (ret (make-Error))]
|
||||
[(tc-result: f-ty _ _) (tc-error/expr #:return (ret (Un))
|
||||
"Cannot apply expression of type ~a, since it is not a function type" f-ty)]))))
|
||||
|
||||
;(trace tc/funapp)
|
||||
|
||||
|
||||
|
||||
(define (tc/app form) (tc/app/internal form #f))
|
||||
|
||||
(define (tc/app/check form expected)
|
||||
(define t (tc/app/internal form expected))
|
||||
(check-below t expected)
|
||||
(ret expected))
|
||||
|
||||
(define-syntax-class lv-clause
|
||||
#:transparent
|
||||
(pattern [(v:id ...) e:expr]))
|
||||
|
||||
(define-syntax-class lv-clauses
|
||||
#:transparent
|
||||
(pattern (cl:lv-clause ...)
|
||||
#:with (e ...) #'(cl.e ...)
|
||||
#:with (vs ...) #'((cl.v ...) ...)))
|
||||
|
||||
(define-syntax-class core-expr
|
||||
#:literals (reverse letrec-syntaxes+values let-values #%plain-app
|
||||
if letrec-values begin #%plain-lambda set! case-lambda
|
||||
begin0 with-continuation-mark)
|
||||
#:transparent
|
||||
(pattern (let-values cls:lv-clauses body)
|
||||
#:with (expr ...) #'(cls.e ... body))
|
||||
(pattern (letrec-values cls:lv-clauses body)
|
||||
#:with (expr ...) #'(cls.e ... body))
|
||||
(pattern (letrec-syntaxes+values _ cls:lv-clauses body)
|
||||
#:with (expr ...) #'(cls.e ... body))
|
||||
(pattern (#%plain-app expr ...))
|
||||
(pattern (if expr ...))
|
||||
(pattern (with-continuation-mark expr ...))
|
||||
(pattern (begin expr ...))
|
||||
(pattern (begin0 expr ...))
|
||||
(pattern (#%plain-lambda _ e)
|
||||
#:with (expr ...) #'(e))
|
||||
(pattern (case-lambda [_ expr] ...))
|
||||
(pattern (set! _ e)
|
||||
#:with (expr ...) #'(e))
|
||||
(pattern _
|
||||
#:with (expr ...) #'()))
|
||||
|
||||
;; expr id -> type or #f
|
||||
;; if there is a binding in stx of the form:
|
||||
;; (let ([x (reverse name)]) e)
|
||||
;; where x has a type annotation, return that annotation, otherwise #f
|
||||
(define (find-annotation stx name)
|
||||
(define (find s) (find-annotation s name))
|
||||
(define (match? b)
|
||||
(syntax-parse b
|
||||
#:literals (#%plain-app reverse)
|
||||
[c:lv-clause
|
||||
#:with (#%plain-app reverse n:id) #'c.e
|
||||
#:with (v) #'(c.v ...)
|
||||
#:when (free-identifier=? name #'n)
|
||||
(type-annotation #'v)]
|
||||
[_ #f]))
|
||||
(syntax-parse stx
|
||||
#:literals (let-values)
|
||||
[(let-values cls:lv-clauses body)
|
||||
(or (ormap match? (syntax->list #'cls))
|
||||
(find #'body))]
|
||||
[e:core-expr
|
||||
(ormap find (syntax->list #'(e.expr ...)))]))
|
||||
|
||||
|
||||
(define (check-do-make-object cl pos-args names named-args)
|
||||
(let* ([names (map syntax-e (syntax->list names))]
|
||||
[name-assoc (map list names (syntax->list named-args))])
|
||||
(let loop ([t (tc-expr cl)])
|
||||
(match t
|
||||
[(tc-result: (? Mu? t)) (loop (ret (unfold t)))]
|
||||
[(tc-result: (and c (Class: pos-tys (list (and tnflds (list tnames _ _)) ...) _)))
|
||||
(unless (= (length pos-tys)
|
||||
(length (syntax->list pos-args)))
|
||||
(tc-error/delayed "expected ~a positional arguments, but got ~a"
|
||||
(length pos-tys) (length (syntax->list pos-args))))
|
||||
;; use for, since they might be different lengths in error case
|
||||
(for ([pa (in-syntax pos-args)]
|
||||
[pt (in-list pos-tys)])
|
||||
(tc-expr/check pa pt))
|
||||
(for ([n names]
|
||||
#:when (not (memq n tnames)))
|
||||
(tc-error/delayed
|
||||
"unknown named argument ~a for class~nlegal named arguments are ~a"
|
||||
n (stringify tnames)))
|
||||
(for-each (match-lambda
|
||||
[(list tname tfty opt?)
|
||||
(let ([s (cond [(assq tname name-assoc) => cadr]
|
||||
[(not opt?)
|
||||
(tc-error/delayed "value not provided for named init arg ~a" tname)
|
||||
#f]
|
||||
[else #f])])
|
||||
(if s
|
||||
;; this argument was present
|
||||
(tc-expr/check s tfty)
|
||||
;; this argument wasn't provided, and was optional
|
||||
#f))])
|
||||
tnflds)
|
||||
(ret (make-Instance c))]
|
||||
[(tc-result: t)
|
||||
(tc-error/expr #:return (ret (Un)) "expected a class value for object creation, got: ~a" t)]))))
|
||||
|
||||
(define (tc-keywords form arities kws kw-args pos-args expected)
|
||||
(match arities
|
||||
[(list (arr: dom rng rest #f ktys _ _))
|
||||
;; assumes that everything is in sorted order
|
||||
(let loop ([actual-kws kws]
|
||||
[actuals (map tc-expr/t (syntax->list kw-args))]
|
||||
[formals ktys])
|
||||
(match* (actual-kws formals)
|
||||
[('() '())
|
||||
(void)]
|
||||
[(_ '())
|
||||
(tc-error/expr #:return (ret (Un))
|
||||
"Unexpected keyword argument ~a" (car actual-kws))]
|
||||
[('() (cons fst rst))
|
||||
(match fst
|
||||
[(Keyword: k _ #t)
|
||||
(tc-error/expr #:return (ret (Un))
|
||||
"Missing keyword argument ~a" k)]
|
||||
[_ (loop actual-kws actuals rst)])]
|
||||
[((cons k kws-rest) (cons (Keyword: k* t req?) form-rest))
|
||||
(cond [(eq? k k*) ;; we have a match
|
||||
(unless (subtype (car actuals) t)
|
||||
(tc-error/delayed
|
||||
"Wrong function argument type, expected ~a, got ~a for keyword argument ~a"
|
||||
t (car actuals) k))
|
||||
(loop kws-rest (cdr actuals) form-rest)]
|
||||
[req? ;; this keyword argument was required
|
||||
(tc-error/delayed "Missing keyword argument ~a" k*)
|
||||
(loop kws-rest (cdr actuals) form-rest)]
|
||||
[else ;; otherwise, ignore this formal param, and continue
|
||||
(loop actual-kws actuals form-rest)])]))
|
||||
(tc/funapp (car (syntax-e form)) kw-args (ret (make-Function arities)) (map tc-expr (syntax->list pos-args)) expected)]
|
||||
[_ (int-err "case-lambda w/ keywords not supported")]))
|
||||
|
||||
|
||||
(define (type->list t)
|
||||
(match t
|
||||
[(Pair: (Value: (? keyword? k)) b) (cons k (type->list b))]
|
||||
[(Value: '()) null]
|
||||
[_ (int-err "bad value in type->list: ~a" t)]))
|
||||
|
||||
;; id: identifier
|
||||
;; sym: a symbol
|
||||
;; mod: a quoted require spec like 'scheme/base
|
||||
;; is id the name sym defined in mod?
|
||||
(define (id-from? id sym mod)
|
||||
(and (eq? (syntax-e id) sym)
|
||||
(eq? (module-path-index-resolve (syntax-source-module id))
|
||||
((current-module-name-resolver) mod #f #f #f))))
|
||||
|
||||
(define (tc/app/internal form expected)
|
||||
(kernel-syntax-case* form #f
|
||||
(values apply k:apply not list list* call-with-values do-make-object make-object cons
|
||||
andmap ormap) ;; the special-cased functions
|
||||
;; special case for delay
|
||||
[(#%plain-app
|
||||
mp1
|
||||
(#%plain-lambda ()
|
||||
(#%plain-app mp2 (#%plain-app call-with-values (#%plain-lambda () e) list))))
|
||||
(and (id-from? #'mp1 'make-promise 'scheme/promise)
|
||||
(id-from? #'mp2 'make-promise 'scheme/promise))
|
||||
(ret (-Promise (tc-expr/t #'e)))]
|
||||
;; special cases for classes
|
||||
[(#%plain-app make-object cl . args)
|
||||
(check-do-make-object #'cl #'args #'() #'())]
|
||||
[(#%plain-app do-make-object cl (#%plain-app list . pos-args) (#%plain-app list (#%plain-app cons 'names named-args) ...))
|
||||
(check-do-make-object #'cl #'pos-args #'(names ...) #'(named-args ...))]
|
||||
[(#%plain-app do-make-object . args)
|
||||
(int-err "bad do-make-object : ~a" (syntax->datum #'args))]
|
||||
;; call-with-values
|
||||
[(#%plain-app call-with-values prod con)
|
||||
(match-let* ([(tc-result: prod-t) (tc-expr #'prod)])
|
||||
(define (values-ty->list t)
|
||||
(match t
|
||||
[(Values: ts) ts]
|
||||
[_ (list t)]))
|
||||
(match prod-t
|
||||
[(Function: (list (arr: (list) vals _ #f '() _ _)))
|
||||
(tc/funapp #'con #'prod (tc-expr #'con) (map ret (values-ty->list vals)) expected)]
|
||||
[_ (tc-error/expr #:return (ret (Un))
|
||||
"First argument to call with values must be a function that can accept no arguments, got: ~a"
|
||||
prod-t)]))]
|
||||
;; special cases for `values'
|
||||
;; special case the single-argument version to preserve the effects
|
||||
[(#%plain-app values arg) (tc-expr #'arg)]
|
||||
[(#%plain-app values . args)
|
||||
(let ([tys (map tc-expr/t (syntax->list #'args))])
|
||||
(ret (-values tys)))]
|
||||
;; special case for `list'
|
||||
[(#%plain-app list . args)
|
||||
(let ([tys (map tc-expr/t (syntax->list #'args))])
|
||||
(ret (apply -lst* tys)))]
|
||||
;; special case for `list*'
|
||||
[(#%plain-app list* . args)
|
||||
(match-let* ([(list last tys-r ...) (reverse (map tc-expr/t (syntax->list #'args)))]
|
||||
[tys (reverse tys-r)])
|
||||
(ret (foldr make-Pair last tys)))]
|
||||
;; in eq? cases, call tc/eq
|
||||
[(#%plain-app eq? v1 v2)
|
||||
(and (identifier? #'eq?) (comparator? #'eq?))
|
||||
(begin
|
||||
;; make sure the whole expression is type correct
|
||||
(tc/funapp #'eq? #'(v1 v2) (tc-expr #'eq?) (map tc-expr (syntax->list #'(v1 v2))) expected)
|
||||
;; check thn and els with the eq? info
|
||||
(let-values ([(thn-eff els-eff) (tc/eq #'eq? #'v1 #'v2)])
|
||||
(ret B thn-eff els-eff)))]
|
||||
;; special case for `not'
|
||||
[(#%plain-app not arg)
|
||||
(match (tc-expr #'arg)
|
||||
;; if arg was a predicate application, we swap the effects
|
||||
[(tc-result: t thn-eff els-eff)
|
||||
(ret B (map var->type-eff els-eff) (map var->type-eff thn-eff))])]
|
||||
[(#%plain-app k:apply . args)
|
||||
(tc/app/internal #'(#%plain-app apply . args) expected)]
|
||||
;; special-er case for (apply values (list x y z))
|
||||
[(#%plain-app apply values e)
|
||||
(cond [(with-handlers ([exn:fail? (lambda _ #f)])
|
||||
(untuple (tc-expr/t #'e)))
|
||||
=> (lambda (t) (ret (-values t)))]
|
||||
[else (tc/apply #'values #'(e))])]
|
||||
;; special case for `apply'
|
||||
[(#%plain-app apply f . args) (tc/apply #'f #'args)]
|
||||
;; special case for keywords
|
||||
[(#%plain-app
|
||||
(#%plain-app kpe kws num fn)
|
||||
kw-list
|
||||
(#%plain-app list . kw-arg-list)
|
||||
. pos-args)
|
||||
(eq? (syntax-e #'kpe) 'keyword-procedure-extract)
|
||||
(match (tc-expr #'fn)
|
||||
[(tc-result: (Function: arities))
|
||||
(tc-keywords form arities (type->list (tc-expr/t #'kws)) #'kw-arg-list #'pos-args expected)]
|
||||
[(tc-result: t) (tc-error/expr #:return (ret (Un))
|
||||
"Cannot apply expression of type ~a, since it is not a function type" t)])]
|
||||
;; even more special case for match
|
||||
[(#%plain-app (letrec-values ([(lp) (#%plain-lambda args . body)]) lp*) . actuals)
|
||||
(and expected (not (andmap type-annotation (syntax->list #'args))) (free-identifier=? #'lp #'lp*))
|
||||
(let-loop-check form #'lp #'actuals #'args #'body expected)]
|
||||
;; or/andmap of ... argument
|
||||
[(#%plain-app or/andmap f arg)
|
||||
(and
|
||||
(identifier? #'or/andmap)
|
||||
(or (free-identifier=? #'or/andmap #'ormap)
|
||||
(free-identifier=? #'or/andmap #'andmap))
|
||||
(with-handlers ([exn:fail? (lambda _ #f)])
|
||||
(tc/dots #'arg)
|
||||
#t))
|
||||
(let-values ([(ty bound) (tc/dots #'arg)])
|
||||
(parameterize ([current-tvars (extend-env (list bound)
|
||||
(list (make-DottedBoth (make-F bound)))
|
||||
(current-tvars))])
|
||||
(match-let* ([ft (tc-expr #'f)]
|
||||
[(tc-result: t) (tc/funapp #'f #'(arg) ft (list (ret ty)) #f)])
|
||||
(ret (Un (-val #f) t)))))]
|
||||
;; infer for ((lambda
|
||||
[(#%plain-app (#%plain-lambda (x ...) . body) args ...)
|
||||
(= (length (syntax->list #'(x ...)))
|
||||
(length (syntax->list #'(args ...))))
|
||||
(tc/let-values/check #'((x) ...) #'(args ...) #'body
|
||||
#'(let-values ([(x) args] ...) . body)
|
||||
expected)]
|
||||
;; default case
|
||||
[(#%plain-app f args ...)
|
||||
(tc/funapp #'f #'(args ...) (tc-expr #'f) (map tc-expr (syntax->list #'(args ...))) expected)]))
|
||||
|
||||
(define (let-loop-check form lp actuals args body expected)
|
||||
(kernel-syntax-case* #`(#,args #,body #,actuals) #f (null?)
|
||||
[((val acc ...)
|
||||
((if (#%plain-app null? val*) thn els))
|
||||
(actual actuals ...))
|
||||
(and (free-identifier=? #'val #'val*)
|
||||
(ormap (lambda (a) (find-annotation #'(if (#%plain-app null? val*) thn els) a))
|
||||
(syntax->list #'(acc ...))))
|
||||
(let* ([ts1 (generalize (tc-expr/t #'actual))]
|
||||
[ann-ts (for/list ([a (in-syntax #'(acc ...))]
|
||||
[ac (in-syntax #'(actuals ...))])
|
||||
(or (find-annotation #'(if (#%plain-app null? val*) thn els) a)
|
||||
(generalize (tc-expr/t ac))))]
|
||||
[ts (cons ts1 ann-ts)])
|
||||
;; check that the actual arguments are ok here
|
||||
(map tc-expr/check (syntax->list #'(actuals ...)) ann-ts)
|
||||
;; then check that the function typechecks with the inferred types
|
||||
(tc/rec-lambda/check form args body lp ts expected)
|
||||
(ret expected))]
|
||||
;; special case when argument needs inference
|
||||
[_
|
||||
(let ([ts (for/list ([ac (syntax->list actuals)]
|
||||
[f (syntax->list args)])
|
||||
(or
|
||||
(type-annotation f #:infer #t)
|
||||
(generalize (tc-expr/t ac))))])
|
||||
(tc/rec-lambda/check form args body lp ts expected)
|
||||
(ret expected))]))
|
||||
|
||||
(define (matches? stx)
|
||||
(let loop ([stx stx] [ress null] [acc*s null])
|
||||
(syntax-case stx (#%plain-app reverse)
|
||||
[([(res) (#%plain-app reverse acc*)] . more)
|
||||
(loop #'more (cons #'res ress) (cons #'acc* acc*s))]
|
||||
[rest
|
||||
(syntax->list #'rest)
|
||||
(begin
|
||||
;(printf "ress: ~a~n" (map syntax-e ress))
|
||||
(list (reverse ress) (reverse acc*s) #'rest))]
|
||||
[_ #f])))
|
||||
|
||||
;(trace tc/app/internal)
|
||||
|
|
@ -1,192 +0,0 @@
|
|||
#lang scheme/unit
|
||||
|
||||
(require (rename-in "../utils/utils.ss" [infer r:infer]))
|
||||
(require "signatures.ss"
|
||||
(rep type-rep filter-rep object-rep)
|
||||
(rename-in (types convenience subtype union utils comparison remove-intersect)
|
||||
[remove *remove])
|
||||
(env lexical-env)
|
||||
(r:infer infer)
|
||||
(utils tc-utils mutated-vars)
|
||||
syntax/kerncase
|
||||
mzlib/trace
|
||||
mzlib/plt-match)
|
||||
|
||||
;; if typechecking
|
||||
(import tc-expr^)
|
||||
(export tc-if^)
|
||||
|
||||
|
||||
|
||||
;; combinators for typechecking in the context of effects
|
||||
;; t/f tells us whether this is the true or the false branch of an if
|
||||
;; neccessary for handling true/false effects
|
||||
;; Boolean Expr listof[Effect] option[type] -> TC-Result
|
||||
(define (tc-expr/eff t/f expr effs expected)
|
||||
;; this flag represents whether the refinement proves that this expression cannot be executed
|
||||
(let ([flag (box #f)])
|
||||
;; this does the operation on the old type
|
||||
;; type-op : (Type Type -> Type) Type -> _ Type -> Type
|
||||
(define ((type-op f t) _ old)
|
||||
(let ([new-t (f old t)])
|
||||
;; if this operation produces an uninhabitable type, then this expression can't be executed
|
||||
(when (type-equal? new-t (Un))
|
||||
(set-box! flag #t))
|
||||
;; have to return something here, so that we can continue typechecking
|
||||
new-t))
|
||||
;; loop : listof[effect] -> tc-result
|
||||
(let loop ([effs effs])
|
||||
;; convenience macro for checking the rest of the list
|
||||
(define-syntax check-rest
|
||||
(syntax-rules ()
|
||||
[(check-rest f v)
|
||||
(with-update-type/lexical f v (loop (cdr effs)))]
|
||||
[(check-rest f t v)
|
||||
(check-rest (type-op f t) v)]))
|
||||
(if (null? effs)
|
||||
;; base case
|
||||
(let* ([reachable? (not (unbox flag))])
|
||||
(unless reachable?
|
||||
(warn-unreachable expr))
|
||||
(cond
|
||||
;; if flag is true, then we don't want to verify that this branch has the appropriate type
|
||||
;; in particular, it might be (void)
|
||||
[(and expected reachable?)
|
||||
(tc-expr/check expr expected)]
|
||||
;; this code is reachable, but we have no expected type
|
||||
[reachable?
|
||||
(tc-expr expr)]
|
||||
;; otherwise, this code is unreachable
|
||||
;; and the resulting type should be the empty type
|
||||
[(check-unreachable-code?)
|
||||
(tc-expr/check expr Univ)
|
||||
(ret (Un))]
|
||||
[else
|
||||
(ret (Un))]))
|
||||
;; recursive case
|
||||
(match (car effs)
|
||||
;; these effects have no consequence for the typechecking
|
||||
[(True-Effect:)
|
||||
(or t/f (set-box! flag #t))
|
||||
(loop (cdr effs))]
|
||||
[(False-Effect:)
|
||||
(and t/f (set-box! flag #t))
|
||||
(loop (cdr effs))]
|
||||
;; restrict v to have a type that's a subtype of t
|
||||
[(Restrict-Effect: t v)
|
||||
(check-rest restrict t v)]
|
||||
;; remove t from the type of v
|
||||
[(Remove-Effect: t v) (check-rest *remove t v)]
|
||||
;; just replace the type of v with (-val #f)
|
||||
[(Var-False-Effect: v) (check-rest (lambda (_ old) (-val #f)) v)]
|
||||
;; v cannot have type (-val #f)
|
||||
[(Var-True-Effect: v)
|
||||
(check-rest *remove (-val #f) v)])))))
|
||||
|
||||
;; the main function
|
||||
(define (tc/if-twoarm tst thn els)
|
||||
;; check in the context of the effects, and return
|
||||
(match-let* ([(tc-result: tst-ty tst-thn-eff tst-els-eff) (tc-expr tst)]
|
||||
[(tc-result: thn-ty thn-thn-eff thn-els-eff) (tc-expr/eff #t thn tst-thn-eff #f)]
|
||||
[(tc-result: els-ty els-thn-eff els-els-eff) (tc-expr/eff #f els tst-els-eff #f)])
|
||||
(match* (els-ty thn-thn-eff thn-els-eff els-thn-eff els-els-eff)
|
||||
;; this is the case for `or'
|
||||
;; the then branch has to be #t
|
||||
;; the else branch has to be a simple predicate
|
||||
;; FIXME - can something simpler be done by using demorgan's law?
|
||||
;; note that demorgan's law doesn't hold for scheme `and' and `or' because they can produce arbitrary values
|
||||
;; FIXME - mzscheme's or macro doesn't match this!
|
||||
[(_ (list (True-Effect:)) (list (True-Effect:)) (list (Restrict-Effect: t v)) (list (Remove-Effect: t v*)))
|
||||
(=> unmatch)
|
||||
(match (list tst-thn-eff tst-els-eff)
|
||||
;; check that the test was also a simple predicate
|
||||
[(list (list (Restrict-Effect: s u)) (list (Remove-Effect: s u*)))
|
||||
(if (and
|
||||
;; check that all the predicates are for the for the same identifier
|
||||
(free-identifier=? u u*)
|
||||
(free-identifier=? v v*)
|
||||
(free-identifier=? v u))
|
||||
;; this is just a very simple or
|
||||
(ret (Un (-val #t) els-ty)
|
||||
;; the then and else effects are just the union of the two types
|
||||
(list (make-Restrict-Effect (Un s t) v))
|
||||
(list (make-Remove-Effect (Un s t) v)))
|
||||
;; otherwise, something complicated is happening and we bail
|
||||
(unmatch))]
|
||||
;; similarly, bail here
|
||||
[_ (unmatch)])]
|
||||
;; this is the case for `and'
|
||||
[(_ _ _ (list (False-Effect:)) (list (False-Effect:)))
|
||||
(ret (Un (-val #f) thn-ty)
|
||||
;; we change variable effects to type effects in the test,
|
||||
;; because only the boolean result of the test is used
|
||||
;; whereas, the actual value of the then branch is returned, not just the boolean result
|
||||
(append (map var->type-eff tst-thn-eff) thn-thn-eff)
|
||||
;; no else effects for and, because any branch could have been false
|
||||
(list))]
|
||||
;; if the else branch can never happen, just use the effect of the then branch
|
||||
[((Union: (list)) _ _ _ _)
|
||||
(ret thn-ty thn-thn-eff thn-els-eff)]
|
||||
;; otherwise this expression has no effects
|
||||
[(_ _ _ _ _)
|
||||
(ret (Un thn-ty els-ty))])))
|
||||
|
||||
;; checking version
|
||||
(define (tc/if-twoarm/check tst thn els expected)
|
||||
;; check in the context of the effects, and return
|
||||
(match-let* ([(tc-result: tst-ty tst-thn-eff tst-els-eff) (tc-expr tst)]
|
||||
[(tc-result: thn-ty thn-thn-eff thn-els-eff) (tc-expr/eff #t thn tst-thn-eff expected)]
|
||||
[(tc-result: els-ty els-thn-eff els-els-eff) (tc-expr/eff #f els tst-els-eff expected)])
|
||||
(match* (els-ty thn-thn-eff thn-els-eff els-thn-eff els-els-eff)
|
||||
;; this is the case for `or'
|
||||
;; the then branch has to be #t
|
||||
;; the else branch has to be a simple predicate
|
||||
;; FIXME - can something simpler be done by using demorgan's law?
|
||||
;; note that demorgan's law doesn't hold for scheme `and' and `or' because they can produce arbitrary values
|
||||
;; FIXME - mzscheme's or macro doesn't match this!
|
||||
[(_ (list (True-Effect:)) (list (True-Effect:)) (list (Restrict-Effect: t v)) (list (Remove-Effect: t v*)))
|
||||
(=> unmatch)
|
||||
(match (list tst-thn-eff tst-els-eff)
|
||||
;; check that the test was also a simple predicate
|
||||
[(list (list (Restrict-Effect: s u)) (list (Remove-Effect: s u*)))
|
||||
(if (and
|
||||
;; check that all the predicates are for the for the same identifier
|
||||
(free-identifier=? u u*)
|
||||
(free-identifier=? v v*)
|
||||
(free-identifier=? v u))
|
||||
;; this is just a very simple or
|
||||
(let ([t (Un (-val #t) els-ty)])
|
||||
(check-below t expected)
|
||||
(ret t
|
||||
;; the then and else effects are just the union of the two types
|
||||
(list (make-Restrict-Effect (Un s t) v))
|
||||
(list (make-Remove-Effect (Un s t) v))))
|
||||
;; otherwise, something complicated is happening and we bail
|
||||
(unmatch))]
|
||||
;; similarly, bail here
|
||||
[_ (unmatch)])]
|
||||
;; this is the case for `and'
|
||||
[(_ _ _ (list (False-Effect:)) (list (False-Effect:)))
|
||||
(let ([t (Un thn-ty (-val #f))])
|
||||
(check-below t expected)
|
||||
(ret t
|
||||
;; we change variable effects to type effects in the test,
|
||||
;; because only the boolean result of the test is used
|
||||
;; whereas, the actual value of the then branch is returned, not just the boolean result
|
||||
(append (map var->type-eff tst-thn-eff) thn-thn-eff)
|
||||
;; no else effects for and, because any branch could have been false
|
||||
(list)))]
|
||||
;; if the else branch can never happen, just use the effect of the then branch
|
||||
[((Union: (list)) _ _ _ _)
|
||||
(ret thn-ty
|
||||
;; we change variable effects to type effects in the test,
|
||||
;; because only the boolean result of the test is used
|
||||
;; whereas, the actual value of the then branch is returned, not just the boolean result
|
||||
thn-thn-eff
|
||||
;; no else effects for and, because any branch could have been false
|
||||
thn-els-eff)]
|
||||
;; otherwise this expression has no effects
|
||||
[(_ _ _ _ _)
|
||||
(let ([t (Un thn-ty els-ty)])
|
||||
(check-below t expected)
|
||||
(ret t))])))
|
||||
|
|
@ -1,18 +0,0 @@
|
|||
#lang scheme/unit
|
||||
|
||||
(require "signatures.ss" "../utils/utils.ss")
|
||||
(require (utils tc-utils))
|
||||
|
||||
(import tc-expr^ tc-lambda^ tc-dots^)
|
||||
(export tc-app^)
|
||||
|
||||
(define (tc/app . args)
|
||||
(int-err "tc/app NYI"))
|
||||
|
||||
(define (tc/app/check . args)
|
||||
(int-err "tc/app/check NYI"))
|
||||
|
||||
(define (tc/funapp . args)
|
||||
(int-err "tc/funapp NYI"))
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user