From f3104f383eb56a365a1831fd90d8d25dce860472 Mon Sep 17 00:00:00 2001 From: Andrew Kent Date: Fri, 9 Jan 2015 23:03:15 -0500 Subject: [PATCH 1/2] path-type allow non-subtype struct acc proper path-type mismatch error --- .../typed-racket/env/lexical-env.rkt | 59 +------------------ .../typed-racket/typecheck/tc-expr-unit.rkt | 3 +- 2 files changed, 5 insertions(+), 57 deletions(-) diff --git a/typed-racket-lib/typed-racket/env/lexical-env.rkt b/typed-racket-lib/typed-racket/env/lexical-env.rkt index 1bf2e9d8..813fedc5 100644 --- a/typed-racket-lib/typed-racket/env/lexical-env.rkt +++ b/typed-racket-lib/typed-racket/env/lexical-env.rkt @@ -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)])) diff --git a/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt b/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt index 44039eaf..23975ca8 100644 --- a/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt +++ b/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt @@ -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) From fd4f05e64b374f1de8ff1de988752e7841217989 Mon Sep 17 00:00:00 2001 From: Andrew Kent Date: Sat, 10 Jan 2015 15:11:10 -0500 Subject: [PATCH 2/2] path-type sep file --- .../typed-racket/types/path-type.rkt | 64 +++++++++++++++++++ 1 file changed, 64 insertions(+) create mode 100644 typed-racket-lib/typed-racket/types/path-type.rkt diff --git a/typed-racket-lib/typed-racket/types/path-type.rkt b/typed-racket-lib/typed-racket/types/path-type.rkt new file mode 100644 index 00000000..d1be728f --- /dev/null +++ b/typed-racket-lib/typed-racket/types/path-type.rkt @@ -0,0 +1,64 @@ +#lang racket/base + +(require "../utils/utils.rkt" + racket/match racket/set + (contract-req) + (rep object-rep type-rep) + (utils tc-utils) + (typecheck renamer) + (types subtype resolve union) + (except-in (types utils abbrev kw-types) -> ->* one-of/c)) + +(provide/cond-contract + [path-type ((listof PathElem?) Type/c . -> . Type/c)]) + + +;; 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 =( + [(_ _) Err])) +