From 917b4edd3809dea0874adfaa795657187991914d Mon Sep 17 00:00:00 2001 From: Eric Dobson Date: Sun, 6 Jul 2014 23:24:16 -0700 Subject: [PATCH] Make filters on mutated/undefined vars an error. Closes PR 14422. Closes PR 14495. original commit: fdd76794265c752492832b1f91a20ce96ac61930 --- .../typed-racket/private/parse-type.rkt | 54 ++++++++++--------- .../unit-tests/parse-type-tests.rkt | 22 +++++++- 2 files changed, 48 insertions(+), 28 deletions(-) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/parse-type.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/parse-type.rkt index 48a9e7b6..0d326db4 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/parse-type.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/parse-type.rkt @@ -10,7 +10,7 @@ (utils tc-utils stxclass-util literal-syntax-class) syntax/stx (prefix-in c: (contract-req)) 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) (only-in racket/list flatten) racket/dict @@ -210,17 +210,6 @@ (pattern :cdr^ #: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 @ #:description "@" @@ -244,22 +233,12 @@ #:attributes (prop) (pattern :Top^ #:attr prop -top) (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 - (pattern (t:expr :@ ~! pe:path-elem ... i:idx-obj) - #:fail-unless (< (attribute i.arg) (length doms)) - (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)))) + (pattern (t:expr :@ ~! pe:path-elem ... (~var o (filter-object doms))) + #:attr prop (-filter (parse-type #'t) (-acc-path (attribute pe.pe) (attribute o.obj)))) ;; Here is wrong check - (pattern (:! t:expr :@ ~! pe:path-elem ... i:idx-obj) - #:fail-unless (< (attribute i.arg) (length doms)) - (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 :@ ~! pe:path-elem ... (~var o (filter-object doms))) + #:attr prop (-not-filter (parse-type #'t) (-acc-path (attribute pe.pe) (attribute o.obj)))) (pattern (:! t:expr) #:attr prop (-not-filter (parse-type #'t) 0)) (pattern (and (~var p (prop doms)) ...) @@ -271,6 +250,29 @@ (pattern t:expr #: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 #:attributes (object) (pattern e:expr diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/parse-type-tests.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/parse-type-tests.rkt index ca4e6558..2cf23c80 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/parse-type-tests.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/parse-type-tests.rkt @@ -7,7 +7,7 @@ racket/set syntax/parse (base-env base-structs) - (env tvar-env type-alias-env) + (env tvar-env type-alias-env mvar-env) (utils tc-utils) (private parse-type) (rep type-rep) @@ -26,8 +26,13 @@ (provide tests) (gen-test-main) + +(define mutated-var #f) +(define not-mutated-var #f) + (begin-for-syntax - (do-standard-inits)) + (do-standard-inits) + (register-mutated-var #'mutated-var)) (define-syntax (pt-test stx) (syntax-parse stx @@ -172,6 +177,19 @@ (t:-> -Integer (-poly (x) (t:-> x x)))] [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 [(->* (String Symbol) Void) (t:-> -String -Symbol -Void)] [(->* (String Symbol) (String) Void)