Add subtyping for Parameters.

Closes PR11992. This required moving more stuff in to base-abbrev so that it could be used in subtype.
2013-02-17 08:47:31 -08:00 · 2013-02-17 08:47:31 -08:00 · ddb8e7f807
commit ddb8e7f807
parent 0b87c999b3
4 changed files with 162 additions and 143 deletions
--- a/collects/tests/typed-racket/unit-tests/subtype-tests.rkt
+++ b/collects/tests/typed-racket/unit-tests/subtype-tests.rkt
@ -154,6 +154,11 @@
   [(-pair -String (-lst -String)) (-seq -String)]
   [FAIL (-pair -String (-lst -Symbol)) (-seq -String)]
   [FAIL (-pair -String (-vec -String)) (-seq -String)]
+
+   [(-Param -Byte -Byte) (-Param (-val 0) -Int)]
+   [FAIL (-Param -Byte -Byte) (-Param -Int -Int)]
+   [(-Param -String -Symbol) (cl->* (-> -Symbol) (-> -String -Void))]
+
   ))

 (define-go
--- a/collects/typed-racket/types/abbrev.rkt
+++ b/collects/typed-racket/types/abbrev.rkt
@ -2,11 +2,10 @@

 (require "../utils/utils.rkt")

-(require (rename-in (rep type-rep object-rep filter-rep rep-utils) [make-Base make-Base*])
+(require (rename-in (rep type-rep object-rep rep-utils) [make-Base make-Base*])
         (utils tc-utils)
         "base-abbrev.rkt" "match-expanders.rkt"
         (types union numeric-tower)
-         (env mvar-env)
         racket/list
         racket/match
         racket/function
@ -17,7 +16,6 @@
         racket/lazy-require
         (except-in racket/contract/base ->* -> one-of/c)
         (prefix-in c: racket/contract/base)
-         (for-syntax racket/base syntax/parse racket/list)
         (for-template racket/base racket/contract/base racket/promise racket/tcp racket/flonum racket/udp '#%place)
         racket/pretty racket/udp
         ;; for base type predicates
@ -46,7 +44,6 @@
 (define -set make-Set)
 (define -vec make-Vector)
 (define -future make-Future)
-(define -val make-Value)
 (define (-seq . args) (make-Sequence args))
 (define (one-of/c . args)
  (apply Un (map -val args)))
@ -69,9 +66,6 @@



-(define/cond-contract (-result t [f -no-filter] [o -no-obj])
-  (c:->* (Type/c) (FilterSet? Object?) Result?)
-  (make-Result t f o))

 ;; convenient constructor for Values
 ;; (wraps arg types with Result)
@ -97,7 +91,6 @@

 (define -Boolean (Un (-val #t) (-val #f)))
 (define -Symbol (make-Base 'Symbol #'symbol? symbol? #'-Symbol))
-(define -Void (make-Base 'Void #'void? void? #'-Void))
 (define -Undefined
  (make-Base 'Undefined
             #'(lambda (x) (equal? (letrec ([y y]) y) x)) ; initial value of letrec bindings
@ -275,20 +268,7 @@



-
-(define -top (make-Top))
-(define -bot (make-Bot))
-(define -no-filter (make-FilterSet -top -top))
-(define -no-obj (make-Empty))
-
-
-(define/cond-contract (-FS + -)
-      (c:-> Filter/c Filter/c FilterSet?)
-      (match* (+ -)
-             [((Bot:) _) (make-FilterSet -bot -top)]
-             [(_ (Bot:)) (make-FilterSet -top -bot)]
-             [(+ -) (make-FilterSet + -)]))
-
+;; Paths
 (define -car (make-CarPE))
 (define -cdr (make-CdrPE))
 (define -syntax-e (make-SyntaxPE))
@ -316,130 +296,10 @@

 (define top-func (make-Function (list (make-top-arr))))

-(define/cond-contract (make-arr* dom rng
-                                 #:rest [rest #f] #:drest [drest #f] #:kws [kws null]
-                                 #:filters [filters -no-filter] #:object [obj -no-obj])
-  (c:->* ((listof Type/c) (or/c SomeValues/c Type/c))
-         (#:rest (or/c #f Type/c)
-          #:drest (or/c #f (cons/c Type/c symbol?))
-          #:kws (listof Keyword?)
-          #:filters FilterSet?
-          #:object Object?)
-         arr?)
-  (make-arr dom (if (Type/c? rng)
-                    (make-Values (list (-result rng filters obj)))
-                    rng)
-            rest drest (sort #:key Keyword-kw kws keyword<?)))
-
-(define-syntax (->* stx)
-  (define-syntax-class c
-    (pattern x:id #:fail-unless (eq? ': (syntax-e #'x)) #f))
-  (syntax-parse stx
-    [(_ dom rng)
-     #'(make-Function (list (make-arr* dom rng)))]
-    [(_ dom rst rng)
-     #'(make-Function (list (make-arr* dom rng #:rest rst)))]
-    [(_ dom rng :c filters)
-     #'(make-Function (list (make-arr* dom rng #:filters filters)))]
-    [(_ dom rng _:c filters _:c object)
-     #'(make-Function (list (make-arr* dom rng #:filters filters #:object object)))]
-    [(_ dom rst rng _:c filters)
-     #'(make-Function (list (make-arr* dom rng #:rest rst #:filters filters)))]
-    [(_ dom rst rng _:c filters : object)
-     #'(make-Function (list (make-arr* dom rng #:rest rst #:filters filters #:object object)))]))
-
-(define-syntax (-> stx)
-  (define-syntax-class c
-    (pattern x:id #:fail-unless (eq? ': (syntax-e #'x)) #f))
-  (syntax-parse stx
-    [(_ dom ... rng _:c filters _:c objects)
-     #'(->* (list dom ...) rng : filters : objects)]
-    [(_ dom ... rng :c filters)
-     #'(->* (list dom ...) rng : filters)]
-    [(_ dom ... rng)
-     #'(->* (list dom ...) rng)]))
-
-(define-syntax ->...
-  (syntax-rules (:)
-    [(_ dom rng)
-     (->* dom rng)]
-    [(_ dom (dty dbound) rng)
-     (make-Function (list (make-arr* dom rng #:drest (cons dty 'dbound))))]
-    [(_ dom rng : filters)
-     (->* dom rng : filters)]
-    [(_ dom (dty dbound) rng : filters)
-     (make-Function (list (make-arr* dom rng #:drest (cons dty 'dbound) #:filters filters)))]))
-
-(define (->acc dom rng path)
-  (make-Function (list (make-arr* dom rng
-                                  #:filters (-FS (-not-filter (-val #f) 0 path)
-                                                 (-filter (-val #f) 0 path))
-                                  #:object (make-Path path 0)))))
-
-(define (cl->* . args)
-  (define (funty-arities f)
-    (match f
-      [(Function: as) as]))
-  (make-Function (apply append (map funty-arities args))))
-
-(define-syntax cl->
-  (syntax-parser
-   [(_ [(dom ...) rng] ...)
-    #'(cl->* (dom ... . -> . rng) ...)]))
-
-(define-syntax (->key stx)
-  (syntax-parse stx
-                [(_ ty:expr ... (~seq k:keyword kty:expr opt:boolean) ... rng)
-                 #'(make-Function
-                    (list
-                     (make-arr* (list ty ...)
-                                rng
-                                #:kws (sort #:key (match-lambda [(Keyword: kw _ _) kw])
-                                            (list (make-Keyword 'k kty opt) ...)
-                                            keyword<?))))]))
-
-(define-syntax (->optkey stx)
-  (syntax-parse stx
-                [(_ ty:expr ... [oty:expr ...] (~seq k:keyword kty:expr opt:boolean) ... rng)
-                 (let ([l (syntax->list #'(oty ...))])
-                   (with-syntax ([((extra ...) ...)
-                                  (for/list ([i (in-range (add1 (length l)))])
-                                    (take l i))])
-                   #'(make-Function
-                      (list
-                       (make-arr* (list ty ... extra ...)
-                                  rng
-                                  #:kws (sort #:key (match-lambda [(Keyword: kw _ _) kw])
-                                              (list (make-Keyword 'k kty opt) ...)
-                                              keyword<?))
-                       ...))))]))
-
-(define (make-arr-dots dom rng dty dbound)
-  (make-arr* dom rng #:drest (cons dty dbound)))

 (define (-struct name parent flds [proc #f] [poly #f] [pred #'dummy])
  (make-Struct name parent flds proc poly pred))

-(define/cond-contract (-filter t i [p null])
-     (c:->* (Type/c name-ref/c) ((listof PathElem?)) Filter/c)
-     (if (or (type-equal? Univ t) (and (identifier? i) (is-var-mutated? i)))
-         -top
-         (make-TypeFilter t p i)))
-
-(define/cond-contract (-not-filter t i [p null])
-     (c:->* (Type/c name-ref/c) ((listof PathElem?)) Filter/c)
-     (if (or (type-equal? -Bottom t) (and (identifier? i) (is-var-mutated? i)))
-         -top
-         (make-NotTypeFilter t p i)))
-
-(define (-filter-at t o)
-  (match o
-    [(Path: p i) (-filter t i p)]
-    [_ -top]))
-(define (-not-filter-at t o)
-  (match o
-    [(Path: p i) (-not-filter t i p)]
-    [_ -top]))

 (define (asym-pred dom rng filter)
  (make-Function (list (make-arr* (list dom) rng #:filters filter))))
--- a/collects/typed-racket/types/base-abbrev.rkt
+++ b/collects/typed-racket/types/base-abbrev.rkt
@ -3,8 +3,10 @@

 (require "../utils/utils.rkt")

-(require (rep type-rep)
+(require (rep type-rep filter-rep object-rep)
+         (env mvar-env)
         racket/match racket/list
+         (for-syntax racket/base syntax/parse racket/list)
         (for-template racket/base))

 (provide (all-defined-out)
@ -19,9 +21,14 @@
 ;return type of functions
 (define ManyUniv (make-AnyValues))

+;;Convinient constructors
+(define -val make-Value)
+
 ;; Char type and List type (needed because of how sequences are checked in subtype)
 (define -Char (make-Base 'Char #'char? char? #'-Char #f))
 (define (make-Listof elem) (-mu list-rec (simple-Un (make-Value null) (make-Pair elem list-rec))))
+;; Void is needed for Params
+(define -Void (make-Base 'Void #'void? void? #'-Void #f))


 ;; Simple union type, does not check for overlaps
@ -63,3 +70,146 @@
    [(_ var ty)
     (let ([var (-v var)])
       (make-Mu 'var ty))]))
+
+;;Results
+(define/cond-contract (-result t [f -no-filter] [o -no-obj])
+  (c:->* (Type/c) (FilterSet? Object?) Result?)
+  (make-Result t f o))
+
+;;Filters
+(define -top (make-Top))
+(define -bot (make-Bot))
+(define -no-filter (make-FilterSet -top -top))
+(define -no-obj (make-Empty))
+
+
+(define/cond-contract (-FS + -)
+      (c:-> Filter/c Filter/c FilterSet?)
+      (match* (+ -)
+             [((Bot:) _) (make-FilterSet -bot -top)]
+             [(_ (Bot:)) (make-FilterSet -top -bot)]
+             [(+ -) (make-FilterSet + -)]))
+
+(define/cond-contract (-filter t i [p null])
+     (c:->* (Type/c name-ref/c) ((listof PathElem?)) Filter/c)
+     (if (or (type-equal? Univ t) (and (identifier? i) (is-var-mutated? i)))
+         -top
+         (make-TypeFilter t p i)))
+
+(define/cond-contract (-not-filter t i [p null])
+     (c:->* (Type/c name-ref/c) ((listof PathElem?)) Filter/c)
+     (if (or (type-equal? -Bottom t) (and (identifier? i) (is-var-mutated? i)))
+         -top
+         (make-NotTypeFilter t p i)))
+
+(define (-filter-at t o)
+  (match o
+    [(Path: p i) (-filter t i p)]
+    [_ -top]))
+(define (-not-filter-at t o)
+  (match o
+    [(Path: p i) (-not-filter t i p)]
+    [_ -top]))
+
+
+;; Function types
+(define/cond-contract (make-arr* dom rng
+                                 #:rest [rest #f] #:drest [drest #f] #:kws [kws null]
+                                 #:filters [filters -no-filter] #:object [obj -no-obj])
+  (c:->* ((listof Type/c) (or/c SomeValues/c Type/c))
+         (#:rest (or/c #f Type/c)
+          #:drest (or/c #f (cons/c Type/c symbol?))
+          #:kws (listof Keyword?)
+          #:filters FilterSet?
+          #:object Object?)
+         arr?)
+  (make-arr dom (if (Type/c? rng)
+                    (make-Values (list (-result rng filters obj)))
+                    rng)
+            rest drest (sort #:key Keyword-kw kws keyword<?)))
+
+(define-syntax (->* stx)
+  (define-syntax-class c
+    (pattern x:id #:fail-unless (eq? ': (syntax-e #'x)) #f))
+  (syntax-parse stx
+    [(_ dom rng)
+     #'(make-Function (list (make-arr* dom rng)))]
+    [(_ dom rst rng)
+     #'(make-Function (list (make-arr* dom rng #:rest rst)))]
+    [(_ dom rng :c filters)
+     #'(make-Function (list (make-arr* dom rng #:filters filters)))]
+    [(_ dom rng _:c filters _:c object)
+     #'(make-Function (list (make-arr* dom rng #:filters filters #:object object)))]
+    [(_ dom rst rng _:c filters)
+     #'(make-Function (list (make-arr* dom rng #:rest rst #:filters filters)))]
+    [(_ dom rst rng _:c filters : object)
+     #'(make-Function (list (make-arr* dom rng #:rest rst #:filters filters #:object object)))]))
+
+(define-syntax (-> stx)
+  (define-syntax-class c
+    (pattern x:id #:fail-unless (eq? ': (syntax-e #'x)) #f))
+  (syntax-parse stx
+    [(_ dom ... rng _:c filters _:c objects)
+     #'(->* (list dom ...) rng : filters : objects)]
+    [(_ dom ... rng :c filters)
+     #'(->* (list dom ...) rng : filters)]
+    [(_ dom ... rng)
+     #'(->* (list dom ...) rng)]))
+
+(define-syntax ->...
+  (syntax-rules (:)
+    [(_ dom rng)
+     (->* dom rng)]
+    [(_ dom (dty dbound) rng)
+     (make-Function (list (make-arr* dom rng #:drest (cons dty 'dbound))))]
+    [(_ dom rng : filters)
+     (->* dom rng : filters)]
+    [(_ dom (dty dbound) rng : filters)
+     (make-Function (list (make-arr* dom rng #:drest (cons dty 'dbound) #:filters filters)))]))
+
+(define (->acc dom rng path)
+  (make-Function (list (make-arr* dom rng
+                                  #:filters (-FS (-not-filter (-val #f) 0 path)
+                                                 (-filter (-val #f) 0 path))
+                                  #:object (make-Path path 0)))))
+
+(define (cl->* . args)
+  (define (funty-arities f)
+    (match f
+      [(Function: as) as]))
+  (make-Function (apply append (map funty-arities args))))
+
+(define-syntax cl->
+  (syntax-parser
+   [(_ [(dom ...) rng] ...)
+    #'(cl->* (dom ... . -> . rng) ...)]))
+
+(define-syntax (->key stx)
+  (syntax-parse stx
+                [(_ ty:expr ... (~seq k:keyword kty:expr opt:boolean) ... rng)
+                 #'(make-Function
+                    (list
+                     (make-arr* (list ty ...)
+                                rng
+                                #:kws (sort #:key (match-lambda [(Keyword: kw _ _) kw])
+                                            (list (make-Keyword 'k kty opt) ...)
+                                            keyword<?))))]))
+
+(define-syntax (->optkey stx)
+  (syntax-parse stx
+                [(_ ty:expr ... [oty:expr ...] (~seq k:keyword kty:expr opt:boolean) ... rng)
+                 (let ([l (syntax->list #'(oty ...))])
+                   (with-syntax ([((extra ...) ...)
+                                  (for/list ([i (in-range (add1 (length l)))])
+                                    (take l i))])
+                   #'(make-Function
+                      (list
+                       (make-arr* (list ty ... extra ...)
+                                  rng
+                                  #:kws (sort #:key (match-lambda [(Keyword: kw _ _) kw])
+                                              (list (make-Keyword 'k kty opt) ...)
+                                              keyword<?))
+                       ...))))]))
+
+(define (make-arr-dots dom rng dty dbound)
+  (make-arr* dom rng #:drest (cons dty dbound)))
--- a/collects/typed-racket/types/subtype.rkt
+++ b/collects/typed-racket/types/subtype.rkt
@ -440,6 +440,10 @@
               (subtype* A0 t t*)]
              [((Future: t) (Future: t*))
               (subtype* A0 t t*)]
+              [((Param: s-in s-out) (Param: t-in t-out))
+               (subtype* (subtype* A0 t-in s-in) s-out t-out)]
+              [((Param: in out) t)
+               (subtype* A0 (cl->* (-> out) (-> in -Void)) t)]
              [((Instance: t) (Instance: t*))
               (subtype* A0 t t*)]
              [((Class: '() '() (list (and s  (list names  meths )) ...))