Allow arbitrary filter specification in function types.

Allow (A -> B -> C) for curried function types.

collects/tests/typed-scheme/run.rkt

@@ -36,7 +36,7 @@
        (printf "Skipping Typed Racket tests.\n")]
       [(when (the-tests)
          (unless (= 0 ((exec) (the-tests)))
-           (eprintf "Typed Racket Tests did not pass.")))
+           (eprintf "Typed Racket Tests did not pass.\n")))
        (when (opt?)
          (parameterize ([current-command-line-arguments #()])
            (dynamic-require '(file "optimizer/run.rkt") #f))

collects/tests/typed-scheme/succeed/multi-arr-parse.rkt

@@ -1,6 +1,4 @@
-#;
-(exn-pred #rx".*once in a form.*")
 #lang typed/scheme
 
 (: foo : (Integer -> Integer -> Integer))
-(define foo 1)
+(define ((foo x) y) 1)

collects/tests/typed-scheme/unit-tests/parse-type-tests.rkt

@@ -5,7 +5,7 @@
 	 (env type-alias-env type-env-structs tvar-env type-name-env init-envs)
 	 (rep type-rep)
 	 (rename-in (types comparison subtype union utils convenience)
-                    [Un t:Un] [-> t:->])
+                    [Un t:Un] [-> t:->] [->* t:->*])
          (private base-types base-types-extra colon)
          (for-template (private base-types base-types-extra base-env colon))
          (private parse-type)
@@ -83,7 +83,7 @@
    ;; requires transformer time stuff that doesn't work
    #;[(Refinement even?) (make-Refinement #'even?)]
    [(Number Number Number Boolean -> Number) (N N N B . t:-> . N)]
-   [(Number Number Number * -> Boolean) ((list N N) N . ->* . B)]
+   [(Number Number Number * -> Boolean) ((list N N) N . t:->* . B)]
    ;[((. Number) -> Number) (->* (list) N N)] ;; not legal syntax
    [(U Number Boolean) (t:Un N B)]
    [(U Number Boolean Number) (t:Un N B)]
@@ -111,6 +111,12 @@
     (-polydots (a) ((list) [a a] . ->... . N))]
    
    [(Any -> Boolean : Number) (make-pred-ty -Number)]
+   [(Any -> Boolean : #:+ (Number @ 0) #:- (! Number @ 0))
+    (make-pred-ty -Number)]
+   [(Any -> Boolean : #:+ (! Number @ 0) #:- (Number @ 0))
+    (t:->* (list Univ) -Boolean : (-FS (-not-filter -Number 0 null) (-filter -Number 0 null)))]
+   [(Number -> Number -> Number)
+    (t:-> -Number (t:-> -Number -Number))]
    [(Integer -> (All (X) (X -> X)))
     (t:-> -Integer (-poly (x) (t:-> x x)))]
    

collects/typed-scheme/private/parse-type.rkt

@@ -2,7 +2,7 @@
 
 (require "../utils/utils.rkt"
 	 (except-in (rep type-rep) make-arr)
-         (rename-in (types convenience union utils) [make-arr* make-arr])
+         (rename-in (types convenience union utils printer filter-ops) [make-arr* make-arr])
          (utils tc-utils stxclass-util)
          syntax/stx (prefix-in c: scheme/contract)
          syntax/parse
@@ -22,6 +22,7 @@
 
 (provide star ddd/bound)
 (define enable-mu-parsing (make-parameter #t))
+(print-complex-filters? #t)
 
 (define ((parse/id p) loc datum)
   #;(printf "parse-type/id id : ~a\n ty: ~a\n" (syntax-object->datum loc) (syntax-object->datum stx))
@@ -103,7 +104,7 @@
   (pattern cdr
            #:attr pe (make-CdrPE)))
 
-(define-splicing-syntax-class latent-filter
+(define-splicing-syntax-class simple-latent-filter
   #:description "latent filter"  
   (pattern (~seq t:expr (~describe "@" (~datum @)) pe:path-elem ...)
            #:attr type (parse-type #'t)
@@ -112,6 +113,41 @@
            #:attr type (parse-type #'t)
            #:attr path '()))
 
+(define-syntax-class prop
+  #:attributes (prop)
+  (pattern (~literal Top) #:attr prop -top)
+  (pattern (~literal Bot) #:attr prop -bot)
+  (pattern (t:expr (~describe "@" (~datum @)) pe:path-elem ... i:nat)
+           #:attr prop (-filter (parse-type #'t) (syntax-e #'i) (attribute pe.pe)))
+  (pattern ((~datum !) t:expr (~describe "@" (~datum @)) pe:path-elem ... i:nat)
+           #:attr prop (-not-filter (parse-type #'t) (syntax-e #'i) (attribute pe.pe)))
+  (pattern ((~literal and) p:prop ...)
+           #:attr prop (apply -and (attribute p.prop)))
+  (pattern ((~literal or) p:prop ...)
+           #:attr prop (apply -or (attribute p.prop)))
+  (pattern ((~literal implies) p1:prop p2:prop)
+           #:attr prop (-imp (attribute p1.prop) (attribute p2.prop))))
+
+(define-syntax-class object
+  #:attributes (object)
+  (pattern e:expr
+           #:attr object -no-obj))
+
+(define-splicing-syntax-class full-latent
+  #:description "latent propositions and object"
+  (pattern (~seq (~optional (~seq #:+ p+:prop ...))
+                 (~optional (~seq #:- p-:prop ...))
+                 (~optional (~seq #:object o:object)))
+           #:attr positive (if (attribute p+.prop)
+                               (apply -and (attribute p+.prop))
+                               -top)
+           #:attr negative (if (attribute p-.prop)
+                               (apply -and (attribute p-.prop))
+                               -top)
+           #:attr object (if (attribute o.object)
+                             (attribute o.object)
+                             -no-obj)))
+
 (define (parse-type stx)    
   (parameterize ([current-orig-stx stx])    
     (syntax-parse
@@ -210,14 +246,25 @@
       [((~and kw t:Parameter) t1 t2)      
        (add-type-name-reference #'kw)
        (-Param (parse-type #'t1) (parse-type #'t2))]
-      ;; function types
+      ;; curried function notation
-      ;; handle this error first:
+      [((~and dom:non-keyword-ty (~not t:->)) ...
-      [((~or dom (~between (~and kw t:->) 2 +inf.0)) ...)
+        (~and kw t:->) 
-       (for ([k (syntax->list #'(kw ...))]) (add-type-name-reference k))
+        (~and (~seq rest-dom ...) (~seq (~or _ (~between t:-> 1 +inf.0)) ...)))
-       (tc-error/stx (syntax->list #'(kw ...))
+       (add-type-name-reference #'kw)
-                     "The -> type constructor may be used only once in a form")
+       (let ([doms (for/list ([d (syntax->list #'(dom ...))])
-       Err]
+                    (parse-type d))])
-      [(dom (~and kw t:->) rng : ~! latent:latent-filter)
+         (make-Function
+          (list (make-arr
+                 doms
+                 (parse-type (syntax/loc stx (rest-dom ...)))))))]
+      [(dom ... (~and kw t:->) rng : latent:full-latent)
+       (add-type-name-reference #'kw)
+       ;; use parse-type instead of parse-values-type because we need to add the filters from the pred-ty
+       (->* (map parse-type (syntax->list #'(dom ...)))
+            (parse-type #'rng)
+            : (-FS (attribute latent.positive) (attribute latent.negative))
+            : (attribute latent.object))]
+      [(dom (~and kw t:->) rng : ~! latent:simple-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) (attribute latent.type) 0 (attribute latent.path))]

collects/typed-scheme/typecheck/tc-metafunctions.rkt

@@ -9,15 +9,7 @@
          racket/contract racket/match unstable/match
          (for-syntax racket/base))
 
-;; this implements the sequence invariant described on the first page relating to Bot
+(provide abstract-results)
-
-(define (combine l1 l2)
-  (match* (l1 l2) 
-          [(_ (Bot:)) (-FS -top -bot)]
-          [((Bot:) _) (-FS -bot -top)]
-          [(_ _) (-FS l1 l2)]))
-
-(provide combine abstract-results)
 
 
 (d/c (abstract-results results arg-names)
@@ -51,8 +43,8 @@
   (-> (listof identifier?) (listof name-ref/c) FilterSet/c FilterSet/c)
   (match fs
     [(FilterSet: f+ f-)
-     (combine (abo ids keys f+) (abo ids keys f-))]
+     (-FS (abo ids keys f+) (abo ids keys f-))]
-    [(NoFilter:) (combine -top -top)]))
+    [(NoFilter:) (-FS -top -top)]))
 
 (d/c (abo xs idxs f)
   ((listof identifier?) (listof name-ref/c) Filter/c . -> . Filter/c)
@@ -76,7 +68,7 @@
 (define (merge-filter-sets fs)
   (match fs
     [(list (FilterSet: f+ f-) ...)
-     (make-FilterSet (make-AndFilter f+) (make-AndFilter f-))]))
+     (-FS (make-AndFilter f+) (make-AndFilter f-))]))
 
 (define (tc-results->values tc)
   (match tc

collects/typed-scheme/typecheck/tc-subst.rkt

@@ -33,8 +33,8 @@
            [_ f]))
   (match fs
     [(FilterSet: f+ f-)
-     (combine (subst-filter (add-extra-filter f+) k o polarity)
+     (-FS (subst-filter (add-extra-filter f+) k o polarity)
-	      (subst-filter (add-extra-filter f-) k o polarity))]
+          (subst-filter (add-extra-filter f-) k o polarity))]
     [_ (-FS -top -top)]))
 
 (d/c (subst-type t k o polarity)

collects/typed-scheme/types/filter-ops.rkt

@@ -96,6 +96,13 @@
            (loop (cdr props) others)]
           [p (loop (cdr props) (cons p others))]))))
 
+
+(define (-imp p1 p2)
+  (match* (p1 p2)
+    [((Bot:) _) -top]
+    [((Top:) _) p2]
+    [(_ _) (make-ImpFilter p1 p2)]))
+
 (define (-or . args)
   (define mk
     (case-lambda [() -bot]