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

Make filters on mutated/undefined vars an error.

Browse Source 
Closes PR 14422.
Closes PR 14495.
This commit is contained in:
Eric Dobson 2014-07-06 23:24:16 -07:00
parent 5c5bc86915
commit fdd7679426
2 changed files with 48 additions and 28 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

54
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/parse-type.rkt
View File

@ -10,7 +10,7 @@
(utils tc-utils stxclass-util literal-syntax-class) (utils tc-utils stxclass-util literal-syntax-class)
syntax/stx (prefix-in c: (contract-req)) syntax/stx (prefix-in c: (contract-req))
syntax/parse unstable/sequence syntax/parse unstable/sequence
(env tvar-env type-name-env type-alias-env (env tvar-env type-name-env type-alias-env mvar-env
lexical-env index-env row-constraint-env) lexical-env index-env row-constraint-env)
(only-in racket/list flatten) (only-in racket/list flatten)
racket/dict racket/dict
@ -210,17 +210,6 @@
(pattern :cdr^ (pattern :cdr^
#:attr pe (make-CdrPE))) #:attr pe (make-CdrPE)))
(define-splicing-syntax-class idx-obj
#:description "index object"
#:attributes (arg depth path)
(pattern (~seq idx:nat)
#:attr arg (syntax-e #'idx)
#:attr depth 0
#:attr path (-arg-path (attribute arg) (attribute depth)))
(pattern (~seq depth-idx:nat idx:nat)
#:attr arg (syntax-e #'idx)
#:attr depth (syntax-e #'depth-idx)
#:attr path (-arg-path (attribute arg) (attribute depth))))
(define-syntax-class @ (define-syntax-class @
#:description "@" #:description "@"
@ -244,22 +233,12 @@
#:attributes (prop) #:attributes (prop)
(pattern :Top^ #:attr prop -top) (pattern :Top^ #:attr prop -top)
(pattern :Bot^ #:attr prop -bot) (pattern :Bot^ #:attr prop -bot)
(pattern (t:expr :@ pe:path-elem ... i:id)
#:attr prop (-filter (parse-type #'t) (-acc-path (attribute pe.pe) (-id-path #'i))))
;; Here is wrong check ;; Here is wrong check
(pattern (t:expr :@ ~! pe:path-elem ... i:idx-obj) (pattern (t:expr :@ ~! pe:path-elem ... (~var o (filter-object doms)))
#:fail-unless (< (attribute i.arg) (length doms)) #:attr prop (-filter (parse-type #'t) (-acc-path (attribute pe.pe) (attribute o.obj))))
(format "Filter proposition's object index ~a is larger than argument length ~a"
(attribute i.arg) (length doms))
#:attr prop (-filter (parse-type #'t) (-acc-path (attribute pe.pe) (attribute i.path))))
(pattern (:! t:expr :@ pe:path-elem ... i:id)
#:attr prop (-not-filter (parse-type #'t) (-acc-path (attribute pe.pe) (-id-path #'i))))
;; Here is wrong check ;; Here is wrong check
(pattern (:! t:expr :@ ~! pe:path-elem ... i:idx-obj) (pattern (:! t:expr :@ ~! pe:path-elem ... (~var o (filter-object doms)))
#:fail-unless (< (attribute i.arg) (length doms)) #:attr prop (-not-filter (parse-type #'t) (-acc-path (attribute pe.pe) (attribute o.obj))))
(format "Filter proposition's object index ~a is larger than argument length ~a"
(attribute i.arg) (length doms))
#:attr prop (-not-filter (parse-type #'t) (-acc-path (attribute pe.pe) (attribute i.path))))
(pattern (:! t:expr) (pattern (:! t:expr)
#:attr prop (-not-filter (parse-type #'t) 0)) #:attr prop (-not-filter (parse-type #'t) 0))
(pattern (and (~var p (prop doms)) ...) (pattern (and (~var p (prop doms)) ...)
@ -271,6 +250,29 @@
(pattern t:expr (pattern t:expr
#:attr prop (-filter (parse-type #'t) 0))) #:attr prop (-filter (parse-type #'t) 0)))
(define-splicing-syntax-class (filter-object doms)
#:description "filter object"
#:attributes (obj)
(pattern i:id
#:fail-unless (identifier-binding #'i)
"Filters for predicates may not reference identifiers that are unbound"
#:fail-when (is-var-mutated? #'i)
"Filters for predicates may not reference identifiers that are mutated"
#:attr obj (-id-path #'i))
(pattern idx:nat
#:do [(define arg (syntax-e #'idx))]
#:fail-unless (< arg (length doms))
(format "Filter proposition's object index ~a is larger than argument length ~a"
arg (length doms))
#:attr obj (-arg-path arg 0))
(pattern (~seq depth-idx:nat idx:nat)
#:do [(define arg (syntax-e #'idx))]
#:fail-unless (< arg (length doms))
(format "Filter proposition's object index ~a is larger than argument length ~a"
arg (length doms))
#:attr obj (-arg-path arg (syntax-e #'depth-idx))))
(define-syntax-class object (define-syntax-class object
#:attributes (object) #:attributes (object)
(pattern e:expr (pattern e:expr

22
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/parse-type-tests.rkt
View File

@ -7,7 +7,7 @@
racket/set racket/set
syntax/parse syntax/parse
(base-env base-structs) (base-env base-structs)
(env tvar-env type-alias-env) (env tvar-env type-alias-env mvar-env)
(utils tc-utils) (utils tc-utils)
(private parse-type) (private parse-type)
(rep type-rep) (rep type-rep)
@ -26,8 +26,13 @@
(provide tests) (provide tests)
(gen-test-main) (gen-test-main)
(define mutated-var #f)
(define not-mutated-var #f)
(begin-for-syntax (begin-for-syntax
(do-standard-inits)) (do-standard-inits)
(register-mutated-var #'mutated-var))
(define-syntax (pt-test stx) (define-syntax (pt-test stx)
(syntax-parse stx (syntax-parse stx
@ -172,6 +177,19 @@
(t:-> -Integer (-poly (x) (t:-> x x)))] (t:-> -Integer (-poly (x) (t:-> x x)))]
[FAIL -> #:msg "incorrect use of -> type constructor"] [FAIL -> #:msg "incorrect use of -> type constructor"]
[(Any -> Boolean : #:+ (Symbol @ not-mutated-var))
(t:-> Univ -Boolean : (-FS (-filter -Symbol (-id-path #'not-mutated-var)) -top))]
[FAIL (Any -> Boolean : #:+ (Symbol @ mutated-var))
#:msg "may not reference identifiers that are mutated"]
[(Any -> Boolean : #:+ (! Symbol @ not-mutated-var))
(t:-> Univ -Boolean : (-FS (-not-filter -Symbol (-id-path #'not-mutated-var)) -top))]
[FAIL (Any -> Boolean : #:+ (! Symbol @ mutated-var))
#:msg "may not reference identifiers that are mutated"]
[FAIL (Any -> Boolean : #:+ (String @ unbound))
#:msg "may not reference identifiers that are unbound"]
;; ->* types ;; ->* types
[(->* (String Symbol) Void) (t:-> -String -Symbol -Void)] [(->* (String Symbol) Void) (t:-> -String -Symbol -Void)]
[(->* (String Symbol) (String) Void) [(->* (String Symbol) (String) Void)