diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt index 0013ff0b..ec480f79 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt @@ -5,7 +5,7 @@ unstable/list (contract-req) (infer-in infer) - (rep type-rep filter-rep object-rep) + (rep type-rep filter-rep object-rep rep-utils) (utils tc-utils) (types resolve subtype remove-intersect union) (only-in (env type-env-structs lexical-env) @@ -18,60 +18,43 @@ ;(trace replace-nth) -(define/cond-contract (update t lo) - (Type/c Filter/c . -> . Type/c) +(define/cond-contract (update t ft pos? lo) + (Type/c Type/c boolean? (listof PathElem?) . -> . Type/c) (match* ((resolve t) lo) ;; pair ops - [((Pair: t s) (TypeFilter: u (list rst ... (CarPE:)) x)) - (make-Pair (update t (-filter u x rst)) s)] - [((Pair: t s) (NotTypeFilter: u (list rst ... (CarPE:)) x)) - (make-Pair (update t (-not-filter u x rst)) s)] - [((Pair: t s) (TypeFilter: u (list rst ... (CdrPE:)) x)) - (make-Pair t (update s (-filter u x rst)))] - [((Pair: t s) (NotTypeFilter: u (list rst ... (CdrPE:)) x)) - (make-Pair t (update s (-not-filter u x rst)))] + [((Pair: t s) (list rst ... (CarPE:))) + (-pair (update t ft pos? rst) s)] + [((Pair: t s) (list rst ... (CdrPE:))) + (-pair t (update s ft pos? rst))] ;; syntax ops - [((Syntax: t) (TypeFilter: u (list rst ... (SyntaxPE:)) x)) - (make-Syntax (update t (-filter u x rst)))] - [((Syntax: t) (NotTypeFilter: u (list rst ... (SyntaxPE:)) x)) - (make-Syntax (update t (-not-filter u x rst)))] + [((Syntax: t) (list rst ... (SyntaxPE:))) + (-Syntax (update t ft pos? rst))] ;; promise op - [((Promise: t) (TypeFilter: u (list rst ... (ForcePE:)) x)) - (make-Promise (update t (-filter u x rst)))] - [((Promise: t) (NotTypeFilter: u (list rst ... (ForcePE:)) x)) - (make-Promise (update t (-not-filter u x rst)))] + [((Promise: t) (list rst ... (ForcePE:))) + (-Promise (update t ft pos? rst))] ;; struct ops [((Struct: nm par flds proc poly pred) - (TypeFilter: u (list rst ... (StructPE: (? (lambda (s) (subtype t s)) s) idx)) x)) + (list rst ... (StructPE: (? (lambda (s) (subtype t s)) s) idx))) (make-Struct nm par - (list-update flds idx - (match-lambda [(fld: e acc-id #f) - (make-fld - (update e (-filter u x rst)) - acc-id #f)] - [_ (int-err "update on mutable struct field")])) - proc poly pred)] - [((Struct: nm par flds proc poly pred) - (NotTypeFilter: u (list rst ... (StructPE: (? (lambda (s) (subtype t s)) s) idx)) x)) - (make-Struct nm par (list-update flds idx - (match-lambda [(fld: e acc-id #f) - (make-fld - (update e (-not-filter u x rst)) - acc-id #f)] + (list-update flds idx (match-lambda + [(fld: e acc-id #f) + (make-fld (update e ft pos? rst) acc-id #f)] [_ (int-err "update on mutable struct field")])) proc poly pred)] ;; otherwise - [(t (TypeFilter: u (list) _)) - (restrict t u)] - [(t (NotTypeFilter: u (list) _)) - (remove t u)] + [(t (list)) + (if pos? + (restrict t ft) + (remove t ft))] [((Union: ts) lo) - (apply Un (map (lambda (t) (update t lo)) ts))] + (apply Un (map (lambda (t) (update t ft pos? lo)) ts))] [(t* lo) + ;; This likely comes up with (-lst t) and we need to improve the system to make sure this case + ;; dosen't happen #; (int-err "update along ill-typed path: ~a ~a ~a" t t* lo) t])) @@ -84,8 +67,8 @@ (for/fold ([Γ (replace-props env (append atoms props))]) ([f (in-list atoms)]) (match f [(Bot:) (set-box! flag #f) (env-map (lambda (k v) (Un)) Γ)] - [(or (TypeFilter: _ _ x) (NotTypeFilter: _ _ x)) - (update-type/lexical (lambda (x t) (let ([new-t (update t f)]) + [(or (TypeFilter: ft lo x) (NotTypeFilter: ft lo x)) + (update-type/lexical (lambda (x t) (let ([new-t (update t ft (TypeFilter? f) lo)]) (when (type-equal? new-t (Un)) (set-box! flag #f)) new-t))