suzanne.soy/typed-racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

path-type allow non-subtype struct acc

Browse Source 
proper path-type mismatch error
This commit is contained in:
Andrew Kent 2015-01-09 23:03:15 -05:00
parent 864b0ad5fc
commit f3104f383e
2 changed files with 5 additions and 57 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

59
typed-racket-lib/typed-racket/env/lexical-env.rkt vendored
View File

@ -7,15 +7,13 @@
;; but split here for performance
(require "../utils/utils.rkt"
racket/keyword-transform racket/list racket/match racket/set
racket/keyword-transform racket/list
(for-syntax syntax/parse racket/base)
(contract-req)
(contract-req)
(env type-env-structs global-env mvar-env)
(rep object-rep type-rep rep-utils)
(utils tc-utils)
(only-in (rep type-rep) Type/c)
(typecheck renamer)
(types subtype resolve union)
(except-in (types utils abbrev kw-types) -> ->* one-of/c))
(provide lexical-env
@ -25,8 +23,7 @@
update-type/lexical)
(provide/cond-contract
[lookup-type/lexical ((identifier?) (env? #:fail (or/c #f (-> any/c #f))) . ->* . (or/c Type/c #f))]
[lookup-alias/lexical ((identifier?) (env?) . ->* . (or/c Path? Empty?))]
[path-type ((listof PathElem?) Type/c . -> . Type/c)])
[lookup-alias/lexical ((identifier?) (env?) . ->* . (or/c Path? Empty?))])
;; the current lexical environment
(define lexical-env (make-parameter empty-prop-env))
@ -100,53 +97,3 @@
[new-v (f i v)]
[new-env (extend env i new-v)])
new-env)))]))
;; returns the result of following a path into a type
;; (Listof PathElem) Type -> Type
;; Ex. '(CarPE) (Pair α β) -> α
;; resolved is the set of resolved types so far at a particular
;; path - it ensures we are making progress, that we do not
;; continue unfolding types infinitely while not progressing.
;; It is intentionally reset each time we decrease the
;; paths size on a recursive call, and maintained/extended
;; when the path does not decrease on a recursive call.
(define (path-type path t [resolved (set)])
(match* (t path)
;; empty path
[(t (list)) t]
;; pair ops
[((Pair: t s) (list rst ... (CarPE:)))
(path-type rst t)]
[((Pair: t s) (list rst ... (CdrPE:)))
(path-type rst s)]
;; syntax ops
[((Syntax: t) (list rst ... (SyntaxPE:)))
(path-type rst t)]
;; promise op
[((Promise: t) (list rst ... (ForcePE:)))
(path-type rst t)]
;; struct ops
[((Struct: nm par flds proc poly pred)
(list rst ... (StructPE: (? (λ (s) (subtype t s)) s) idx)))
(match-let ([(fld: ft _ _) (list-ref flds idx)])
(path-type rst ft))]
[((Union: ts) _)
(apply Un (map (λ (t) (path-type path t resolved)) ts))]
;; paths into polymorphic types
[((Poly: _ body-t) _) (path-type path body-t resolved)]
[((PolyDots: _ body-t) _) (path-type path body-t resolved)]
[((PolyRow: _ _ body-t) _) (path-type path body-t resolved)]
;; types which need resolving
[((? needs-resolving?) _) #:when (not (set-member? resolved t))
(path-type path (resolve-once t) (set-add resolved t))]
;; type/path mismatch =(
[(_ _)
(int-err "\n\tBad path/type lookup!\n\tPath:~a\n\tType: ~a\n" path t)]))

3
typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
View File

@ -5,7 +5,8 @@
racket/match (prefix-in - (contract-req))
"signatures.rkt"
"check-below.rkt" "../types/kw-types.rkt"
(types utils abbrev union subtype type-table filter-ops remove-intersect resolve generalize)
(types utils abbrev union subtype type-table path-type
filter-ops remove-intersect resolve generalize)
(private-in syntax-properties)
(rep type-rep filter-rep object-rep)
(only-in (infer infer) restrict)