From 12be4e80ab99869a140a247ae25db92ac94c5a6b Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Thu, 14 Jan 2010 23:17:56 +0000
Subject: [PATCH] Syntax for predicates with non-empty paths

svn: r17660

original commit: 5e1b355e325a8a910911caaa25069b51eea7cd7b
---
 .../tests/typed-scheme/succeed/parse-path.ss  |  4 ++++
 collects/typed-scheme/private/parse-type.ss   | 23 +++++++++++++++++--
 collects/typed-scheme/types/abbrev.ss         |  5 +++-
 collects/typed-scheme/types/printer.ss        | 11 ++++++---
 4 files changed, 37 insertions(+), 6 deletions(-)
 create mode 100644 collects/tests/typed-scheme/succeed/parse-path.ss

diff --git a/collects/tests/typed-scheme/succeed/parse-path.ss b/collects/tests/typed-scheme/succeed/parse-path.ss
new file mode 100644
index 00000000..ea36af8c
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/parse-path.ss
@@ -0,0 +1,4 @@
+#lang typed/scheme
+
+(: f ((Pair Any Any) -> Boolean : Number @ car))
+(define f (lambda: ([x : (Pair Any Any)]) (number? (car x))))
\ No newline at end of file
diff --git a/collects/typed-scheme/private/parse-type.ss b/collects/typed-scheme/private/parse-type.ss
index c85c5bb2..a552956a 100644
--- a/collects/typed-scheme/private/parse-type.ss
+++ b/collects/typed-scheme/private/parse-type.ss
@@ -67,6 +67,7 @@
        (add-type-name-reference #'kw)
        (parameterize ([current-tvars (extend-env vars tvars (current-tvars))])
          (make-Poly vars (parse-type #'t))))]
+    [(t:All (_:id ...) _ _ _ ...) (tc-error "All: too many forms in body of All type")]
     [(t:All . rest) (tc-error "All: bad syntax")]))
 
 (define-splicing-syntax-class keyword-tys
@@ -75,6 +76,24 @@
   (pattern (~seq [k:keyword t:expr])
            #:attr Keyword (make-Keyword (syntax-e #'k) (parse-type #'t) #f)))
 
+(define-syntax-class path-elem
+  #:description "path element"
+  #:literals (car cdr)
+  (pattern car
+           #:attr pe (make-CarPE))
+  (pattern cdr
+           #:attr pe (make-CdrPE)))
+
+(define-splicing-syntax-class latent-filter
+  #:description "latent filter"  
+  (pattern (~seq t:expr @:id pe:path-elem ...)
+           #:fail-unless (eq? (syntax-e #'@) '@) "expected @"
+           #:attr type (parse-type #'t)
+           #:attr path (attribute pe.pe))
+  (pattern t:expr
+           #:attr type (parse-type #'t)
+           #:attr path '()))
+
 (define (parse-type stx)    
   (parameterize ([current-orig-stx stx])    
     (syntax-parse
@@ -171,10 +190,10 @@
        (add-type-name-reference #'kw)
        (-Param (parse-type #'t1) (parse-type #'t2))]
       ;; function types
-      [(dom (~and kw t:->) rng : pred-ty)
+      [(dom (~and kw t:->) rng : ~! latent:latent-filter)
        (add-type-name-reference #'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) (parse-type #'pred-ty))]
+       (make-pred-ty (list (parse-type #'dom)) (parse-type #'rng) (attribute latent.type) 0 (attribute latent.path))]
       [(dom:expr ... rest:expr ddd:star kws:keyword-tys ... (~and kw t:->) rng)
        (add-type-name-reference #'kw)
        (make-Function
diff --git a/collects/typed-scheme/types/abbrev.ss b/collects/typed-scheme/types/abbrev.ss
index 8c58bdc6..ca5ca183 100644
--- a/collects/typed-scheme/types/abbrev.ss
+++ b/collects/typed-scheme/types/abbrev.ss
@@ -265,8 +265,11 @@
 (d/c make-pred-ty
   (case-> (c:-> Type/c Type/c)
           (c:-> (listof Type/c) Type/c Type/c Type/c)
-          (c:-> (listof Type/c) Type/c Type/c integer? Type/c))
+          (c:-> (listof Type/c) Type/c Type/c integer? Type/c)
+          (c:-> (listof Type/c) Type/c Type/c integer? (listof PathElem?) Type/c))
   (case-lambda 
+    [(in out t n p)
+     (->* in out : (-LFS (list (-filter t p n)) (list (-not-filter t p n))))]
     [(in out t n)
      (->* in out : (-LFS (list (-filter t null n)) (list (-not-filter t null n))))]
     [(in out t)
diff --git a/collects/typed-scheme/types/printer.ss b/collects/typed-scheme/types/printer.ss
index 8763f202..b81ca892 100644
--- a/collects/typed-scheme/types/printer.ss
+++ b/collects/typed-scheme/types/printer.ss
@@ -43,6 +43,8 @@
                                (fp "LTop")
                                (for ([i els]) (fp " ~a" i)))
                            (fp")")]
+    [(LNotTypeFilter: type path 0) (fp "(! ~a @ ~a)" type path)]
+    [(LTypeFilter: type path 0) (fp "(~a @ ~a)" type path)]
     [(LNotTypeFilter: type path idx) (fp "(! ~a @ ~a ~a)" type path idx)]
     [(LTypeFilter: type path idx) (fp "(~a @ ~a ~a)" type path idx)]
     [(LBot:) (fp "LBot")]
@@ -115,10 +117,13 @@
          [(Values: (list (Result: t (LFilterSet: (list) (list)) (LEmpty:))))
           (fp "-> ~a" t)]
          [(Values: (list (Result: t
-				  (LFilterSet: (list (LTypeFilter: ft '() 0))
-					       (list (LNotTypeFilter: ft '() 0)))
+				  (LFilterSet: (list (LTypeFilter: ft pth 0))
+					       (list (LNotTypeFilter: ft pth 0)))
 				  (LEmpty:)))) 
-          (fp "-> ~a : ~a" t ft)]
+          (if (null? pth)
+              (fp "-> ~a : ~a" t ft)
+              (begin (fp "-> ~a : ~a @" t ft)
+                     (for ([pe pth]) (fp " ~a" pe))))]
          [(Values: (list (Result: t fs (LEmpty:)))) 
           (fp/filter "-> ~a : ~a" t fs)]
          [(Values: (list (Result: t lf lo)))