Make let correctly implement the TC-Let rule from the paper.
original commit: b9e7d087bae3ea5d9a46a426607d4986e7bc189d
This commit is contained in:
Eric Dobson
parent
6864b0fb79
commit
4311b0b052
|
|
@ -531,5 +531,5 @@
|
|||
(with-lexical-env/extend
|
||||
(list name) (list ft)
|
||||
(values
|
||||
(erase-names/results formals (ret ft))
|
||||
(erase-names/results formals (tc-body/check body return)))))))
|
||||
(replace-names (map (λ (f) (list f -empty-obj)) formals) (ret ft))
|
||||
(replace-names (map (λ (f) (list f -empty-obj)) formals) (tc-body/check body return)))))))
|
||||
|
|
|
|||
|
|
@ -11,6 +11,7 @@
|
|||
(typecheck signatures tc-metafunctions internal-forms)
|
||||
(utils tarjan)
|
||||
racket/match (contract-req)
|
||||
racket/list
|
||||
syntax/parse syntax/stx
|
||||
syntax/id-table
|
||||
;; For internal type forms
|
||||
|
|
@ -20,12 +21,25 @@
|
|||
(import tc-expr^)
|
||||
(export tc-let^)
|
||||
|
||||
(define/cond-contract (do-check expr->type namess results expected-results exprs body expected #:abstract [abstract null])
|
||||
(((syntax? tc-results/c . -> . any/c)
|
||||
(listof (listof identifier?)) (listof tc-results/c) (listof tc-results/c)
|
||||
(listof syntax?) (listof syntax?) (or/c #f tc-results/c))
|
||||
(#:abstract any/c)
|
||||
. ->* .
|
||||
;; get-names+objects (listof (listof identifier?)) (listof tc-results?) -> (listof (list/c identifier Object?))
|
||||
;; Given a list of bindings and the tc-results for the corresponding expressions, return a list of
|
||||
;; tuples of the binding-name and corresponding objects from the results.
|
||||
;; This is used to replace the names with the objects after the names go out of scope.
|
||||
(define (get-names+objects namess results)
|
||||
(append*
|
||||
(for/list ([names namess] [results results])
|
||||
(match results
|
||||
[(tc-results: _ _ os)
|
||||
(map list names os)]))))
|
||||
|
||||
;; Checks that the body has the expected type when names are bound to the types spcified by results.
|
||||
;; The exprs are also typechecked by using expr->type.
|
||||
;; TODO: make this function sane.
|
||||
(define/cond-contract (do-check expr->type namess results expected-results exprs body expected)
|
||||
((syntax? tc-results/c . -> . any/c)
|
||||
(listof (listof identifier?)) (listof tc-results/c) (listof tc-results/c)
|
||||
(listof syntax?) syntax? (or/c #f tc-results/c)
|
||||
. -> .
|
||||
tc-results/c)
|
||||
(with-cond-contract t/p ([types (listof (listof Type/c))] ; types that may contain undefined (letrec)
|
||||
[expected-types (listof (listof Type/c))] ; types that may not contain undefined (what we got from the user)
|
||||
|
|
@ -74,7 +88,7 @@
|
|||
expected-types ; types w/o undefined
|
||||
(append p1 p2)
|
||||
;; typecheck the body
|
||||
(erase-names/results (apply append abstract namess)
|
||||
(replace-names (get-names+objects namess expected-results)
|
||||
(if expected
|
||||
(tc-body/check body (erase-filter expected))
|
||||
(tc-body body))))))
|
||||
|
|
@ -130,44 +144,47 @@
|
|||
(values name expr)))
|
||||
|
||||
;; Check those and gather an environment for use below
|
||||
(define-values (env-names env-types)
|
||||
(define-values (env-names env-results)
|
||||
(check-non-recursive-clauses ordered-clauses))
|
||||
|
||||
(with-lexical-env/extend env-names env-types
|
||||
(cond
|
||||
;; after everything, check the body expressions
|
||||
[(null? remaining-names)
|
||||
(do-check void null null null null body expected #:abstract orig-flat-names)]
|
||||
[else
|
||||
(define flat-names (apply append remaining-names))
|
||||
(do-check tc-expr/check
|
||||
remaining-names
|
||||
;; compute set of variables that can't be undefined. see below.
|
||||
(let-values
|
||||
([(safe-bindings _)
|
||||
(for/fold ([safe-bindings '()] ; includes transitively-safe
|
||||
[transitively-safe-bindings '()])
|
||||
([names (in-list remaining-names)]
|
||||
[expr (in-list remaining-exprs)])
|
||||
(case (safe-letrec-values-clause? expr transitively-safe-bindings flat-names)
|
||||
;; transitively safe -> safe to mention in a subsequent rhs
|
||||
[(transitively-safe) (values (append names safe-bindings)
|
||||
(append names transitively-safe-bindings))]
|
||||
;; safe -> safe by itself, but may not be safe to use in a subsequent rhs
|
||||
[(safe) (values (append names safe-bindings)
|
||||
transitively-safe-bindings)]
|
||||
;; unsafe -> could be undefined
|
||||
[(unsafe) (values safe-bindings transitively-safe-bindings)]))])
|
||||
(map (λ (l) (let ([types-from-user (map get-type l)])
|
||||
(ret (if (andmap (λ (x) ; are all the lhs vars safe?
|
||||
(member x safe-bindings bound-identifier=?))
|
||||
l)
|
||||
types-from-user
|
||||
(map (λ (x) (Un x -Undefined)) types-from-user)))))
|
||||
remaining-names))
|
||||
;; types the user gave. check against that to error if we could get undefined
|
||||
(map (λ (l) (ret (map get-type l))) remaining-names)
|
||||
remaining-exprs body expected)]))))
|
||||
(replace-names (get-names+objects env-names env-results)
|
||||
(with-lexical-env/extend env-names (map tc-results-ts env-results)
|
||||
(cond
|
||||
;; after everything, check the body expressions
|
||||
[(null? remaining-names)
|
||||
(if expected
|
||||
(tc-body/check body (erase-filter expected))
|
||||
(tc-body body))]
|
||||
[else
|
||||
(define flat-names (apply append remaining-names))
|
||||
(do-check tc-expr/check
|
||||
remaining-names
|
||||
;; compute set of variables that can't be undefined. see below.
|
||||
(let-values
|
||||
([(safe-bindings _)
|
||||
(for/fold ([safe-bindings '()] ; includes transitively-safe
|
||||
[transitively-safe-bindings '()])
|
||||
([names (in-list remaining-names)]
|
||||
[expr (in-list remaining-exprs)])
|
||||
(case (safe-letrec-values-clause? expr transitively-safe-bindings flat-names)
|
||||
;; transitively safe -> safe to mention in a subsequent rhs
|
||||
[(transitively-safe) (values (append names safe-bindings)
|
||||
(append names transitively-safe-bindings))]
|
||||
;; safe -> safe by itself, but may not be safe to use in a subsequent rhs
|
||||
[(safe) (values (append names safe-bindings)
|
||||
transitively-safe-bindings)]
|
||||
;; unsafe -> could be undefined
|
||||
[(unsafe) (values safe-bindings transitively-safe-bindings)]))])
|
||||
(map (λ (l) (let ([types-from-user (map get-type l)])
|
||||
(ret (if (andmap (λ (x) ; are all the lhs vars safe?
|
||||
(member x safe-bindings bound-identifier=?))
|
||||
l)
|
||||
types-from-user
|
||||
(map (λ (x) (Un x -Undefined)) types-from-user)))))
|
||||
remaining-names))
|
||||
;; types the user gave. check against that to error if we could get undefined
|
||||
(map (λ (l) (ret (map get-type l))) remaining-names)
|
||||
remaining-exprs body expected)])))))
|
||||
|
||||
;; An lr-clause is a
|
||||
;; (lr-clause (Listof Identifier) Syntax)
|
||||
|
|
@ -233,7 +250,7 @@
|
|||
remaining))
|
||||
|
||||
;; check-non-recursive-clauses : (Listof lr-clause) ->
|
||||
;; (Listof Identifier) (Listof Type)
|
||||
;; (Listof (Listof Identifier)) (Listof tc-results)
|
||||
;; Given a list of non-recursive clauses, check the clauses in order and
|
||||
;; build up a type environment for use in the second pass.
|
||||
(define (check-non-recursive-clauses clauses)
|
||||
|
|
@ -245,11 +262,10 @@
|
|||
(get-type/infer names expr
|
||||
(lambda (e) (tc-expr/maybe-expected/t e names))
|
||||
tc-expr/check))
|
||||
(match-define (tc-results: types) results)
|
||||
(with-lexical-env/extend names types
|
||||
(with-lexical-env/extend names (tc-results-ts results)
|
||||
(loop (cdr clauses)
|
||||
(cons names env-ids)
|
||||
(cons types env-types)))])))
|
||||
(cons results env-types)))])))
|
||||
|
||||
;; determines whether any of the variables bound in the given clause can have an undefined value
|
||||
;; in this case, we cannot trust the type the user gave us and must union it with undefined
|
||||
|
|
|
|||
|
|
@ -9,10 +9,13 @@
|
|||
(contract-req))
|
||||
|
||||
(provide abstract-results
|
||||
erase-names/results
|
||||
combine-props
|
||||
tc-results->values)
|
||||
|
||||
(provide/cond-contract
|
||||
[replace-names (-> (listof (list/c identifier? Object?)) tc-results/c tc-results/c)])
|
||||
|
||||
|
||||
;; abstract-results
|
||||
;;
|
||||
;; Given results from the range of a lambda, abstract any
|
||||
|
|
@ -236,16 +239,14 @@
|
|||
[(Bot:) (set-box! flag #f) (values derived-props derived-atoms)]
|
||||
[_ (loop (cons p derived-props) derived-atoms (cdr worklist))])))))
|
||||
|
||||
;; erase-names/results: (listof identifier?) tc-results? -> tc-results?
|
||||
;; Maps all of the given names in the results to the empty object.
|
||||
;; replace-names: (listof (list/c identifier? Object?) tc-results? -> tc-results?
|
||||
;; For each name replaces all uses of it in res with the corresponding object.
|
||||
;; This is used so that names do not escape the scope of their definitions
|
||||
;; TODO support mapping names to other objects.
|
||||
(define (erase-names/results names res)
|
||||
(define (replace-names names+objects res)
|
||||
(define (subber proc lst)
|
||||
(for/list ([i (in-list lst)])
|
||||
(for/fold ([s i])
|
||||
([nm (in-list names)])
|
||||
(proc s nm -empty-obj #t))))
|
||||
(for/fold ([s i]) ([name/object (in-list names+objects)])
|
||||
(proc s (first name/object) (second name/object) #t))))
|
||||
(match res
|
||||
[(tc-any-results:) res]
|
||||
[(tc-results: ts fs os)
|
||||
|
|
|
|||
|
|
@ -2,6 +2,7 @@
|
|||
|
||||
(require "abbrev.rkt" "../rep/type-rep.rkt"
|
||||
"../utils/tc-utils.rkt"
|
||||
"tc-result.rkt"
|
||||
racket/list racket/set racket/dict racket/match
|
||||
syntax/parse)
|
||||
|
||||
|
|
@ -68,6 +69,20 @@
|
|||
(make-arr* ts/false rng #:drest drest)))
|
||||
(list (make-arr* ts rng #:rest rest #:drest drest)))))
|
||||
|
||||
|
||||
;; This is used to fix the filters of keyword types.
|
||||
;; TODO: This should also explore deeper into the actual types and remove filters in there as well.
|
||||
;; TODO: This should not remove the filters but instead make them refer to the actual arguments after
|
||||
;; keyword conversion.
|
||||
(define (erase-filter/Values values)
|
||||
(match values
|
||||
[(AnyValues:) values]
|
||||
[(Results: ts fs os)
|
||||
(-values ts)]
|
||||
[(Results: ts fs os dty dbound)
|
||||
(-values-dots ts dty dbound)]))
|
||||
|
||||
|
||||
(define (prefix-of a b)
|
||||
(define (rest-equal? a b)
|
||||
(match* (a b)
|
||||
|
|
@ -176,7 +191,7 @@
|
|||
(and rest? (last other-args)))
|
||||
(make-Function
|
||||
(list (make-arr* (take other-args non-kw-argc)
|
||||
rng
|
||||
(erase-filter/Values rng)
|
||||
#:kws actual-kws
|
||||
#:rest rest-type)))]
|
||||
[(and (even? (length arrs)) ; had optional args
|
||||
|
|
@ -198,7 +213,7 @@
|
|||
(make-Function
|
||||
(for/list ([to-take (in-range (add1 (length opt-types)))])
|
||||
(make-arr* (append mand-args (take opt-types to-take))
|
||||
rng
|
||||
(erase-filter/Values rng)
|
||||
#:kws actual-kws
|
||||
#:rest rest-type)))]
|
||||
[else (int-err "unsupported arrs in keyword function type")])]
|
||||
|
|
|
|||
|
|
@ -51,7 +51,7 @@
|
|||
[(_ tp) (struct tc-results ((list (struct tc-result (tp _ _)))
|
||||
#f))]))
|
||||
|
||||
(define (tc-results-t tc)
|
||||
(define (tc-results-ts* tc)
|
||||
(match tc
|
||||
[(tc-results: t) t]))
|
||||
|
||||
|
|
@ -63,7 +63,8 @@
|
|||
(define-match-expander Results:
|
||||
(syntax-rules ()
|
||||
[(_ tp) (Values: (list (Result: tp _ _) (... ...)))]
|
||||
[(_ tp fp op) (Values: (list (Result: tp fp op) (... ...)))]))
|
||||
[(_ tp fp op) (Values: (list (Result: tp fp op) (... ...)))]
|
||||
[(_ tp fp op dty dbound) (ValuesDots: (list (Result: tp fp op) (... ...)) dty dbound)]))
|
||||
|
||||
;; convenience function for returning the result of typechecking an expression
|
||||
(define ret
|
||||
|
|
@ -125,6 +126,7 @@
|
|||
(provide/cond-contract
|
||||
[combine-results ((c:listof tc-results?) . c:-> . tc-results?)]
|
||||
[tc-result-t (tc-result? . c:-> . Type/c)]
|
||||
[rename tc-results-ts* tc-results-ts (tc-results? . c:-> . (c:listof Type/c))]
|
||||
[tc-result-equal? (tc-result? tc-result? . c:-> . boolean?)]
|
||||
[tc-results? (c:any/c . c:-> . boolean?)]
|
||||
[tc-results/c c:flat-contract?])
|
||||
|
|
|
|||
|
|
@ -1205,12 +1205,12 @@
|
|||
#f)
|
||||
#:ret (ret -Void -top-filter -empty-obj)]
|
||||
[tc-err (apply +)]
|
||||
[tc-e/t
|
||||
[tc-e
|
||||
(let ([x eof])
|
||||
(if (procedure? x)
|
||||
x
|
||||
(lambda (z) (eq? x z))))
|
||||
(make-pred-ty (-val eof))]
|
||||
#:ret (ret (make-pred-ty (-val eof)) (-FS (-not-filter top-func #'eof) -bot))]
|
||||
[tc-e ((inst map Number (Pairof Number Number)) car (ann (list (cons 1 2) (cons 2 3) (cons 4 5)) (Listof (Pairof Number Number))))
|
||||
(-lst -Number)]
|
||||
[tc-err (list (values 1 2))
|
||||
|
|
@ -2651,6 +2651,22 @@
|
|||
0))
|
||||
#:ret (ret -Bottom)]
|
||||
|
||||
[tc-e
|
||||
(let: ([x : Any 4])
|
||||
(if (let: ([y x]) (number? y))
|
||||
(add1 x)
|
||||
4))
|
||||
-Number]
|
||||
|
||||
[tc-e
|
||||
(let ()
|
||||
(: g (-> Boolean))
|
||||
(define (g) (g))
|
||||
(: x Any)
|
||||
(define x 0)
|
||||
(number? x))
|
||||
-Boolean]
|
||||
|
||||
)
|
||||
(test-suite
|
||||
"tc-literal tests"
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user