Add a field to base types to indicate if they are numeric types or not.

This commit is contained in:
Vincent St-Amour 2011-09-12 16:41:53 -04:00
parent 32b56eb2fa
commit 40456b4fd8
11 changed files with 48 additions and 38 deletions

View File

@ -112,12 +112,12 @@
[(-values (list -Number)) (-values (list Univ))] [(-values (list -Number)) (-values (list Univ))]
[(-poly (b) ((Un (make-Base 'foo #'dummy values #'values) [(-poly (b) ((Un (make-Base 'foo #'dummy values #'values #f)
(-struct #'bar #f (-struct #'bar #f
(list (make-fld -Number #'values #f) (make-fld b #'values #f)) (list (make-fld -Number #'values #f) (make-fld b #'values #f))
#'values)) #'values))
. -> . (-lst b))) . -> . (-lst b)))
((Un (make-Base 'foo #'dummy values #'values) (-struct #'bar #f (list (make-fld -Number #'values #f) (make-fld (-pair -Number (-v a)) #'values #f)) #'values)) ((Un (make-Base 'foo #'dummy values #'values #f) (-struct #'bar #f (list (make-fld -Number #'values #f) (make-fld (-pair -Number (-v a)) #'values #f)) #'values))
. -> . (-lst (-pair -Number (-v a))))] . -> . (-lst (-pair -Number (-v a))))]
[(-poly (b) ((-struct #'bar #f (list (make-fld -Number #'values #f) (make-fld b #'values #f)) #'values) . -> . (-lst b))) [(-poly (b) ((-struct #'bar #f (list (make-fld -Number #'values #f) (make-fld b #'values #f)) #'values) . -> . (-lst b)))
((-struct #'bar #f (list (make-fld -Number #'values #f) (make-fld (-pair -Number (-v a)) #'values #f)) #'values) . -> . (-lst (-pair -Number (-v a))))] ((-struct #'bar #f (list (make-fld -Number #'values #f) (make-fld (-pair -Number (-v a)) #'values #f)) #'values) . -> . (-lst (-pair -Number (-v a))))]

View File

@ -7,7 +7,7 @@
(provide type-equal-tests) (provide type-equal-tests)
(define (-base x) (make-Base x #'dummy values #'values)) (define (-base x) (make-Base x #'dummy values #'values #f))
(define-syntax (te-tests stx) (define-syntax (te-tests stx)

View File

@ -22,7 +22,7 @@
(string->symbol (string-append "make-" (substring (symbol->string sym) 7)))) (string->symbol (string-append "make-" (substring (symbol->string sym) 7))))
(match v (match v
[(Union: elems) `(make-Union (sort (list ,@(map sub elems)) < #:key Type-seq))] [(Union: elems) `(make-Union (sort (list ,@(map sub elems)) < #:key Type-seq))]
[(Base: n cnt pred marshaled) marshaled] [(Base: n cnt pred marshaled _) marshaled]
[(Name: stx) `(make-Name (quote-syntax ,stx))] [(Name: stx) `(make-Name (quote-syntax ,stx))]
[(fld: t acc mut) `(make-fld ,(sub t) (quote-syntax ,acc) ,mut)] [(fld: t acc mut) `(make-fld ,(sub t) (quote-syntax ,acc) ,mut)]
[(Struct: name parent flds proc poly? pred-id cert maker-id) [(Struct: name parent flds proc poly? pred-id cert maker-id)

View File

@ -411,11 +411,11 @@
(cg t t*)))] (cg t t*)))]
[((Vector: t) (Sequence: (list t*))) [((Vector: t) (Sequence: (list t*)))
(cg t t*)] (cg t t*)]
[((Base: 'String _ _ _) (Sequence: (list t*))) [((Base: 'String _ _ _ _) (Sequence: (list t*)))
(cg -Char t*)] (cg -Char t*)]
[((Base: 'Bytes _ _ _) (Sequence: (list t*))) [((Base: 'Bytes _ _ _ _) (Sequence: (list t*)))
(cg -Nat t*)] (cg -Nat t*)]
[((Base: 'Input-Port _ _ _) (Sequence: (list t*))) [((Base: 'Input-Port _ _ _ _) (Sequence: (list t*)))
(cg -Nat t*)] (cg -Nat t*)]
[((Vector: t) (Sequence: (list t*))) [((Vector: t) (Sequence: (list t*)))
(cg t t*)] (cg t t*)]

View File

@ -175,7 +175,7 @@
(inexact-real? (real-part x))))))] (inexact-real? (real-part x))))))]
[(== t:-Number type-equal?) #'(flat-named-contract 'Number number?)] [(== t:-Number type-equal?) #'(flat-named-contract 'Number number?)]
[(Base: sym cnt _ _) #`(flat-named-contract '#,sym (flat-contract-predicate #,cnt))] [(Base: sym cnt _ _ _) #`(flat-named-contract '#,sym (flat-contract-predicate #,cnt))]
[(Refinement: par p? cert) [(Refinement: par p? cert)
#`(and/c #,(t->c par) (flat-contract #,(cert p?)))] #`(and/c #,(t->c par) (flat-contract #,(cert p?)))]
[(Union: elems) [(Union: elems)
@ -278,7 +278,7 @@
(maker fld-cnts ...))))]) (maker fld-cnts ...))))])
rec))))] rec))))]
[else #`(flat-named-contract '#,(syntax-e pred?) #,(cert pred?))])] [else #`(flat-named-contract '#,(syntax-e pred?) #,(cert pred?))])]
[(Syntax: (Base: 'Symbol _ _ _)) #'identifier?] [(Syntax: (Base: 'Symbol _ _ _ _)) #'identifier?]
[(Syntax: t) #`(syntax/c #,(t->c t))] [(Syntax: t) #`(syntax/c #,(t->c t))]
[(Value: v) #`(flat-named-contract #,(format "~a" v) (lambda (x) (equal? x '#,v)))] [(Value: v) #`(flat-named-contract #,(format "~a" v) (lambda (x) (equal? x '#,v)))]
[(Param: in out) #`(parameter/c #,(t->c out))] [(Param: in out) #`(parameter/c #,(t->c out))]

View File

@ -161,15 +161,17 @@
;; marshaled has to be a syntax object that refers to the base type ;; marshaled has to be a syntax object that refers to the base type
;; being created. this allows us to avoid reconstructing the base type ;; being created. this allows us to avoid reconstructing the base type
;; when using it from its marshaled representation ;; when using it from its marshaled representation
(def-type Base ([name symbol?] [contract syntax?] [predicate procedure?] [marshaled syntax?]) (def-type Base ([name symbol?] [contract syntax?] [predicate procedure?] [marshaled syntax?] [numeric? boolean?])
[#:frees #f] [#:fold-rhs #:base] [#:intern name] [#:frees #f] [#:fold-rhs #:base] [#:intern name]
[#:key (case name [#:key (if numeric?
[(Number Integer) 'number] 'number
[(Boolean) 'boolean] (case name
[(String) 'string] [(Number Integer) 'number]
[(Symbol) 'symbol] [(Boolean) 'boolean]
[(Keyword) 'keyword] [(String) 'string]
[else #f])]) [(Symbol) 'symbol]
[(Keyword) 'keyword]
[else #f]))])
;; body is a Scope ;; body is a Scope
(def-type Mu ([body (scope-depth 1)]) #:no-provide [#:frees (λ (f) (f body))] (def-type Mu ([body (scope-depth 1)]) #:no-provide [#:frees (λ (f) (f body))]

View File

@ -2,7 +2,7 @@
(require "../utils/utils.rkt") (require "../utils/utils.rkt")
(require (rep type-rep object-rep filter-rep rep-utils) (require (rename-in (rep type-rep object-rep filter-rep rep-utils) [make-Base make-Base*])
"resolve.rkt" "resolve.rkt"
(utils tc-utils) (utils tc-utils)
racket/list racket/list
@ -20,10 +20,14 @@
;; for base type predicates ;; for base type predicates
racket/promise racket/tcp racket/flonum) racket/promise racket/tcp racket/flonum)
(provide (except-out (all-defined-out) Promise) (provide (except-out (all-defined-out) Promise make-Base)
(rename-out [make-Listof -lst] (rename-out [make-Listof -lst]
[make-MListof -mlst])) [make-MListof -mlst]))
;; all the types defined here are not numeric
(define (make-Base name contract predicate marshaled)
(make-Base* name contract predicate marshaled #f))
;; convenient constructors ;; convenient constructors

View File

@ -3,7 +3,7 @@
(require "../utils/utils.rkt") (require "../utils/utils.rkt")
(require (types abbrev numeric-predicates) (require (types abbrev numeric-predicates)
(rep type-rep) (rename-in (rep type-rep) [make-Base make-Base*])
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)))
@ -20,6 +20,10 @@
-ExactNumber -FloatComplex -SingleFlonumComplex -InexactComplex -Number -ExactNumber -FloatComplex -SingleFlonumComplex -InexactComplex -Number
(rename-out (-Int -Integer))) (rename-out (-Int -Integer)))
;; all the types defined here are numeric
(define (make-Base name contract predicate marshaled)
(make-Base* name contract predicate marshaled #t))
;; Numeric hierarchy ;; Numeric hierarchy
;; All built as unions of non-overlapping base types. ;; All built as unions of non-overlapping base types.

View File

@ -218,7 +218,7 @@
[else (fp "~a" v)])] [else (fp "~a" v)])]
[(? tuple? t) [(? tuple? t)
(fp "~a" (cons 'List (tuple-elems t)))] (fp "~a" (cons 'List (tuple-elems t)))]
[(Base: n cnt _ _) (fp "~s" n)] [(Base: n cnt _ _ _) (fp "~s" n)]
[(Opaque: pred _) (fp "(Opaque ~a)" (syntax->datum pred))] [(Opaque: pred _) (fp "(Opaque ~a)" (syntax->datum pred))]
[(Struct: (? (lambda (nm) (free-identifier=? promise-id nm))) [(Struct: (? (lambda (nm) (free-identifier=? promise-id nm)))
#f (list (fld: t _ _)) _ _ _ _ _) #f (list (fld: t _ _)) _ _ _ _ _)
@ -269,10 +269,10 @@
#; #;
[(Mu-unsafe: b) (fp "(unsafe-mu ~a ~a)" (Type-seq c) b)] [(Mu-unsafe: b) (fp "(unsafe-mu ~a ~a)" (Type-seq c) b)]
[(Mu: x (Syntax: (Union: (list [(Mu: x (Syntax: (Union: (list
(Base: 'Number _ _ _) (Base: 'Number _ _ _ _)
(Base: 'Boolean _ _ _) (Base: 'Boolean _ _ _ _)
(Base: 'Symbol _ _ _) (Base: 'Symbol _ _ _ _)
(Base: 'String _ _ _) (Base: 'String _ _ _ _)
(Mu: var (Union: (list (Value: '()) (Mu: var (Union: (list (Value: '())
(Pair: (F: x) (F: var))))) (Pair: (F: x) (F: var)))))
(Mu: y (Union: (list (F: x) (Mu: y (Union: (list (F: x)

View File

@ -42,16 +42,16 @@
(ormap (lambda (t*) (overlap t t*)) e)] (ormap (lambda (t*) (overlap t t*)) e)]
[(or (list _ (? Poly?)) (list (? Poly?) _)) [(or (list _ (? Poly?)) (list (? Poly?) _))
#t] ;; these can have overlap, conservatively #t] ;; these can have overlap, conservatively
[(list (Base: s1 _ _ _) (Base: s2 _ _ _)) (or (subtype t1 t2) (subtype t2 t1))] [(list (Base: s1 _ _ _ _) (Base: s2 _ _ _ _)) (or (subtype t1 t2) (subtype t2 t1))]
[(list (Base: _ _ _ _) (Value: _)) (subtype t2 t1)] ;; conservative [(list (Base: _ _ _ _ _) (Value: _)) (subtype t2 t1)] ;; conservative
[(list (Value: _) (Base: _ _ _ _)) (subtype t1 t2)] ;; conservative [(list (Value: _) (Base: _ _ _ _ _)) (subtype t1 t2)] ;; conservative
[(list (Syntax: t) (Syntax: t*)) [(list (Syntax: t) (Syntax: t*))
(overlap t t*)] (overlap t t*)]
[(or (list (Syntax: _) _) [(or (list (Syntax: _) _)
(list _ (Syntax: _))) (list _ (Syntax: _)))
#f] #f]
[(list (Base: _ _ _ _) _) #f] [(list (Base: _ _ _ _ _) _) #f]
[(list _ (Base: _ _ _ _)) #f] [(list _ (Base: _ _ _ _ _)) #f]
[(list (Value: (? pair? v)) (Pair: _ _)) #t] [(list (Value: (? pair? v)) (Pair: _ _)) #t]
[(list (Pair: _ _) (Value: (? pair? v))) #t] [(list (Pair: _ _) (Value: (? pair? v))) #t]
[(list (Pair: a b) (Pair: a* b*)) [(list (Pair: a b) (Pair: a* b*))

View File

@ -261,7 +261,7 @@
;; value types ;; value types
[((Value: v1) (Value: v2)) (=> unmatch) (if (equal? v1 v2) A0 (unmatch))] [((Value: v1) (Value: v2)) (=> unmatch) (if (equal? v1 v2) A0 (unmatch))]
;; values are subtypes of their "type" ;; values are subtypes of their "type"
[((Value: v) (Base: _ _ pred _)) (if (pred v) A0 (fail! s t))] [((Value: v) (Base: _ _ pred _ _)) (if (pred v) A0 (fail! s t))]
;; tvars are equal if they are the same variable ;; tvars are equal if they are the same variable
[((F: t) (F: t*)) (if (eq? t t*) A0 (fail! s t))] [((F: t) (F: t*)) (if (eq? t t*) A0 (fail! s t))]
;; Avoid needing to resolve things that refer to different structs. ;; Avoid needing to resolve things that refer to different structs.
@ -274,9 +274,9 @@
(fail! s t)] (fail! s t)]
[else (unmatch)])] [else (unmatch)])]
;; similar case for structs and base types, which are obviously unrelated ;; similar case for structs and base types, which are obviously unrelated
[((Base: _ _ _ _) (or (? Struct? s1) (NameStruct: s1))) [((Base: _ _ _ _ _) (or (? Struct? s1) (NameStruct: s1)))
(fail! s t)] (fail! s t)]
[((or (? Struct? s1) (NameStruct: s1)) (Base: _ _ _ _)) [((or (? Struct? s1) (NameStruct: s1)) (Base: _ _ _ _ _))
(fail! s t)] (fail! s t)]
;; same for all values. ;; same for all values.
[((Value: (? (negate struct?) _)) (or (? Struct? s1) (NameStruct: s1))) [((Value: (? (negate struct?) _)) (or (? Struct? s1) (NameStruct: s1)))
@ -284,8 +284,8 @@
[((or (? Struct? s1) (NameStruct: s1)) (Value: (? (negate struct?) _))) [((or (? Struct? s1) (NameStruct: s1)) (Value: (? (negate struct?) _)))
(fail! s t)] (fail! s t)]
;; just checking if s/t is a struct misses recursive/union/etc cases ;; just checking if s/t is a struct misses recursive/union/etc cases
[((? (lambda (_) (eq? ks 'struct))) (Base: _ _ _ _)) (fail! s t)] [((? (lambda (_) (eq? ks 'struct))) (Base: _ _ _ _ _)) (fail! s t)]
[((Base: _ _ _ _) (? (lambda (_) (eq? kt 'struct)))) (fail! s t)] [((Base: _ _ _ _ _) (? (lambda (_) (eq? kt 'struct)))) (fail! s t)]
;; sequences are covariant ;; sequences are covariant
[((Sequence: ts) (Sequence: ts*)) [((Sequence: ts) (Sequence: ts*))
(subtypes* A0 ts ts*)] (subtypes* A0 ts ts*)]
@ -297,11 +297,11 @@
(subtypes* A0 ts (map (λ _ t*) ts))] (subtypes* A0 ts (map (λ _ t*) ts))]
[((Vector: t) (Sequence: (list t*))) [((Vector: t) (Sequence: (list t*)))
(subtype* A0 t t*)] (subtype* A0 t t*)]
[((Base: 'String _ _ _) (Sequence: (list t*))) [((Base: 'String _ _ _ _) (Sequence: (list t*)))
(subtype* A0 -Char t*)] (subtype* A0 -Char t*)]
[((Base: 'Bytes _ _ _) (Sequence: (list t*))) [((Base: 'Bytes _ _ _ _) (Sequence: (list t*)))
(subtype* A0 -Byte t*)] (subtype* A0 -Byte t*)]
[((Base: 'Input-Port _ _ _) (Sequence: (list t*))) [((Base: 'Input-Port _ _ _ _) (Sequence: (list t*)))
(subtype* A0 -Nat t*)] (subtype* A0 -Nat t*)]
[((Hashtable: k v) (Sequence: (list k* v*))) [((Hashtable: k v) (Sequence: (list k* v*)))
(subtypes* A0 (list k v) (list k* v*))] (subtypes* A0 (list k v) (list k* v*))]