Rearange type code, so that abbrev.rkt can depend on union.rkt.

Split out base-abbrev.rkt so that subtype is not dependent on abbrev.rkt.
Remove unused code in numeric-tower.rkt so that it is now a dependent of
abbrev.rkt, which allows the body of convenience.rkt to be merged back in.
Remove special casing for union.rkt and extraneous subtyping checks.
Remove union-maker.
This commit is contained in:
Eric Dobson 2012-07-15 20:37:26 -07:00 committed by Sam Tobin-Hochstadt
parent 6dbc054e41
commit 56fd9e6321
9 changed files with 182 additions and 181 deletions

View File

@ -3,7 +3,7 @@
(for-syntax scheme/base) (for-syntax scheme/base)
typed-racket/private/type-annotation typed-racket/private/type-annotation
typed-racket/private/parse-type typed-racket/private/parse-type
(types abbrev numeric-tower utils) (types convenience utils)
(env type-env-structs init-envs) (env type-env-structs init-envs)
(utils tc-utils) (utils tc-utils)
(rep type-rep filter-rep object-rep) (rep type-rep filter-rep object-rep)

View File

@ -5,8 +5,12 @@
"rep-utils.rkt" "object-rep.rkt" "filter-rep.rkt" "free-variance.rkt" "rep-utils.rkt" "object-rep.rkt" "filter-rep.rkt" "free-variance.rkt"
racket/match ;mzlib/etc racket/match ;mzlib/etc
racket/contract racket/contract
unstable/lazy-require
(for-syntax racket/base syntax/parse)) (for-syntax racket/base syntax/parse))
;; Ugly hack - should use units
(lazy-require ("../types/union.rkt" (Un)))
(define name-table (make-weak-hasheq)) (define name-table (make-weak-hasheq))
(define Type/c? (define Type/c?
@ -358,7 +362,7 @@
e))]) e))])
sorted?))))]) sorted?))))])
[#:frees (λ (f) (combine-frees (map f elems)))] [#:frees (λ (f) (combine-frees (map f elems)))]
[#:fold-rhs ((get-union-maker) (map type-rec-id elems))] [#:fold-rhs (apply Un (map type-rec-id elems))]
[#:key (let loop ([res null] [ts elems]) [#:key (let loop ([res null] [ts elems])
(if (null? ts) res (if (null? ts) res
(let ([k (Type-key (car ts))]) (let ([k (Type-key (car ts))])
@ -427,17 +431,6 @@
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Ugly hack - should use units
(define union-maker (box (lambda args (int-err "Union not yet available"))))
(define (set-union-maker! v) (set-box! union-maker v))
(define (get-union-maker) (unbox union-maker))
(provide set-union-maker! get-union-maker)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; remove-dups: List[Type] -> List[Type] ;; remove-dups: List[Type] -> List[Type]
;; removes duplicate types from a SORTED list ;; removes duplicate types from a SORTED list
(define/cond-contract (remove-dups types) (define/cond-contract (remove-dups types)

View File

@ -4,6 +4,8 @@
(require (rename-in (rep type-rep object-rep filter-rep rep-utils) [make-Base make-Base*]) (require (rename-in (rep type-rep object-rep filter-rep rep-utils) [make-Base make-Base*])
(utils tc-utils) (utils tc-utils)
"base-abbrev.rkt"
(types union numeric-tower)
racket/list racket/list
racket/match racket/match
racket/function racket/function
@ -13,7 +15,7 @@
unstable/function unstable/function
racket/udp racket/udp
unstable/lazy-require unstable/lazy-require
(except-in racket/contract/base ->* ->) (except-in racket/contract/base ->* -> one-of/c)
(prefix-in c: racket/contract/base) (prefix-in c: racket/contract/base)
(for-syntax racket/base syntax/parse racket/list) (for-syntax racket/base syntax/parse racket/list)
(for-template racket/base racket/contract/base racket/promise racket/tcp racket/flonum) (for-template racket/base racket/contract/base racket/promise racket/tcp racket/flonum)
@ -21,9 +23,8 @@
;; for base type predicates ;; for base type predicates
racket/promise racket/tcp racket/flonum) racket/promise racket/tcp racket/flonum)
(lazy-require ["resolve.rkt" (resolve)])
(provide (except-out (all-defined-out) Promise make-Base) (provide (except-out (all-defined-out) make-Base)
(rename-out [make-Listof -lst] (rename-out [make-Listof -lst]
[make-MListof -mlst])) [make-MListof -mlst]))
@ -37,7 +38,6 @@
(define -App make-App) (define -App make-App)
(define -pair make-Pair) (define -pair make-Pair)
(define -mpair make-MPair) (define -mpair make-MPair)
(define -val make-Value)
(define -Param make-Param) (define -Param make-Param)
(define -box make-Box) (define -box make-Box)
(define -channel make-Channel) (define -channel make-Channel)
@ -45,26 +45,17 @@
(define -set make-Set) (define -set make-Set)
(define -vec make-Vector) (define -vec make-Vector)
(define -future make-Future) (define -future make-Future)
(define -val make-Value)
(define (-seq . args) (make-Sequence args)) (define (-seq . args) (make-Sequence args))
(define (one-of/c . args)
(apply Un (map -val args)))
(define (-opt t) (Un (-val #f) t))
(define (flat t)
(match t
[(Union: es) es]
[(Values: (list (Result: (Union: es) _ _))) es]
[(Values: (list (Result: t _ _))) (list t)]
[_ (list t)]))
;; TODO make this file depend on union.rkt, and use the real Union constructor.
;; Simple union constructor.
;; Flattens nested unions and sorts types, but does not check for
;; overlapping subtypes.
(define (*Un . args)
(make-Union (remove-dups (sort (apply append (map flat args)) type<?))))
(define (make-Listof elem) (-mu list-rec (*Un (-val null) (-pair elem list-rec)))) (define (make-Listof elem) (-mu list-rec (Un (-val null) (-pair elem list-rec))))
(define (make-MListof elem) (-mu mlist-rec (*Un (-val null) (-mpair elem mlist-rec)))) (define (make-MListof elem) (-mu mlist-rec (Un (-val null) (-mpair elem mlist-rec))))
(define (-lst* #:tail [tail (-val null)] . args) (define (-lst* #:tail [tail (-val null)] . args)
(for/fold ([tl tail]) ([a (reverse args)]) (-pair a tl))) (for/fold ([tl tail]) ([a (reverse args)]) (-pair a tl)))
@ -75,30 +66,7 @@
(define (-Tuple* l b) (define (-Tuple* l b)
(foldr -pair b l)) (foldr -pair b l))
(define (untuple t)
(match (resolve t)
[(Value: '()) null]
[(Pair: a b) (cond [(untuple b) => (lambda (l) (cons a l))]
[else #f])]
[_ #f]))
(define-match-expander Listof:
(lambda (stx)
(syntax-parse stx
[(_ elem-pat (~optional var-pat #:defaults ([var-pat #'var])))
(syntax/loc stx (Mu: var-pat (Union: (list (Value: '()) (Pair: elem-pat (F: var-pat))))))])))
(define-match-expander List:
(lambda (stx)
(syntax-parse stx
[(_ elem-pats)
#'(app untuple (? values elem-pats))])))
(define-match-expander MListof:
(lambda (stx)
(syntax-parse stx
[(_ elem-pat)
#'(Mu: var (Union: (list (Value: '()) (MPair: elem-pat (F: var)))))])))
(define/cond-contract (-result t [f -no-filter] [o -no-obj]) (define/cond-contract (-result t [f -no-filter] [o -no-obj])
@ -114,15 +82,10 @@
;; basic types ;; basic types
(define Promise #f)
(define promise-id #'Promise)
(define make-promise-ty
(lambda (t)
(make-Struct promise-id #f (list (make-fld t #'values #f)) #f #f #'promise? values #'values)))
(define -Listof (-poly (list-elem) (make-Listof list-elem))) (define -Listof (-poly (list-elem) (make-Listof list-elem)))
(define -Boolean (*Un (-val #t) (-val #f))) (define -Boolean (Un (-val #t) (-val #f)))
(define -Symbol (make-Base 'Symbol #'symbol? symbol? #'-Symbol)) (define -Symbol (make-Base 'Symbol #'symbol? symbol? #'-Symbol))
(define -Void (make-Base 'Void #'void? void? #'-Void)) (define -Void (make-Base 'Void #'void? void? #'-Void))
(define -Undefined (define -Undefined
@ -142,16 +105,16 @@
#'pregexp? #'pregexp?
pregexp? pregexp?
#'-PRegexp)) #'-PRegexp))
(define -Regexp (*Un -PRegexp -Base-Regexp)) (define -Regexp (Un -PRegexp -Base-Regexp))
(define -Byte-Base-Regexp (make-Base 'Byte-Regexp (define -Byte-Base-Regexp (make-Base 'Byte-Regexp
#'(and/c byte-regexp? (not/c byte-pregexp?)) #'(and/c byte-regexp? (not/c byte-pregexp?))
(conjoin byte-regexp? (negate byte-pregexp?)) (conjoin byte-regexp? (negate byte-pregexp?))
#'-Byte-Regexp)) #'-Byte-Regexp))
(define -Byte-PRegexp (make-Base 'Byte-PRegexp #'byte-pregexp? byte-pregexp? #'-Byte-PRegexp)) (define -Byte-PRegexp (make-Base 'Byte-PRegexp #'byte-pregexp? byte-pregexp? #'-Byte-PRegexp))
(define -Byte-Regexp (*Un -Byte-Base-Regexp -Byte-PRegexp)) (define -Byte-Regexp (Un -Byte-Base-Regexp -Byte-PRegexp))
(define -Pattern (*Un -Bytes -Regexp -Byte-Regexp -String)) (define -Pattern (Un -Bytes -Regexp -Byte-Regexp -String))
@ -161,8 +124,15 @@
(define -Keyword (make-Base 'Keyword #'keyword? keyword? #'-Keyword)) (define -Keyword (make-Base 'Keyword #'keyword? keyword? #'-Keyword))
(define -Char (make-Base 'Char #'char? char? #'-Char))
(define -Thread (make-Base 'Thread #'thread? thread? #'-Thread)) (define -Thread (make-Base 'Thread #'thread? thread? #'-Thread))
(define -Module-Path (Un -Symbol -String
(-lst* (-val 'quote) -Symbol)
(-lst* (-val 'lib) -String)
(-lst* (-val 'file) -String)
(-pair (-val 'planet)
(Un (-lst* -Symbol)
(-lst* -String)
(-lst* -String (-lst* -String -String #:tail (make-Listof (Un -Nat (-lst* (Un -Nat (one-of/c '= '+ '-)) -Nat)))))))))
(define -Resolved-Module-Path (make-Base 'Resolved-Module-Path #'resolved-module-path? resolved-module-path? #'-Resolved-Module-Path)) (define -Resolved-Module-Path (make-Base 'Resolved-Module-Path #'resolved-module-path? resolved-module-path? #'-Resolved-Module-Path))
(define -Module-Path-Index (make-Base 'Module-Path-Index #'module-path-index? module-path-index? #'-Module-Path-Index)) (define -Module-Path-Index (make-Base 'Module-Path-Index #'module-path-index? module-path-index? #'-Module-Path-Index))
(define -Compiled-Module-Expression (make-Base 'Compiled-Module-Expression #'compiled-module-expression? compiled-module-expression? #'-Compiled-Module-Expression)) (define -Compiled-Module-Expression (make-Base 'Compiled-Module-Expression #'compiled-module-expression? compiled-module-expression? #'-Compiled-Module-Expression))
@ -171,7 +141,7 @@
#'(and/c compiled-expression? (not/c compiled-module-expression?)) #'(and/c compiled-expression? (not/c compiled-module-expression?))
(conjoin compiled-expression? (negate compiled-module-expression?)) (conjoin compiled-expression? (negate compiled-module-expression?))
#'-Compiled-Non-Module-Expression)) #'-Compiled-Non-Module-Expression))
(define -Compiled-Expression (*Un -Compiled-Module-Expression -Compiled-Non-Module-Expression)) (define -Compiled-Expression (Un -Compiled-Module-Expression -Compiled-Non-Module-Expression))
(define -Prompt-Tag (make-Base 'Prompt-Tag #'continuation-prompt-tag? continuation-prompt-tag? #'-Prompt-Tag)) (define -Prompt-Tag (make-Base 'Prompt-Tag #'continuation-prompt-tag? continuation-prompt-tag? #'-Prompt-Tag))
(define -Cont-Mark-Set (make-Base 'Continuation-Mark-Set #'continuation-mark-set? continuation-mark-set? #'-Cont-Mark-Set)) (define -Cont-Mark-Set (make-Base 'Continuation-Mark-Set #'continuation-mark-set? continuation-mark-set? #'-Cont-Mark-Set))
(define -Path (make-Base 'Path #'path? path? #'-Path)) (define -Path (make-Base 'Path #'path? path? #'-Path))
@ -188,29 +158,48 @@
(define -FlVector (make-Base 'FlVector #'flvector? flvector? #'-FlVector)) (define -FlVector (make-Base 'FlVector #'flvector? flvector? #'-FlVector))
(define -Syntax make-Syntax) (define -Syntax make-Syntax)
(define In-Syntax
(-mu e
(Un (-val null) -Boolean -Symbol -String -Keyword -Char -Number
(make-Vector (-Syntax e))
(make-Box (-Syntax e))
(make-Listof (-Syntax e))
(-pair (-Syntax e) (-Syntax e)))))
(define Any-Syntax (-Syntax In-Syntax))
(define (-Sexpof t)
(-mu sexp
(Un (-val '())
-Number -Boolean -Symbol -String -Keyword -Char
(-pair sexp sexp)
(make-Vector sexp)
(make-Box sexp)
t)))
(define -Sexp (-Sexpof (Un)))
(define Syntax-Sexp (-Sexpof Any-Syntax))
(define Ident (-Syntax -Symbol))
(define -HT make-Hashtable) (define -HT make-Hashtable)
(define -Promise make-promise-ty)
(define -HashTop (make-HashtableTop)) (define -HashTop (make-HashtableTop))
(define -VectorTop (make-VectorTop)) (define -VectorTop (make-VectorTop))
(define Univ (make-Univ))
(define Err (make-Error))
;A Type that corresponds to the any contract for the (define -Port (Un -Output-Port -Input-Port))
;return type of functions
;FIXME
;This is not correct as Univ is only a single value.
(define ManyUniv Univ)
(define -Port (*Un -Output-Port -Input-Port)) (define -SomeSystemPath (Un -Path -OtherSystemPath))
(define -Pathlike (Un -String -Path))
(define -SomeSystemPath (*Un -Path -OtherSystemPath)) (define -SomeSystemPathlike (Un -String -SomeSystemPath))
(define -Pathlike (*Un -String -Path)) (define -Pathlike* (Un -String -Path (-val 'up) (-val 'same)))
(define -SomeSystemPathlike (*Un -String -SomeSystemPath)) (define -SomeSystemPathlike* (Un -String -SomeSystemPath(-val 'up) (-val 'same)))
(define -Pathlike* (*Un -String -Path (-val 'up) (-val 'same))) (define -PathConventionType (Un (-val 'unix) (-val 'windows)))
(define -SomeSystemPathlike* (*Un -String -SomeSystemPath(-val 'up) (-val 'same)))
(define -PathConventionType (*Un (-val 'unix) (-val 'windows)))
@ -262,6 +251,7 @@
(define -Logger (make-Base 'Logger #'logger? logger? #'-Logger)) (define -Logger (make-Base 'Logger #'logger? logger? #'-Logger))
(define -Log-Receiver (make-Base 'LogReceiver #'log-receiver? log-receiver? #'-Log-Receiver)) (define -Log-Receiver (make-Base 'LogReceiver #'log-receiver? log-receiver? #'-Log-Receiver))
(define -Log-Level (one-of/c 'fatal 'error 'warning 'info 'debug))
(define -Place (define -Place
@ -269,7 +259,7 @@
(define -Base-Place-Channel (define -Base-Place-Channel
(make-Base 'Base-Place-Channel #'(and/c place-channel? (not/c place?)) (conjoin place-channel? (negate place?)) #'-Base-Place-Channel)) (make-Base 'Base-Place-Channel #'(and/c place-channel? (not/c place?)) (conjoin place-channel? (negate place?)) #'-Base-Place-Channel))
(define -Place-Channel (*Un -Place -Base-Place-Channel)) (define -Place-Channel (Un -Place -Base-Place-Channel))
(define -Will-Executor (define -Will-Executor
(make-Base 'Will-Executor #'will-executor? will-executor? #'-Will-Executor)) (make-Base 'Will-Executor #'will-executor? will-executor? #'-Will-Executor))

View File

@ -0,0 +1,63 @@
#lang racket/base
;; This file is for the abbreviations need to implement union.rkt
(require "../utils/utils.rkt")
(require (rep type-rep)
racket/match
(types resolve)
(for-template racket/base)
(for-syntax racket/base syntax/parse racket/list))
(provide (except-out (all-defined-out) Promise))
;Top and error types
(define Univ (make-Univ))
(define Err (make-Error))
;A Type that corresponds to the any contract for the
;return type of functions
;FIXME
;This is not correct as Univ is only a single value.
(define ManyUniv Univ)
; Promise type
; TODO make this not a struct type, but the same as all other container types
(define Promise #f)
(define promise-id #'Promise)
(define -Promise
(lambda (t)
(make-Struct promise-id #f (list (make-fld t #'values #f)) #f #f #'promise? values #'values)))
;; Char type (needed because of how sequences are checked in subtype)
(define -Char (make-Base 'Char #'char? char? #'-Char #f))
;;List expanders
(define-match-expander Listof:
(lambda (stx)
(syntax-parse stx
[(_ elem-pat (~optional var-pat #:defaults ([var-pat #'var])))
(syntax/loc stx (Mu: var-pat (Union: (list (Value: '()) (Pair: elem-pat (F: var-pat))))))])))
(define-match-expander List:
(lambda (stx)
(syntax-parse stx
[(_ elem-pats)
#'(app untuple (? values elem-pats))])))
(define (untuple t)
(match (resolve t)
[(Value: '()) null]
[(Pair: a b) (cond [(untuple b) => (lambda (l) (cons a l))]
[else #f])]
[_ #f]))
(define-match-expander MListof:
(lambda (stx)
(syntax-parse stx
[(_ elem-pat)
#'(Mu: var (Union: (list (Value: '()) (MPair: elem-pat (F: var)))))])))

View File

@ -1,59 +1,16 @@
#lang racket/base #lang racket/base
(require "../utils/utils.rkt" (require "../utils/utils.rkt"
(rep type-rep filter-rep object-rep rep-utils) (rep type-rep filter-rep object-rep)
(utils tc-utils) (types union)
(only-in racket/contract current-blame-format) "base-abbrev.rkt" "abbrev.rkt" "numeric-tower.rkt")
"abbrev.rkt" "numeric-tower.rkt"
unstable/lazy-require
(for-template racket/base))
(lazy-require ["union.rkt" (Un)]) (provide (all-from-out "abbrev.rkt" "base-abbrev.rkt" "numeric-tower.rkt")
;; TODO change the uses of this export to Un
(provide (all-defined-out) (rename-out (Un *Un))
(all-from-out "abbrev.rkt" "numeric-tower.rkt")
;; these should all eventually go away ;; these should all eventually go away
make-Name make-ValuesDots make-Function make-Name make-ValuesDots make-Function
(rep-out filter-rep object-rep)) (rep-out filter-rep object-rep))
(define (one-of/c . args)
(apply Un (map -val args)))
(define (-opt t) (Un (-val #f) t))
(define In-Syntax
(-mu e
(Un (-val null) -Boolean -Symbol -String -Keyword -Char -Number
(make-Vector (-Syntax e))
(make-Box (-Syntax e))
(-lst (-Syntax e))
(-pair (-Syntax e) (-Syntax e)))))
(define Any-Syntax (-Syntax In-Syntax))
(define (-Sexpof t)
(-mu sexp
(Un (-val '())
-Number -Boolean -Symbol -String -Keyword -Char
(-pair sexp sexp)
(make-Vector sexp)
(make-Box sexp)
t)))
(define -Sexp (-Sexpof (*Un)))
(define Syntax-Sexp (-Sexpof Any-Syntax))
(define Ident (-Syntax -Symbol))
(define -Module-Path (*Un -Symbol -String
(-lst* (-val 'quote) -Symbol)
(-lst* (-val 'lib) -String)
(-lst* (-val 'file) -String)
(-pair (-val 'planet)
(*Un (-lst* -Symbol)
(-lst* -String)
(-lst* -String (-lst* -String -String #:tail (make-Listof (*Un -Nat (-lst* (*Un -Nat (one-of/c '= '+ '-)) -Nat)))))))))
(define -Log-Level (one-of/c 'fatal 'error 'warning 'info 'debug))

View File

@ -2,8 +2,9 @@
(require "../utils/utils.rkt") (require "../utils/utils.rkt")
(require (types abbrev numeric-predicates) (require (types numeric-predicates)
(rename-in (rep type-rep) [make-Base make-Base*]) (rename-in (rep type-rep) [make-Base make-Base*])
racket/match
racket/function racket/function
unstable/function unstable/function
(for-template racket/base racket/contract racket/flonum (types numeric-predicates))) (for-template racket/base racket/contract racket/flonum (types numeric-predicates)))
@ -24,6 +25,19 @@
(define (make-Base name contract predicate marshaled) (define (make-Base name contract predicate marshaled)
(make-Base* name contract predicate marshaled #t)) (make-Base* name contract predicate marshaled #t))
;; Simple union constructor.
;; Flattens nested unions and sorts types, but does not check for
;; overlapping subtypes.
(define-syntax *Un
(syntax-rules ()
[(_ . args) (make-Union (remove-dups (sort (apply append (map flat (list . args))) type<?)))]))
(define (flat t)
(match t
[(Union: es) es]
[_ (list t)]))
;; Numeric hierarchy ;; Numeric hierarchy
;; All built as unions of non-overlapping base types. ;; All built as unions of non-overlapping base types.
@ -50,8 +64,8 @@
(>= n 0))) (>= n 0)))
;; Singletons ;; Singletons
(define -Zero (-val 0)) ; exact (define -Zero (make-Value 0)) ; exact
(define -One (-val 1)) (define -One (make-Value 1))
;; Integers ;; Integers
(define -Byte>1 (make-Base 'Byte-Larger-Than-One ; unsigned (define -Byte>1 (make-Base 'Byte-Larger-Than-One ; unsigned

View File

@ -6,7 +6,9 @@
(only-in (rep free-variance) combine-frees) (only-in (rep free-variance) combine-frees)
(env index-env tvar-env) (env index-env tvar-env)
racket/match racket/match
racket/contract) racket/contract
unstable/lazy-require)
(lazy-require ("union.rkt" (Un)))
(provide subst-all substitute substitute-dots substitute-dotted subst (provide subst-all substitute substitute-dots substitute-dotted subst
(struct-out t-subst) (struct-out i-subst) (struct-out i-subst/starred) (struct-out i-subst/dotted) (struct-out t-subst) (struct-out i-subst) (struct-out i-subst/starred) (struct-out i-subst/dotted)
@ -31,7 +33,7 @@
;; substitute : Type Name Type -> Type ;; substitute : Type Name Type -> Type
(define/cond-contract (substitute image name target #:Un [Un (get-union-maker)]) (define/cond-contract (substitute image name target #:Un [Un (lambda (args) (apply Un args))])
((Type/c symbol? Type?) (#:Un procedure?) . ->* . Type?) ((Type/c symbol? Type?) (#:Un procedure?) . ->* . Type?)
(define (sb t) (substitute image name t #:Un Un)) (define (sb t) (substitute image name t #:Un Un))
(if (hash-ref (free-vars* target) name #f) (if (hash-ref (free-vars* target) name #f)

View File

@ -2,7 +2,7 @@
(require "../utils/utils.rkt" (require "../utils/utils.rkt"
(rep type-rep filter-rep object-rep rep-utils) (rep type-rep filter-rep object-rep rep-utils)
(utils tc-utils) (utils tc-utils)
(types utils resolve abbrev numeric-tower substitute) (types utils resolve base-abbrev numeric-tower substitute)
(env type-name-env) (env type-name-env)
(only-in (infer infer-dummy) unify) (only-in (infer infer-dummy) unify)
racket/match unstable/match racket/match unstable/match

View File

@ -1,60 +1,42 @@
#lang racket/base #lang racket/base
(require "../utils/utils.rkt" (require "../utils/utils.rkt"
(rep type-rep rep-utils) (rep type-rep)
(utils tc-utils)
(prefix-in c: (contract-req)) (prefix-in c: (contract-req))
(types utils subtype) (types subtype)
racket/match) racket/match
racket/list)
(provide/cond-contract (provide/cond-contract
[Un (() #:rest (c:listof Type/c) . c:->* . Type/c)]) [Un (() #:rest (c:listof Type/c) . c:->* . Type/c)])
(define (make-union* set) ;; List[Type] -> Type
(match set ;; Argument types should not overlap or be union types
(define (make-union* types)
(match types
[(list t) t] [(list t) t]
[_ (make-Union set)])) [_ (make-Union types)]))
(define empty-union (make-Union null)) ;; a is a Type (not a union type)
;; b is a List[Type] (non overlapping, non Union-types)
(define (remove-subtypes ts) ;; The output is a non overlapping list of non Union types.
(let loop ([ts* ts] [result '()]) (define (merge a b)
(cond [(null? ts*) (reverse result)] (define b* (make-union* b))
[(ormap (lambda (t) (subtype (car ts*) t)) result) (loop (cdr ts*) result)] (cond
[else (loop (cdr ts*) (cons (car ts*) result))]))) [(subtype a b*) b]
[(subtype b* a) (list a)]
[else (cons a b)]))
;; Type -> List[Type]
(define (flat t) (define (flat t)
(match t (match t
[(Union: es) es] [(Union: es) es]
[(Values: (list (Result: (Union: es) _ _))) es]
[(Values: (list (Result: t _ _))) (list t)]
[_ (list t)])) [_ (list t)]))
;; Union constructor ;; Union constructor
;; Normalizes representation by sorting types. ;; Normalizes representation by sorting types.
(define Un ;; Type * -> Type
(case-lambda ;; The input types can overlap and be union types
[() empty-union] (define (Un . args)
[(t) t] (make-union* (foldr merge '() (remove-dups (sort (append-map flat args) type<?)))))
[args
;; a is a Type (not a union type)
;; b is a List[Type]
(define (union2 a b)
(define b* (make-union* b))
(cond
[(subtype a b*) (list b*)]
[(subtype b* a) (list a)]
[else (cons a b)]))
(let ([types (remove-dups (sort (apply append (map flat args)) type<?))])
(cond
[(null? types) (make-union* null)]
[(null? (cdr types)) (car types)]
;; FIXME: this sort is unneccessary
[else (make-union* (sort (foldr union2 '() (remove-subtypes types)) type<?))]))]))
(define (u-maker args) (apply Un args))
(set-union-maker! u-maker)