From 56fd9e63219b87d0fddbfd5d9fdb97010acd13f3 Mon Sep 17 00:00:00 2001 From: Eric Dobson Date: Sun, 15 Jul 2012 20:37:26 -0700 Subject: [PATCH] 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. --- .../unit-tests/type-annotation-test.rkt | 2 +- collects/typed-racket/rep/type-rep.rkt | 19 +-- collects/typed-racket/types/abbrev.rkt | 132 ++++++++---------- collects/typed-racket/types/base-abbrev.rkt | 63 +++++++++ collects/typed-racket/types/convenience.rkt | 55 +------- collects/typed-racket/types/numeric-tower.rkt | 20 ++- collects/typed-racket/types/substitute.rkt | 6 +- collects/typed-racket/types/subtype.rkt | 2 +- collects/typed-racket/types/union.rkt | 64 +++------ 9 files changed, 182 insertions(+), 181 deletions(-) create mode 100644 collects/typed-racket/types/base-abbrev.rkt diff --git a/collects/tests/typed-racket/unit-tests/type-annotation-test.rkt b/collects/tests/typed-racket/unit-tests/type-annotation-test.rkt index ad921a2013..1ba6d69426 100644 --- a/collects/tests/typed-racket/unit-tests/type-annotation-test.rkt +++ b/collects/tests/typed-racket/unit-tests/type-annotation-test.rkt @@ -3,7 +3,7 @@ (for-syntax scheme/base) typed-racket/private/type-annotation typed-racket/private/parse-type - (types abbrev numeric-tower utils) + (types convenience utils) (env type-env-structs init-envs) (utils tc-utils) (rep type-rep filter-rep object-rep) diff --git a/collects/typed-racket/rep/type-rep.rkt b/collects/typed-racket/rep/type-rep.rkt index db3f910443..68cdebde50 100644 --- a/collects/typed-racket/rep/type-rep.rkt +++ b/collects/typed-racket/rep/type-rep.rkt @@ -2,11 +2,15 @@ (require "../utils/utils.rkt") (require (utils tc-utils) - "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/contract + unstable/lazy-require (for-syntax racket/base syntax/parse)) +;; Ugly hack - should use units +(lazy-require ("../types/union.rkt" (Un))) + (define name-table (make-weak-hasheq)) (define Type/c? @@ -358,7 +362,7 @@ e))]) sorted?))))]) [#: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]) (if (null? ts) res (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] ;; removes duplicate types from a SORTED list (define/cond-contract (remove-dups types) diff --git a/collects/typed-racket/types/abbrev.rkt b/collects/typed-racket/types/abbrev.rkt index 64c15eaa32..1c9754b9e4 100644 --- a/collects/typed-racket/types/abbrev.rkt +++ b/collects/typed-racket/types/abbrev.rkt @@ -4,6 +4,8 @@ (require (rename-in (rep type-rep object-rep filter-rep rep-utils) [make-Base make-Base*]) (utils tc-utils) + "base-abbrev.rkt" + (types union numeric-tower) racket/list racket/match racket/function @@ -13,17 +15,16 @@ unstable/function racket/udp unstable/lazy-require - (except-in racket/contract/base ->* ->) + (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) + (for-template racket/base racket/contract/base racket/promise racket/tcp racket/flonum) racket/pretty racket/udp ;; for base type predicates 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] [make-MListof -mlst])) @@ -37,7 +38,6 @@ (define -App make-App) (define -pair make-Pair) (define -mpair make-MPair) -(define -val make-Value) (define -Param make-Param) (define -box make-Box) (define -channel make-Channel) @@ -45,26 +45,17 @@ (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))) +(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 (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]) @@ -114,15 +82,10 @@ ;; 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 -Boolean (*Un (-val #t) (-val #f))) +(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 @@ -142,16 +105,16 @@ #'pregexp? pregexp? #'-PRegexp)) -(define -Regexp (*Un -PRegexp -Base-Regexp)) +(define -Regexp (Un -PRegexp -Base-Regexp)) (define -Byte-Base-Regexp (make-Base 'Byte-Regexp #'(and/c byte-regexp? (not/c byte-pregexp?)) (conjoin byte-regexp? (negate byte-pregexp?)) #'-Byte-Regexp)) (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 -Char (make-Base 'Char #'char? char? #'-Char)) (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 -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)) @@ -171,7 +141,7 @@ #'(and/c compiled-expression? (not/c compiled-module-expression?)) (conjoin compiled-expression? (negate compiled-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 -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)) @@ -188,29 +158,48 @@ (define -FlVector (make-Base 'FlVector #'flvector? flvector? #'-FlVector)) (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 -Promise make-promise-ty) (define -HashTop (make-HashtableTop)) (define -VectorTop (make-VectorTop)) -(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) +(define -Port (Un -Output-Port -Input-Port)) -(define -Port (*Un -Output-Port -Input-Port)) - -(define -SomeSystemPath (*Un -Path -OtherSystemPath)) -(define -Pathlike (*Un -String -Path)) -(define -SomeSystemPathlike (*Un -String -SomeSystemPath)) -(define -Pathlike* (*Un -String -Path (-val 'up) (-val 'same))) -(define -SomeSystemPathlike* (*Un -String -SomeSystemPath(-val 'up) (-val 'same))) -(define -PathConventionType (*Un (-val 'unix) (-val 'windows))) +(define -SomeSystemPath (Un -Path -OtherSystemPath)) +(define -Pathlike (Un -String -Path)) +(define -SomeSystemPathlike (Un -String -SomeSystemPath)) +(define -Pathlike* (Un -String -Path (-val 'up) (-val 'same))) +(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 -Log-Receiver (make-Base 'LogReceiver #'log-receiver? log-receiver? #'-Log-Receiver)) +(define -Log-Level (one-of/c 'fatal 'error 'warning 'info 'debug)) (define -Place @@ -269,7 +259,7 @@ (define -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 (make-Base 'Will-Executor #'will-executor? will-executor? #'-Will-Executor)) diff --git a/collects/typed-racket/types/base-abbrev.rkt b/collects/typed-racket/types/base-abbrev.rkt new file mode 100644 index 0000000000..15993e7b58 --- /dev/null +++ b/collects/typed-racket/types/base-abbrev.rkt @@ -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)))))]))) + diff --git a/collects/typed-racket/types/convenience.rkt b/collects/typed-racket/types/convenience.rkt index 3a1585df7f..5420f11ccb 100644 --- a/collects/typed-racket/types/convenience.rkt +++ b/collects/typed-racket/types/convenience.rkt @@ -1,59 +1,16 @@ #lang racket/base (require "../utils/utils.rkt" - (rep type-rep filter-rep object-rep rep-utils) - (utils tc-utils) - (only-in racket/contract current-blame-format) - "abbrev.rkt" "numeric-tower.rkt" - unstable/lazy-require - (for-template racket/base)) + (rep type-rep filter-rep object-rep) + (types union) + "base-abbrev.rkt" "abbrev.rkt" "numeric-tower.rkt") -(lazy-require ["union.rkt" (Un)]) - -(provide (all-defined-out) - (all-from-out "abbrev.rkt" "numeric-tower.rkt") +(provide (all-from-out "abbrev.rkt" "base-abbrev.rkt" "numeric-tower.rkt") + ;; TODO change the uses of this export to Un + (rename-out (Un *Un)) ;; these should all eventually go away make-Name make-ValuesDots make-Function (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)) diff --git a/collects/typed-racket/types/numeric-tower.rkt b/collects/typed-racket/types/numeric-tower.rkt index 45051b9047..654e1a4040 100644 --- a/collects/typed-racket/types/numeric-tower.rkt +++ b/collects/typed-racket/types/numeric-tower.rkt @@ -2,8 +2,9 @@ (require "../utils/utils.rkt") -(require (types abbrev numeric-predicates) +(require (types numeric-predicates) (rename-in (rep type-rep) [make-Base make-Base*]) + racket/match racket/function unstable/function (for-template racket/base racket/contract racket/flonum (types numeric-predicates))) @@ -24,6 +25,19 @@ (define (make-Base name contract predicate marshaled) (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= n 0))) ;; Singletons -(define -Zero (-val 0)) ; exact -(define -One (-val 1)) +(define -Zero (make-Value 0)) ; exact +(define -One (make-Value 1)) ;; Integers (define -Byte>1 (make-Base 'Byte-Larger-Than-One ; unsigned diff --git a/collects/typed-racket/types/substitute.rkt b/collects/typed-racket/types/substitute.rkt index 18e3e7cd5c..05a3e7b8c4 100644 --- a/collects/typed-racket/types/substitute.rkt +++ b/collects/typed-racket/types/substitute.rkt @@ -6,7 +6,9 @@ (only-in (rep free-variance) combine-frees) (env index-env tvar-env) racket/match - racket/contract) + racket/contract + unstable/lazy-require) +(lazy-require ("union.rkt" (Un))) (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) @@ -31,7 +33,7 @@ ;; 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?) (define (sb t) (substitute image name t #:Un Un)) (if (hash-ref (free-vars* target) name #f) diff --git a/collects/typed-racket/types/subtype.rkt b/collects/typed-racket/types/subtype.rkt index 361c08ed29..5f51a5b7e1 100644 --- a/collects/typed-racket/types/subtype.rkt +++ b/collects/typed-racket/types/subtype.rkt @@ -2,7 +2,7 @@ (require "../utils/utils.rkt" (rep type-rep filter-rep object-rep rep-utils) (utils tc-utils) - (types utils resolve abbrev numeric-tower substitute) + (types utils resolve base-abbrev numeric-tower substitute) (env type-name-env) (only-in (infer infer-dummy) unify) racket/match unstable/match diff --git a/collects/typed-racket/types/union.rkt b/collects/typed-racket/types/union.rkt index 9cc399c694..9d78661bb7 100644 --- a/collects/typed-racket/types/union.rkt +++ b/collects/typed-racket/types/union.rkt @@ -1,60 +1,42 @@ #lang racket/base (require "../utils/utils.rkt" - (rep type-rep rep-utils) - (utils tc-utils) + (rep type-rep) (prefix-in c: (contract-req)) - (types utils subtype) - racket/match) - + (types subtype) + racket/match + racket/list) (provide/cond-contract [Un (() #:rest (c:listof Type/c) . c:->* . Type/c)]) -(define (make-union* set) - (match set +;; List[Type] -> Type +;; Argument types should not overlap or be union types +(define (make-union* types) + (match types [(list t) t] - [_ (make-Union set)])) + [_ (make-Union types)])) -(define empty-union (make-Union null)) - -(define (remove-subtypes ts) - (let loop ([ts* ts] [result '()]) - (cond [(null? ts*) (reverse result)] - [(ormap (lambda (t) (subtype (car ts*) t)) result) (loop (cdr ts*) result)] - [else (loop (cdr ts*) (cons (car ts*) result))]))) +;; a is a Type (not a union type) +;; b is a List[Type] (non overlapping, non Union-types) +;; The output is a non overlapping list of non Union types. +(define (merge a b) + (define b* (make-union* b)) + (cond + [(subtype a b*) b] + [(subtype b* a) (list a)] + [else (cons a b)])) +;; Type -> List[Type] (define (flat t) (match t [(Union: es) es] - [(Values: (list (Result: (Union: es) _ _))) es] - [(Values: (list (Result: t _ _))) (list t)] [_ (list t)])) ;; Union constructor ;; Normalizes representation by sorting types. -(define Un - (case-lambda - [() empty-union] - [(t) t] - [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 Type +;; The input types can overlap and be union types +(define (Un . args) + (make-union* (foldr merge '() (remove-dups (sort (append-map flat args) type