Improve error checking for filter objects

original commit: 73050139340c0785c2dfc2cd14ee8e82c16ae4ed
This commit is contained in:
Asumu Takikawa 2013-09-06 14:39:37 -04:00
parent 6188a21d8a
commit 072d05791b
2 changed files with 36 additions and 12 deletions

View File

@ -113,23 +113,30 @@
#:attr type (parse-type #'t)
#:attr path '()))
(define-syntax-class prop
(define-syntax-class (prop doms)
#:description "filter proposition"
#:attributes (prop)
(pattern (~literal Top) #:attr prop -top)
(pattern (~literal Bot) #:attr prop -bot)
(pattern (t:expr (~describe "@" (~datum @)) pe:path-elem ... i:nat)
#:fail-unless (< (syntax-e #'i) (length doms))
(format "Filter proposition's object index ~a is larger than argument length ~a"
(syntax-e #'i) (length doms))
#:attr prop (-filter (parse-type #'t) (syntax-e #'i) (attribute pe.pe)))
(pattern (t:expr (~describe "@" (~datum @)) pe:path-elem ... i:id)
#:attr prop (-filter (parse-type #'t) #'i (attribute pe.pe)))
(pattern ((~datum !) t:expr (~describe "@" (~datum @)) pe:path-elem ... i:nat)
#:fail-unless (< (syntax-e #'i) (length doms))
(format "Filter proposition's object index ~a is larger than argument length ~a"
(syntax-e #'i) (length doms))
#:attr prop (-not-filter (parse-type #'t) (syntax-e #'i) (attribute pe.pe)))
(pattern ((~datum !) t:expr (~describe "@" (~datum @)) pe:path-elem ... i:id)
#:attr prop (-not-filter (parse-type #'t) #'i (attribute pe.pe)))
(pattern ((~literal and) p:prop ...)
(pattern ((~literal and) (~var p (prop doms)) ...)
#:attr prop (apply -and (attribute p.prop)))
(pattern ((~literal or) p:prop ...)
(pattern ((~literal or) (~var p (prop doms)) ...)
#:attr prop (apply -or (attribute p.prop)))
(pattern ((~literal implies) p1:prop p2:prop)
(pattern ((~literal implies) (~var p1 (prop doms)) (~var p2 (prop doms)))
#:attr prop (-imp (attribute p1.prop) (attribute p2.prop))))
(define-syntax-class object
@ -137,10 +144,10 @@
(pattern e:expr
#:attr object -no-obj))
(define-splicing-syntax-class full-latent
(define-splicing-syntax-class (full-latent doms)
#:description "latent propositions and object"
(pattern (~seq (~optional (~seq #:+ p+:prop ...))
(~optional (~seq #:- p-:prop ...))
(pattern (~seq (~optional (~seq #:+ (~var p+ (prop doms)) ...+))
(~optional (~seq #:- (~var p- (prop doms)) ...+))
(~optional (~seq #:object o:object)))
#:attr positive (if (attribute p+.prop)
(apply -and (attribute p+.prop))
@ -286,17 +293,18 @@
(list (make-arr
doms
(parse-type (syntax/loc stx (rest-dom ...)))))))]
[(dom ... (~and kw t:->) rng : latent:full-latent)
[(dom (~and kw t:->) rng : latent:simple-latent-filter)
(add-disappeared-use #'kw)
;; use parse-type instead of parse-values-type because we need to add the filters from the pred-ty
(make-pred-ty (list (parse-type #'dom)) (parse-type #'rng) (attribute latent.type) 0 (attribute latent.path))]
[(dom ... (~and kw t:->) rng
: ~! (~var latent (full-latent (syntax->list #'(dom ...)))))
(add-disappeared-use #'kw)
;; use parse-type instead of parse-values-type because we need to add the filters from the pred-ty
(->* (parse-types #'(dom ...))
(parse-type #'rng)
: (-FS (attribute latent.positive) (attribute latent.negative))
: (attribute latent.object))]
[(dom (~and kw t:->) rng : ~! latent:simple-latent-filter)
(add-disappeared-use #'kw)
;; use parse-type instead of parse-values-type because we need to add the filters from the pred-ty
(make-pred-ty (list (parse-type #'dom)) (parse-type #'rng) (attribute latent.type) 0 (attribute latent.path))]
[(dom:non-keyword-ty ... rest:non-keyword-ty ddd:star kws:keyword-tys ... (~and kw t:->) rng)
(add-disappeared-use #'kw)
(make-Function

View File

@ -0,0 +1,16 @@
#;
(exn-pred #rx"Filter proposition's object index 3 is larger than argument length 1")
#lang typed/racket
;; This test ensures that a filter object like '3' is
;; invalid when the function type only has 1 argument.
(ann (λ (x)
(define f
(ann (λ (y) (exact-integer? x))
(Any -> Boolean : #:+ (Integer @ 3) #:- (! Integer @ x))))
(if (f 'dummy)
(add1 x)
2))
(Any -> Integer))