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

Make update do actual structural recursion over the path.

Browse Source 
original commit: 0d85aa79a380758c9be14a328a885547fdcb0040
This commit is contained in:
Eric Dobson 2014-05-23 08:13:58 -07:00
parent 8ec892abba
commit 3637f691ef
1 changed files with 24 additions and 41 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

65
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt
View File

@ -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))