Add explicit -Null abbreviation.

Also clean up many use cases of -pair and (-val null) with -lst*.

original commit: 722c4fd075dc65792860f7f8e172c96106578a64
This commit is contained in:
Eric Dobson 2014-05-08 09:21:12 -07:00
parent fddc956333
commit 5054402414
19 changed files with 88 additions and 98 deletions

View File

@ -215,8 +215,8 @@
[range (cl->* (-> (Un -Zero -NegInt) (-val '()))
(-> -One (-pair -One (-val '())))
[range (cl->* (-> (Un -Zero -NegInt) -Null)
(-> -One (-lst* -One))
(-> -Byte (-lst -Byte))
(-> -Index (-lst -Index))
(-> -Fixnum (-lst -Fixnum))

View File

@ -274,7 +274,7 @@
(-> -Char (apply Un (map -val
'(lu ll lt lm lo mn mc me nd nl no ps pe pi pf pd
pc po sc sm sk so zs zp zl cc cf cs co cn))))]
[make-known-char-range-list (-> (-lst (-Tuple (list -PosInt -PosInt B))))]
[make-known-char-range-list (-> (-lst (-lst* -PosInt -PosInt B)))]
[char-upcase (-> -Char -Char)]
[char-downcase (-> -Char -Char)]
@ -504,12 +504,12 @@
[(a (-lst a)) (-lst a)]))]
#;[*list? (make-pred-ty (-lst Univ))]
[null? (make-pred-ty (-val null))]
[null (-val null)]
[null? (make-pred-ty -Null)]
[null -Null]
[cons? (make-pred-ty (-pair Univ Univ))]
[pair? (make-pred-ty (-pair Univ Univ))]
[empty? (make-pred-ty (-val null))]
[empty (-val null)]
[empty? (make-pred-ty -Null)]
[empty -Null]
[ormap (-polydots (a c b) (->... (list (->... (list a) (b b) c) (-lst a)) ((-lst b) b) (Un c (-val #f))))]
[andmap (-polydots (a c d b) (cl->*
@ -611,9 +611,9 @@
#:after-last (-lst b) #f
. ->key . (-lst (Un a b))))]
[last-pair (-poly (a) ((-mu x (Un a (-val '()) (-pair a x)))
[last-pair (-poly (a) ((-mu x (Un a -Null (-pair a x)))
. -> .
(Un (-pair a a) (-pair a (-val '())))))]
(Un (-pair a a) (-lst* a))))]
[takef
(-poly (a b)
(cl->*
@ -843,14 +843,14 @@
(-> (-seq a) (-seq b) (-seq c) (-seq a b c))))]
[in-values-sequence
(-poly (a b c)
(cl->* (-> (-seq a) (-seq (-pair a (-val null))))
(-> (-seq a b) (-seq (-pair a (-pair b (-val null)))))
(-> (-seq a b c) (-seq (-pair a (-pair b (-pair c (-val null))))))))]
(cl->* (-> (-seq a) (-seq (-lst* a)))
(-> (-seq a b) (-seq (-lst* a b)))
(-> (-seq a b c) (-seq (-lst* a b c)))))]
[in-values*-sequence
(-poly (a b c)
(cl->* (-> (-seq a) (-seq a))
(-> (-seq a b) (-seq (-pair a (-pair b (-val null)))))
(-> (-seq a b c) (-seq (-pair a (-pair b (-pair c (-val null))))))))]
(-> (-seq a b) (-seq (-lst* a b)))
(-> (-seq a b c) (-seq (-lst* a b c)))))]
[stop-before (-poly (a) ((-seq a) (a . -> . Univ) . -> . (-seq a)))]
[stop-after (-poly (a) ((-seq a) (a . -> . Univ) . -> . (-seq a)))]
[make-do-sequence (-poly (a b) ((-> (-values (list (a . -> . b)
@ -933,10 +933,10 @@
[kernel:apply (-poly (a b) (((list) a . ->* . b) (-lst a) . -> . b))]
[time-apply
(-polydots (b a) (cl->*
(-> (-> b) (-val '()) (-values (list (-pair b (-val '())) -Nat -Nat -Nat)))
(-> (-> b) -Null (-values (list (-lst* b) -Nat -Nat -Nat)))
(-> (->... '() (a a) b)
(make-ListDots a 'a)
(-values (list (-pair b (-val '())) -Nat -Nat -Nat)))))]
(-values (list (-lst* b) -Nat -Nat -Nat)))))]
;; Section 4.17.3 (racket/function)
[identity (-poly (a) (->acc (list a) a null))]
@ -1337,12 +1337,12 @@
[A Any-Syntax]
[S (-Syntax Univ)]
[ctxt (-opt S)]
[srclist (-Tuple (list
Univ
(-opt -Integer)
(-opt -Integer)
(-opt -Integer)
(-opt -Integer)))]
[srclist (-lst*
Univ
(-opt -Integer)
(-opt -Integer)
(-opt -Integer)
(-opt -Integer))]
[srcvec (make-HeterogeneousVector (list
Univ
(-opt -Integer)
@ -2114,32 +2114,29 @@
[module-compiled-imports (-> -Compiled-Module-Expression
(-lst (-pair (-opt -Integer)
(-lst -Module-Path-Index))))]
[module-compiled-exports
(-> -Compiled-Module-Expression
(-values
(list
(-lst (-pair (-opt -Integer)
(-lst (-pair -Symbol
(-pair
(-lst
(Un -Module-Path-Index
(-pair -Module-Path-Index
(-pair (-opt -Integer)
(-pair -Symbol
(-pair (-opt -Integer)
(-val null)))))))
(-val null))))))
(-lst (-pair (-opt -Integer)
(-lst (-pair -Symbol
(-pair
(-lst
(Un -Module-Path-Index
(-pair -Module-Path-Index
(-pair (-opt -Integer)
(-pair -Symbol
(-pair (-opt -Integer)
(-val null)))))))
(-val null)))))))))]
(-lst (-pair (-opt -Integer)
(-lst (-lst*
-Symbol
(-lst (Un -Module-Path-Index
(-lst*
-Module-Path-Index
(-opt -Integer)
-Symbol
(-opt -Integer))))))))
(-lst (-pair (-opt -Integer)
(-lst (-lst*
-Symbol
(-lst (Un -Module-Path-Index
(-lst*
-Module-Path-Index
(-opt -Integer)
-Symbol
(-opt -Integer)))))))))))]
[module-compiled-language-info
(-> -Compiled-Module-Expression
(-opt (make-HeterogeneousVector (list -Module-Path -Symbol Univ))))]
@ -2437,7 +2434,7 @@
[tcp-accept-evt
(-> -TCP-Listener
(-evt (-pair -Input-Port (-pair -Output-Port (-val '())))))]
(-evt (-lst* -Input-Port -Output-Port)))]
[tcp-abandon-port (-Port . -> . -Void)]
[tcp-addresses (cl->*
@ -2475,7 +2472,7 @@
(-evt -Void))]
[udp-receive!-evt
(->opt -UDP-Socket -Bytes [-Nat -Nat]
(-evt (-pair -Nat (-pair -String (-pair -Nat (-val null))))))]
(-evt (-lst* -Nat -String -Nat)))]
[udp-addresses
(cl->*

View File

@ -43,7 +43,7 @@
[(make-template-identifier 'qq-append 'racket/private/qq-and-or)
(-poly (a b)
(cl->*
(-> (-lst a) (-val '()) (-lst a))
(-> (-lst a) -Null (-lst a))
(-> (-lst a) (-lst b) (-lst (Un a b)))))]
;; make-sequence
[(make-template-identifier 'make-sequence 'racket/private/for)
@ -193,26 +193,18 @@
;; finite approximation of the type
;; (-> ... 2 args ... (List Pathlike ..._n) -> (List Path ..._n))
(cl->* (-> -Variable-Reference (Un (-> -Path) (-> -Void))
(-pair (Un -Pathlike
(-pair (-val 'lib) (-pair -Pathlike (-lst -Pathlike))))
(-val null))
(-pair -Path (-val null)))
(-lst* (Un -Pathlike (-lst* (-val 'lib) -Pathlike #:tail (-lst -Pathlike))))
(-lst* -Path))
;; this case is for `define-runtime-module-path-index`
(-> -Variable-Reference (Un (-> -Path) (-> -Void))
(-pair (-pair (-val 'module)
(-pair -Module-Path
(-pair -Variable-Reference (-val null))))
(-val null))
(-pair -Module-Path-Index (-val null)))
(-lst* (-lst* (-val 'module) -Module-Path -Variable-Reference))
(-lst* -Module-Path-Index))
(-> -Variable-Reference (Un (-> -Path) (-> -Void))
(-pair -Pathlike (-pair -Pathlike (-val null)))
(-pair -Path (-pair -Path (-val null))))
(-lst* -Pathlike -Pathlike)
(-lst* -Path -Path))
(-> -Variable-Reference (Un (-> -Path) (-> -Void))
(-pair -Pathlike (-pair -Pathlike (-val null)))
(-pair -Path (-pair -Path (-val null))))
(-> -Variable-Reference (Un (-> -Path) (-> -Void))
(-pair -Pathlike (-pair -Pathlike (-pair -Pathlike (-val null))))
(-pair -Path (-pair -Path (-pair -Path (-val null))))))]
(-lst* -Pathlike -Pathlike -Pathlike)
(-lst* -Path -Path -Path)))]
[(make-template-identifier 'extract-module-file 'racket/private/this-expression-source-directory)
(-> (-Syntax Univ) -Path)]
;; for `define-runtime-module-path`

View File

@ -172,9 +172,9 @@
[Setof (-poly (e) (make-Set e))]
[Evtof (-poly (r) (-evt r))]
[Continuation-Mark-Set -Cont-Mark-Set]
[False (-val #f)]
[True (-val #t)]
[Null (-val null)]
[False -False]
[True -True]
[Null -Null]
[Nothing (Un)]
[Futureof (-poly (a) (-future a))]
[Pairof (-poly (a b) (-pair a b))]

View File

@ -532,7 +532,7 @@
;; To check that mutable pair is a sequence we check that the cdr is
;; both an mutable list and a sequence
[((MPair: t1 t2) (Sequence: (list t*)))
(% cset-meet (cg t1 t*) (cg t2 T) (cg t2 (Un (-val null) (make-MPairTop))))]
(% cset-meet (cg t1 t*) (cg t2 T) (cg t2 (Un -Null (make-MPairTop))))]
[((List: ts) (Sequence: (list t*)))
(% cset-meet* (for/list/fail ([t (in-list ts)])
(cg t t*)))]

View File

@ -98,7 +98,7 @@
(match expected
[(tc-result1: (and t (Listof: _))) t]
[_ #f])
(generalize (-val '())))])
(generalize -Null))])
(define-values (fun-results body-results)
(tc/rec-lambda/check args body lp (cons acc-ty ts) expected))
(add-typeof-expr lam fun-results)

View File

@ -84,7 +84,7 @@
[drest (make-ListDots (car drest) (cdr drest))]
;; the function has no rest argument,
;; but provides all the necessary fixed arguments
[else (-val '())]))))
[else -Null]))))
(failure))]
[(tc-result1: (PolyDots: (and vars (list fixed-vars ... dotted-var))
(Function: (list (arr: doms rngs rests drests (list (Keyword: _ _ #f) ...)) ..1))))

View File

@ -86,7 +86,7 @@
[i:byte-regexp -Byte-Regexp]
[i:pregexp -PRegexp]
[i:regexp -Regexp]
[(~and i ()) (-val '())]
[() -Null]
[(i . r)
(match (and expected (resolve (restrict expected (-pair Univ Univ) 'orig)))
[(Pair: a-ty d-ty)

View File

@ -69,7 +69,7 @@
(define (-opt t) (Un (-val #f) t))
(define (-Tuple l)
(foldr -pair (-val '()) l))
(-Tuple* l -Null))
(define (-Tuple* l b)
(foldr -pair b l))
@ -155,7 +155,7 @@
(define -Syntax make-Syntax)
(define/decl In-Syntax
(-mu e
(Un (-val null) -Boolean -Symbol -String -Keyword -Char -Number
(Un -Null -Boolean -Symbol -String -Keyword -Char -Number
(make-Vector (-Syntax e))
(make-Box (-Syntax e))
(make-Listof (-Syntax e))
@ -163,7 +163,7 @@
(define/decl Any-Syntax (-Syntax In-Syntax))
(define (-Sexpof t)
(-mu sexp
(Un (-val '())
(Un -Null
-Number -Boolean -Symbol -String -Keyword -Char
(-pair sexp sexp)
(make-Vector sexp)

View File

@ -48,8 +48,9 @@
;; Char type and List type (needed because of how sequences are checked in subtype)
(define/decl -Char (make-Base 'Char #'char? char? #f))
(define (make-Listof elem) (-mu list-rec (simple-Un (-val null) (make-Pair elem list-rec))))
(define (make-MListof elem) (-mu list-rec (simple-Un (-val null) (make-MPair elem list-rec))))
(define/decl -Null (-val null))
(define (make-Listof elem) (-mu list-rec (simple-Un -Null (make-Pair elem list-rec))))
(define (make-MListof elem) (-mu list-rec (simple-Un -Null (make-MPair elem list-rec))))
;; Needed for evt checking in subtype.rkt
(define/decl -Symbol (make-Base 'Symbol #'symbol? symbol? #f))
@ -60,7 +61,7 @@
;; -lst* Type is needed by substitute for ListDots
(define -pair make-Pair)
(define (-lst* #:tail [tail (-val null)] . args)
(define (-lst* #:tail [tail -Null] . args)
(for/fold ([tl tail]) ([a (in-list (reverse args))]) (-pair a tl)))
;; Simple union type constructor, does not check for overlaps

View File

@ -301,7 +301,7 @@
[((MPair: t1 t2) (Sequence: (list t*)))
(subtype-seq A0
(subtype* t1 t*)
(subtype* t2 (simple-Un (-val null) (make-MPairTop)))
(subtype* t2 (simple-Un -Null (make-MPairTop)))
(subtype* t2 t))]
;; Note: this next case previously used the List: match expander, but
;; using that would cause an infinite loop in certain cases

View File

@ -100,7 +100,7 @@
(Un (-val #f) -Pathlike)
(Un (-val #f) -String)
(-lst (one-of/c 'packages 'enter-packages 'common))
(-lst (-pair -String (-pair -String (-val null))))]
(-lst (-lst* -String -String))]
#:dialog-mixin (Un) #f
(Un (-val #f) -Path))]
[get-file-list
@ -112,7 +112,7 @@
(Un (-val #f) -Pathlike)
(Un (-val #f) -String)
(-lst (one-of/c 'packages 'enter-packages 'common))
(-lst (-pair -String (-pair -String (-val null))))]
(-lst (-lst* -String -String))]
#:dialog-mixin (Un) #f
(Un (-val #f) (-lst -Path)))]
[put-file
@ -124,7 +124,7 @@
(Un (-val #f) -Pathlike)
(Un (-val #f) -String)
(-lst (one-of/c 'packages 'enter-packages 'common))
(-lst (-pair -String (-pair -String (-val null))))]
(-lst (-lst* -String -String))]
#:dialog-mixin (Un) #f
(Un (-val #f) -Path))]
[get-directory
@ -226,7 +226,7 @@
(make-Instance (parse-type #'Frame%))
(make-Instance (parse-type #'Dialog%)))
(Un (make-Instance (parse-type #'Font%)) (-val #f))
(-val null)]
-Null]
(Un (-val #f) (make-Instance (parse-type #'Font%))))]
[can-get-page-setup-from-user? (-> -Boolean)]
;; 4.2 Eventspaces

View File

@ -7,7 +7,7 @@
(Un (-lst type) (-Syntax (-lst type)))))
(type-environment
[stx-null? (make-pred-ty (Un (-val '()) (-Syntax (-val '()))))]
[stx-null? (make-pred-ty (Un -Null (-Syntax -Null)))]
[stx-pair? (make-pred-ty (Un (-pair Univ Univ) (-Syntax (-pair Univ Univ))))]
[stx-list? (make-pred-ty (-stx-list Univ))]
[stx->list (-poly (a)

View File

@ -122,8 +122,8 @@
;(infer-t (make-ListDots -Symbol 'b) (-pair -Symbol (-lst -Symbol)) #:indices '(b))
[i2-t (-v a) N ('a N)]
[i2-t (-pair (-v a) (-v a)) (-pair N (Un N B)) ('a (Un N B))]
[i2-t (-lst (-v a)) (-pair N (-pair N (-val null))) ('a N)]
[i2-t (-lst (-v a)) (-pair N (-pair B (-val null))) ('a (Un N B))]
[i2-t (-lst (-v a)) (-lst* N N) ('a N)]
[i2-t (-lst (-v a)) (-lst* N B) ('a (Un N B))]
[i2-t Univ (Un N B)]
[i2-t ((-v a) . -> . (-v b)) (-> N N) ('b N) ('a (Un))]

View File

@ -137,11 +137,11 @@
[tc-e (in-cycle '(a b) '(z y)) (-seq (one-of/c 'a 'b 'z 'y))]
[tc-e (in-parallel '(a b) '(z y)) (-seq (one-of/c 'a 'b) (one-of/c 'z 'y))]
[tc-e (in-values-sequence (in-parallel '(a b) '(z y)))
(-seq (-pair (one-of/c 'a 'b) (-pair (one-of/c 'z 'y) (-val null))))]
(-seq (-lst* (one-of/c 'a 'b) (one-of/c 'z 'y)))]
[tc-e (in-values-sequence '(a b c))
(-seq (-pair (one-of/c 'a 'b 'c) (-val null)))]
(-seq (-lst* (one-of/c 'a 'b 'c)))]
[tc-e (in-values*-sequence (in-parallel '(a b) '(z y)))
(-seq (-pair (one-of/c 'a 'b) (-pair (one-of/c 'z 'y) (-val null))))]
(-seq (-lst* (one-of/c 'a 'b) (one-of/c 'z 'y)))]
[tc-e (in-values*-sequence '(a b c))
(-seq (one-of/c 'a 'b 'c))]
))

View File

@ -67,6 +67,6 @@
(t/fail (-poly (a) (-lst a)) #:typed-side #f)
(t/sc (-mu a (-lst a)))
(t/sc (-mu a (-box a)))
(t/sc (-mu sexp (Un (-val '()) -Symbol (-pair sexp sexp) (-vec sexp) (-box sexp))))
(t/sc (-mu sexp (Un -Null -Symbol (-pair sexp sexp) (-vec sexp) (-box sexp))))
(t/sc (-mu a (-> a a)))
(t/sc (-seq -Symbol))))

View File

@ -36,9 +36,9 @@
(-Symbol Univ)
(-Void Univ)
[-Number -Number]
[(Un (-pair Univ (-lst Univ)) (-val '())) (-lst Univ)]
[(-pair -Number (-pair -Number (-pair (-val 'foo) (-val '())))) (-lst Univ)]
[(-pair -Number (-pair -Number (-pair (-val 'foo) (-val '())))) (-lst (Un -Number -Symbol))]
[(Un (-pair Univ (-lst Univ)) -Null) (-lst Univ)]
[(-lst* -Number -Number (-val 'foo)) (-lst Univ)]
[(-lst* -Number -Number (-val 'foo)) (-lst (Un -Number -Symbol))]
[(-pair (-val 6) (-val 6)) (-pair -Number -Number)]
[(-val 6) (-val 6)]
;; unions
@ -55,7 +55,7 @@
[(-mu x (Un -Number (make-Listof x))) (-mu x (Un -Number -Symbol (make-Listof x)))]
[(-mu x (Un -Number (make-Listof x))) (-mu y (Un -Number -Symbol (make-Listof y)))]
;; a hard one
[(-mu x (Un -Number (-pair x (-pair -Symbol (-pair x (-val null)))))) -Sexp]
[(-mu x (Un -Number (-lst* x -Symbol x))) -Sexp]
[t1 (unfold t1)]
[(unfold t1) t1]
;; simple function types

View File

@ -44,7 +44,7 @@
(check-prints-as? (-lst -Nat) "(Listof Nonnegative-Integer)")
(check-prints-as? (make-App (-poly (a) (-lst a)) (list -Nat) #'foo)
"(Listof Nonnegative-Integer)")
(check-prints-as? (make-Mu 'x (Un (-val '()) (-pair -Nat (make-F 'x))))
(check-prints-as? (make-Mu 'x (Un -Null (-pair -Nat (make-F 'x))))
"(Listof Nonnegative-Integer)")
(check-prints-as? (-lst* -String -Symbol) "(List String Symbol)")
(check-prints-as? -Custodian "Custodian")

View File

@ -524,7 +524,7 @@
[tc-e/t (if #f 'a 3) -PosByte]
[tc-e/t (if #f #f #t) (t:Un (-val #t))]
[tc-e (when #f 3) -Void]
[tc-e/t '() (-val '())]
[tc-e/t '() -Null]
[tc-e/t (let: ([x : (Listof Number) '(1)])
(cond [(pair? x) 1]
[(null? x) 1]))
@ -656,7 +656,7 @@
-Number]
[tc-e null #:ret (-path (-val null) #'null)]
[tc-e null #:ret (-path -Null #'null)]
[tc-e (let* ([sym 'squarf]
[x (if (= 1 2) 3 sym)])
@ -1021,7 +1021,7 @@
(-polydots (a) ((list -String) (-Number a) . ->... . -Number))]
[tc-e/t (let ([f (plambda: (a ...) [w : a ... a] w)])
(f 1 "hello" #\c))
(-pair -One (-pair -String (-pair -Char (-val null))))]
(-lst* -One -String -Char)]
;; instantiating non-dotted terms
[tc-e/t (inst (plambda: (a) ([x : a]) x) Integer)
(make-Function (list (make-arr* (list -Integer) -Integer
@ -1145,7 +1145,7 @@
(-Number -Number -Number . t:-> . -Number)]
[tc-e (assq 'foo #{'((a b) (foo bar)) :: (Listof (List Symbol Symbol))})
(t:Un (-val #f) (-pair -Symbol (-pair -Symbol (-val null))))]
(t:Un (-val #f) (-lst* -Symbol -Symbol))]
[tc-e/t (ann (lambda (x) x) (All (a) (a -> a)))
(-poly (a) (a . t:-> . a))]
@ -2975,7 +2975,7 @@
(tc-l #:foo (-val '#:foo))
(tc-l #f (-val #f))
(tc-l #"foo" -Bytes)
[tc-l () (-val null)]
[tc-l () -Null]
[tc-l (3 . 4) (-pair -PosByte -PosByte)]
[tc-l #hash() (make-Hashtable Univ Univ)]
[tc-l #hash((1 . 2) (3 . 4)) (make-Hashtable -Integer -Integer)]