checkpoint
svn: r16908 original commit: 111b71c844707b146bbc1500dc086ef3c5ef7070
This commit is contained in:
Sam Tobin-Hochstadt
parent
7fe635dfee
commit
a1f96d6ce8
94
collects/typed-scheme/private/base-env-numeric.ss
Normal file
94
collects/typed-scheme/private/base-env-numeric.ss
Normal file
|
|
@ -0,0 +1,94 @@
|
|||
#lang s-exp "env-lang.ss"
|
||||
|
||||
(require
|
||||
scheme/tcp
|
||||
scheme
|
||||
scheme/unsafe/ops
|
||||
(only-in rnrs/lists-6 fold-left)
|
||||
'#%paramz
|
||||
"extra-procs.ss"
|
||||
(only-in '#%kernel [apply kernel:apply])
|
||||
scheme/promise scheme/system
|
||||
(only-in string-constants/private/only-once maybe-print-message)
|
||||
(only-in scheme/match/runtime match:error matchable? match-equality-test)
|
||||
(for-syntax (only-in (types abbrev) [-Number N] [-Boolean B] [-Symbol Sym])))
|
||||
|
||||
;; numeric operations
|
||||
[modulo (cl->* (-Integer -Integer . -> . -Integer))]
|
||||
[= (->* (list N N) N B)]
|
||||
[>= (->* (list N N) N B)]
|
||||
[< (->* (list N N) N B)]
|
||||
[<= (->* (list N N) N B)]
|
||||
[> (->* (list N N) N B)]
|
||||
[zero? (N . -> . B)]
|
||||
[* (cl->* (->* '() -Integer -Integer) (->* '() N N))]
|
||||
[/ (cl->* (->* (list N) N N))]
|
||||
[+ (cl->* (->* '() -Integer -Integer) (->* '() N N))]
|
||||
[- (cl->* (->* (list -Integer) -Integer -Integer) (->* (list N) N N))]
|
||||
[max (cl->* (->* (list -Integer) -Integer -Integer)
|
||||
(->* (list N) N N))]
|
||||
[min (cl->* (->* (list -Integer) -Integer -Integer)
|
||||
(->* (list N) N N))]
|
||||
[positive? (-> N B)]
|
||||
[negative? (-> N B)]
|
||||
[odd? (-> -Integer B)]
|
||||
[even? (-> -Integer B)]
|
||||
[add1 (cl->* (-> -Integer -Integer)
|
||||
(-> N N))]
|
||||
[sub1 (cl->* (-> -Integer -Integer)
|
||||
(-> N N))]
|
||||
[quotient (-Integer -Integer . -> . -Integer)]
|
||||
[remainder (-Integer -Integer . -> . -Integer)]
|
||||
[quotient/remainder
|
||||
(make-Function (list (make-arr (list -Integer -Integer) (-values (list -Integer -Integer)))))]
|
||||
|
||||
[exact? (N . -> . B)]
|
||||
[inexact? (N . -> . B)]
|
||||
[exact->inexact (N . -> . N)]
|
||||
[inexact->exact (N . -> . N)]
|
||||
|
||||
[number? (make-pred-ty N)]
|
||||
[integer? (Univ . -> . B : (-LFS (list (-filter N)) (list (-not-filter -Integer))))]
|
||||
[exact-integer? (make-pred-ty -Integer)]
|
||||
|
||||
[real? (Univ . -> . B : (-LFS (list (-filter N)) (list)))]
|
||||
[complex? (Univ . -> . B : (-LFS (list (-filter N)) (list)))]
|
||||
[rational? (Univ . -> . B : (-LFS (list (-filter N)) (list)))]
|
||||
[floor (-> N N)]
|
||||
[ceiling (-> N N)]
|
||||
[truncate (-> N N)]
|
||||
[make-rectangular (N N . -> . N)]
|
||||
[make-polar (N N . -> . N)]
|
||||
[real-part (N . -> . N)]
|
||||
[imag-part (N . -> . N)]
|
||||
[magnitude (N . -> . N)]
|
||||
[angle (N . -> . N)]
|
||||
[numerator (N . -> . -Integer)]
|
||||
[denominator (N . -> . -Integer)]
|
||||
[rationalize (N N . -> . N)]
|
||||
[expt (cl->* (-Integer -Integer . -> . -Integer) (N N . -> . N))]
|
||||
[sqrt (N . -> . N)]
|
||||
[log (N . -> . N)]
|
||||
[exp (N . -> . N)]
|
||||
[cos (N . -> . N)]
|
||||
[sin (N . -> . N)]
|
||||
[tan (N . -> . N)]
|
||||
[acos (N . -> . N)]
|
||||
[asin (N . -> . N)]
|
||||
[atan (N . -> . N)]
|
||||
[gcd (null -Integer . ->* . -Integer)]
|
||||
[lcm (null -Integer . ->* . -Integer)]
|
||||
|
||||
[round (N . -> . -Integer)]
|
||||
|
||||
;; scheme/math
|
||||
|
||||
[sgn (-Real . -> . -Real)]
|
||||
[pi N]
|
||||
[sqr (N . -> . N)]
|
||||
[sgn (N . -> . N)]
|
||||
[conjugate (N . -> . N)]
|
||||
[sinh (N . -> . N)]
|
||||
[cosh (N . -> . N)]
|
||||
[tanh (N . -> . N)]
|
||||
;; end numeric ops
|
||||
|
|
@ -11,7 +11,10 @@
|
|||
scheme/promise scheme/system
|
||||
(only-in string-constants/private/only-once maybe-print-message)
|
||||
(only-in scheme/match/runtime match:error matchable? match-equality-test)
|
||||
(for-syntax (only-in (types abbrev) [-Number N] [-Boolean B] [-Symbol Sym])))
|
||||
(for-syntax (only-in (types abbrev) [-Number N] [-Boolean B] [-Symbol Sym]))
|
||||
;; require the split-out files
|
||||
"base-env-numeric.ss"
|
||||
)
|
||||
|
||||
[raise (Univ . -> . (Un))]
|
||||
|
||||
|
|
@ -55,19 +58,12 @@
|
|||
[null? (make-pred-ty (-val null))]
|
||||
[eof-object? (make-pred-ty (-val eof))]
|
||||
[null (-val null)]
|
||||
[number? (make-pred-ty N)]
|
||||
[char? (make-pred-ty -Char)]
|
||||
[integer? (Univ . -> . B : (-LFS (list (-filter N)) (list (-not-filter -Integer))))]
|
||||
[exact-integer? (make-pred-ty -Integer)]
|
||||
|
||||
[boolean? (make-pred-ty B)]
|
||||
[add1 (cl->* (-> -Integer -Integer)
|
||||
(-> N N))]
|
||||
[sub1 (cl->* (-> -Integer -Integer)
|
||||
(-> N N))]
|
||||
[eq? (-> Univ Univ B)]
|
||||
[eqv? (-> Univ Univ B)]
|
||||
[equal? (-> Univ Univ B)]
|
||||
[even? (-> N B)]
|
||||
[assert (-poly (a) (-> (Un a (-val #f)) a))]
|
||||
[gensym (cl-> [(Sym) Sym]
|
||||
[() Sym])]
|
||||
|
|
@ -167,20 +163,6 @@
|
|||
|
||||
[sleep (N . -> . -Void)]
|
||||
|
||||
[= (->* (list N N) N B)]
|
||||
[>= (->* (list N N) N B)]
|
||||
[< (->* (list N N) N B)]
|
||||
[<= (->* (list N N) N B)]
|
||||
[> (->* (list N N) N B)]
|
||||
[zero? (N . -> . B)]
|
||||
[* (cl->* (->* '() -Integer -Integer) (->* '() N N))]
|
||||
[/ (cl->* (->* (list N) N N))]
|
||||
[+ (cl->* (->* '() -Integer -Integer) (->* '() N N))]
|
||||
[- (cl->* (->* (list -Integer) -Integer -Integer) (->* (list N) N N))]
|
||||
[max (cl->* (->* (list -Integer) -Integer -Integer)
|
||||
(->* (list N) N N))]
|
||||
[min (cl->* (->* (list -Integer) -Integer -Integer)
|
||||
(->* (list N) N N))]
|
||||
[build-list (-poly (a) (-Integer (-Integer . -> . a) . -> . (-lst a)))]
|
||||
[reverse (-poly (a) (-> (-lst a) (-lst a)))]
|
||||
[append (-poly (a) (->* (list) (-lst a) (-lst a)))]
|
||||
|
|
@ -229,10 +211,10 @@
|
|||
|
||||
[string-copy (-> -String -String)]
|
||||
[string->immutable-string (-> -String -String)]
|
||||
[string-ref (-> -String N -Char)]
|
||||
[string-ref (-> -String -Nat -Char)]
|
||||
[substring (cl->*
|
||||
(-> -String N -String)
|
||||
(-> -String N N -String))]
|
||||
(-> -String -Nat -String)
|
||||
(-> -String -Nat -Nat -String))]
|
||||
[string->path (-> -String -Path)]
|
||||
[file-exists? (-> -Pathlike B)]
|
||||
|
||||
|
|
@ -248,7 +230,7 @@
|
|||
#:mode (one-of/c 'binary 'text) #f
|
||||
a))]
|
||||
|
||||
[random (cl-> [(-Integer) -Integer] [() N])]
|
||||
[random (cl-> [(-Nat) -Nat] [() -Real])]
|
||||
|
||||
[assq (-poly (a b) (a (-lst (-pair a b)) . -> . (-opt (-pair a b))))]
|
||||
[assv (-poly (a b) (a (-lst (-pair a b)) . -> . (-opt (-pair a b))))]
|
||||
|
|
@ -258,10 +240,6 @@
|
|||
|
||||
[list-ref (-poly (a) ((-lst a) -Integer . -> . a))]
|
||||
[list-tail (-poly (a) ((-lst a) -Integer . -> . (-lst a)))]
|
||||
[positive? (-> N B)]
|
||||
[negative? (-> N B)]
|
||||
[odd? (-> -Integer B)]
|
||||
[even? (-> -Integer B)]
|
||||
|
||||
[apply (-poly (a b) (((list) a . ->* . b) (-lst a) . -> . b))]
|
||||
[kernel:apply (-poly (a b) (((list) a . ->* . b) (-lst a) . -> . b))]
|
||||
|
|
@ -270,7 +248,7 @@
|
|||
(list (make-arr
|
||||
(list ((list) (a a) . ->... . b)
|
||||
(-lst a))
|
||||
(-values (list (-pair b (-val '())) N N N))))))]
|
||||
(-values (list (-pair b (-val '())) -Integer -Integer -Integer))))))]
|
||||
|
||||
[call/cc (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (Un a b)))]
|
||||
[call/ec (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (Un a b)))]
|
||||
|
|
@ -278,12 +256,6 @@
|
|||
[call-with-escape-continuation (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (Un a b)))]
|
||||
|
||||
[struct->vector (Univ . -> . (-vec Univ))]
|
||||
|
||||
[quotient (-Integer -Integer . -> . -Integer)]
|
||||
[remainder (-Integer -Integer . -> . -Integer)]
|
||||
[quotient/remainder
|
||||
(make-Function (list (make-arr (list -Integer -Integer) (-values (list -Integer -Integer)))))]
|
||||
|
||||
;; parameter stuff
|
||||
|
||||
[parameterization-key Sym]
|
||||
|
|
@ -313,7 +285,8 @@
|
|||
|
||||
[regexp-match
|
||||
(let ([?outp (-opt -Output-Port)]
|
||||
[?N (-opt N)]
|
||||
[N -Nat]
|
||||
[?N (-opt -Nat)]
|
||||
[optlist (lambda (t) (-opt (-lst (-opt t))))]
|
||||
[-StrRx (Un -String -Regexp -PRegexp)]
|
||||
[-BtsRx (Un -Bytes -Byte-Regexp -Byte-PRegexp)]
|
||||
|
|
@ -332,7 +305,8 @@
|
|||
[(-Pattern -InpBts N ?N ?outp) (optlist -Bytes)]))]
|
||||
|
||||
[regexp-match*
|
||||
(let ([?N (-opt N)]
|
||||
(let ([N -Nat]
|
||||
[?N (-opt -Nat)]
|
||||
[-StrRx (Un -String -Regexp -PRegexp)]
|
||||
[-BtsRx (Un -Bytes -Byte-Regexp -Byte-PRegexp)]
|
||||
[-InpBts (Un -Input-Port -Bytes)])
|
||||
|
|
@ -342,9 +316,9 @@
|
|||
(-Pattern -InpBts [N ?N] . ->opt . (-lst -Bytes))))]
|
||||
[regexp-try-match
|
||||
(let ([?outp (-opt -Output-Port)]
|
||||
[?N (-opt N)]
|
||||
[?N (-opt -Nat)]
|
||||
[optlist (lambda (t) (-opt (-lst (-opt t))))])
|
||||
(->opt -Pattern -Input-Port [N ?N ?outp] (optlist -Bytes)))]
|
||||
(->opt -Pattern -Input-Port [-Nat ?N ?outp] (optlist -Bytes)))]
|
||||
|
||||
[regexp-match-exact?
|
||||
(-Pattern (Un -String -Bytes -Input-Port) . -> . B)]
|
||||
|
|
@ -352,7 +326,8 @@
|
|||
|
||||
[regexp-match-positions
|
||||
(let ([?outp (-opt -Output-Port)]
|
||||
[?N (-opt N)]
|
||||
[N -Nat]
|
||||
[?N (-opt -Nat)]
|
||||
[optlist (lambda (t) (-opt (-lst (-opt t))))]
|
||||
[-StrRx (Un -String -Regexp -PRegexp)]
|
||||
[-BtsRx (Un -Bytes -Byte-Regexp -Byte-PRegexp)]
|
||||
|
|
@ -360,12 +335,12 @@
|
|||
(->opt -Pattern (Un -String -InpBts) [N ?N ?outp] (optlist (-pair -Nat -Nat))))]
|
||||
[regexp-match-positions*
|
||||
(let ([?outp (-opt -Output-Port)]
|
||||
[?N (-opt N)]
|
||||
[?N (-opt -Nat)]
|
||||
[optlist (lambda (t) (-opt (-lst (-opt t))))]
|
||||
[-StrRx (Un -String -Regexp -PRegexp)]
|
||||
[-BtsRx (Un -Bytes -Byte-Regexp -Byte-PRegexp)]
|
||||
[-InpBts (Un -Input-Port -Bytes)])
|
||||
(->opt -Pattern (Un -String -InpBts) [N ?N ?outp] (-lst (-pair -Nat -Nat))))]
|
||||
(->opt -Pattern (Un -String -InpBts) [-Nat ?N ?outp] (-lst (-pair -Nat -Nat))))]
|
||||
#;
|
||||
[regexp-match-peek-positions*]
|
||||
#;
|
||||
|
|
@ -383,7 +358,6 @@
|
|||
[string->number (cl-> [(-String) N] [(-String N) N])]
|
||||
|
||||
[current-milliseconds (-> -Integer)]
|
||||
[modulo (cl->* (-Integer -Integer . -> . -Integer))]
|
||||
|
||||
;; errors
|
||||
|
||||
|
|
@ -395,38 +369,6 @@
|
|||
;; this is a hack
|
||||
|
||||
[match:error ((list) Univ . ->* . (Un))]
|
||||
[exact? (N . -> . B)]
|
||||
[inexact? (N . -> . B)]
|
||||
[exact->inexact (N . -> . N)]
|
||||
[inexact->exact (N . -> . N)]
|
||||
|
||||
[real? (Univ . -> . B : (-LFS (list (-filter N)) (list)))]
|
||||
[complex? (Univ . -> . B : (-LFS (list (-filter N)) (list)))]
|
||||
[rational? (Univ . -> . B : (-LFS (list (-filter N)) (list)))]
|
||||
[floor (-> N N)]
|
||||
[ceiling (-> N N)]
|
||||
[truncate (-> N N)]
|
||||
[make-rectangular (N N . -> . N)]
|
||||
[make-polar (N N . -> . N)]
|
||||
[real-part (N . -> . N)]
|
||||
[imag-part (N . -> . N)]
|
||||
[magnitude (N . -> . N)]
|
||||
[angle (N . -> . N)]
|
||||
[numerator (N . -> . -Integer)]
|
||||
[denominator (N . -> . -Integer)]
|
||||
[rationalize (N N . -> . N)]
|
||||
[expt (cl->* (-Integer -Integer . -> . -Integer) (N N . -> . N))]
|
||||
[sqrt (N . -> . N)]
|
||||
[log (N . -> . N)]
|
||||
[exp (N . -> . N)]
|
||||
[cos (N . -> . N)]
|
||||
[sin (N . -> . N)]
|
||||
[tan (N . -> . N)]
|
||||
[acos (N . -> . N)]
|
||||
[asin (N . -> . N)]
|
||||
[atan (N . -> . N)]
|
||||
[gcd (null -Integer . ->* . -Integer)]
|
||||
[lcm (null -Integer . ->* . -Integer)]
|
||||
|
||||
[arithmetic-shift (-Integer -Integer . -> . -Integer)]
|
||||
[bitwise-and (null -Integer . ->* . -Integer)]
|
||||
|
|
@ -480,7 +422,6 @@
|
|||
[current-output-port (-Param -Output-Port -Output-Port)]
|
||||
[current-error-port (-Param -Output-Port -Output-Port)]
|
||||
[current-input-port (-Param -Input-Port -Input-Port)]
|
||||
[round (N . -> . -Integer)]
|
||||
[seconds->date (-Integer . -> . (make-Name #'date))]
|
||||
[current-seconds (-> -Integer)]
|
||||
[current-print (-Param (Univ . -> . Univ) (Univ . -> . Univ))]
|
||||
|
|
@ -765,16 +706,6 @@
|
|||
(funarg* a (-opt -Pathlike) . -> . a)
|
||||
(funarg* a (-opt -Pathlike) Univ . -> . a))))]
|
||||
|
||||
;; scheme/math
|
||||
|
||||
[sgn (-Real . -> . -Real)]
|
||||
[pi N]
|
||||
[sqr (N . -> . N)]
|
||||
[sgn (N . -> . N)]
|
||||
[conjugate (N . -> . N)]
|
||||
[sinh (N . -> . N)]
|
||||
[cosh (N . -> . N)]
|
||||
[tanh (N . -> . N)]
|
||||
|
||||
;; scheme/pretty
|
||||
|
||||
|
|
|
|||
|
|
@ -1,7 +1,15 @@
|
|||
#lang s-exp "type-env-lang.ss"
|
||||
|
||||
[Number -Number]
|
||||
[Complex -Number]
|
||||
[Integer -Integer]
|
||||
[Real -Real]
|
||||
[Exact-Rational -ExactRational]
|
||||
[Flonum -Flonum]
|
||||
[Exact-Positive-Integer -ExactPositiveInteger]
|
||||
[Exact-Nonnegative-Integer -ExactNonnegativeInteger]
|
||||
[Natural -ExactNonnegativeInteger]
|
||||
|
||||
[Void -Void]
|
||||
[Boolean -Boolean]
|
||||
[Symbol -Symbol]
|
||||
|
|
|
|||
|
|
@ -32,8 +32,14 @@
|
|||
[i:exp expected]
|
||||
[i:boolean (-val (syntax-e #'i))]
|
||||
[i:identifier (-val (syntax-e #'i))]
|
||||
[i:exact-integer -Integer]
|
||||
[(~var i (3d real?)) -Number]
|
||||
[0 -Zero]
|
||||
[(~var i (3d exact-positive-integer?)) -ExactPositiveInteger]
|
||||
[(~var i (3d exact-nonnegative-integer?)) -ExactNonnegativeInteger]
|
||||
[(~var i (3d exact-integer?)) -Integer]
|
||||
[(~var i (3d (lambda (e) (and (exact? e) (rational? e))))) -ExactRational]
|
||||
[(~var i (3d inexact-real?)) -Flonum]
|
||||
[(~var i (3d real?)) -Real]
|
||||
[(~var i (3d number?)) -Number]
|
||||
[i:str -String]
|
||||
[i:char -Char]
|
||||
[i:keyword (-val (syntax-e #'i))]
|
||||
|
|
|
|||
|
|
@ -67,9 +67,6 @@
|
|||
|
||||
(define -Listof (-poly (list-elem) (make-Listof list-elem)))
|
||||
|
||||
|
||||
(define -Number (make-Base 'Number #'number?))
|
||||
(define -Integer (make-Base 'Integer #'exact-integer?))
|
||||
(define -Boolean (make-Base 'Boolean #'boolean?))
|
||||
(define -Symbol (make-Base 'Symbol #'symbol?))
|
||||
(define -Void (make-Base 'Void #'void?))
|
||||
|
|
@ -96,15 +93,11 @@
|
|||
(define Univ (make-Univ))
|
||||
(define Err (make-Error))
|
||||
|
||||
(define -Nat -Integer)
|
||||
(define -Real -Number)
|
||||
|
||||
(define -Port (*Un -Output-Port -Input-Port))
|
||||
|
||||
(define -Pathlike (*Un -String -Path))
|
||||
(define -Pathlike* (*Un -String -Path (-val 'up) (-val 'same)))
|
||||
(define -Pattern (*Un -Bytes -Regexp -PRegexp -Byte-Regexp -Byte-PRegexp -String))
|
||||
(define -Byte -Number)
|
||||
|
||||
(define -no-lfilter (make-LFilterSet null null))
|
||||
(define -no-filter (make-FilterSet null null))
|
||||
|
|
@ -114,6 +107,26 @@
|
|||
(define -car (make-CarPE))
|
||||
(define -cdr (make-CdrPE))
|
||||
|
||||
;; Numeric hierarchy
|
||||
(define -Number (make-Base 'Number #'number?))
|
||||
|
||||
(define -Flonum (make-Base 'Flonum #'inexact-real?))
|
||||
|
||||
(define -ExactRational
|
||||
(make-Base 'Exact-Rational #'(and/c rational? exact?)))
|
||||
(define -Integer (make-Base 'Integer #'exact-integer?))
|
||||
(define -ExactPositiveInteger
|
||||
(make-Base 'Exact-Positive-Integer #'exact-positive-integer?))
|
||||
|
||||
(define -Zero (-val 0))
|
||||
(define -Real (*Un -Flonum -ExactRational))
|
||||
(define -ExactNonnegativeInteger (*Un -Zero -ExactPositiveInteger))
|
||||
(define -Nat -ExactNonnegativeInteger)
|
||||
|
||||
(define -Byte -Number)
|
||||
|
||||
|
||||
|
||||
;; convenient syntax
|
||||
|
||||
(define-syntax -v
|
||||
|
|
|
|||
|
|
@ -5,7 +5,7 @@
|
|||
(types utils comparison resolve abbrev)
|
||||
(env type-name-env)
|
||||
(only-in (infer infer-dummy) unify)
|
||||
scheme/match
|
||||
scheme/match unstable/match
|
||||
mzlib/trace
|
||||
(for-syntax scheme/base syntax/parse))
|
||||
|
||||
|
|
@ -210,34 +210,46 @@
|
|||
[else
|
||||
(let* ([A0 (remember s t A)])
|
||||
(parameterize ([current-seen A0])
|
||||
(match (list s t)
|
||||
[(list _ (Univ:)) A0]
|
||||
(match* (s t)
|
||||
[(_ (Univ:)) A0]
|
||||
;; error is top and bot
|
||||
[(list _ (Error:)) A0]
|
||||
[(list (Error:) _) A0]
|
||||
[(_ (Error:)) A0]
|
||||
[((Error:) _) A0]
|
||||
;; (Un) is bot
|
||||
[(list _ (Union: (list))) (fail! s t)]
|
||||
[(list (Union: (list)) _) A0]
|
||||
[(_ (Union: (list))) (fail! s t)]
|
||||
[((Union: (list)) _) A0]
|
||||
;; value types
|
||||
[(list (Value: v1) (Value: v2)) (=> unmatch) (if (equal? v1 v2) A0 (unmatch))]
|
||||
;; integers are numbers too
|
||||
[(list (Base: 'Integer _) (Base: 'Number _)) A0]
|
||||
[((Value: v1) (Value: v2)) (=> unmatch) (if (equal? v1 v2) A0 (unmatch))]
|
||||
;; now we encode the numeric hierarchy - bletch
|
||||
[((Base: 'Integer _) (Base: 'Number _)) A0]
|
||||
[((Base: 'Flonum _) (== -Real type-equal?)) A0]
|
||||
[((Base: 'Integer _) (== -Real type-equal?)) A0]
|
||||
[((Base: 'Flonum _) (Base: 'Number _)) A0]
|
||||
[((Base: 'Exact-Rational _) (Base: 'Number _)) A0]
|
||||
[((Base: 'Exact-Positive-Integer _) (Base: 'Exact-Rational _)) A0]
|
||||
[((Base: 'Exact-Positive-Integer _) (Base: 'Number _)) A0]
|
||||
|
||||
;; values are subtypes of their "type"
|
||||
[(list (Value: (? integer? n)) (Base: 'Integer _)) A0]
|
||||
[(list (Value: (? number? n)) (Base: 'Number _)) A0]
|
||||
[(list (Value: (? boolean? n)) (Base: 'Boolean _)) A0]
|
||||
[(list (Value: (? symbol? n)) (Base: 'Symbol _)) A0]
|
||||
[(list (Value: (? string? n)) (Base: 'String _)) A0]
|
||||
[((Value: (? integer? n)) (Base: 'Integer _)) A0]
|
||||
[((Value: (? exact-nonnegative-integer? n)) (Base: 'Exact-Nonnegative-Integer _)) A0]
|
||||
[((Value: (? exact-positive-integer? n)) (Base: 'Exact-Positive-Integer _)) A0]
|
||||
[((Value: (? inexact-real? n)) (Base: 'Flonum _)) A0]
|
||||
[((Value: (? real? n)) (== -Real type-equal?)) A0]
|
||||
[((Value: (? number? n)) (Base: 'Number _)) A0]
|
||||
|
||||
[((Value: (? boolean? n)) (Base: 'Boolean _)) A0]
|
||||
[((Value: (? symbol? n)) (Base: 'Symbol _)) A0]
|
||||
[((Value: (? string? n)) (Base: 'String _)) A0]
|
||||
;; tvars are equal if they are the same variable
|
||||
[(list (F: t) (F: t*)) (if (eq? t t*) A0 (fail! s t))]
|
||||
[((F: t) (F: t*)) (if (eq? t t*) A0 (fail! s t))]
|
||||
;; special-case for case-lambda/union
|
||||
[(list (Function: arr1) (Function: (list arr2)))
|
||||
[((Function: arr1) (Function: (list arr2)))
|
||||
(when (null? arr1) (fail! s t))
|
||||
(or (arr-subtype*/no-fail A0 (combine-arrs arr1) arr2)
|
||||
(supertype-of-one/arr A0 arr2 arr1)
|
||||
(fail! s t))]
|
||||
;; case-lambda
|
||||
[(list (Function: arr1) (Function: arr2))
|
||||
[((Function: arr1) (Function: arr2))
|
||||
(when (null? arr1) (fail! s t))
|
||||
(let loop-arities ([A* A0]
|
||||
[arr2 arr2])
|
||||
|
|
@ -246,65 +258,65 @@
|
|||
[(supertype-of-one/arr A* (car arr2) arr1) => (lambda (A) (loop-arities A (cdr arr2)))]
|
||||
[else (fail! s t)]))]
|
||||
;; recur structurally on pairs
|
||||
[(list (Pair: a d) (Pair: a* d*))
|
||||
[((Pair: a d) (Pair: a* d*))
|
||||
(let ([A1 (subtype* A0 a a*)])
|
||||
(and A1 (subtype* A1 d d*)))]
|
||||
;; quantification over two types preserves subtyping
|
||||
[(list (Poly: ns b1) (Poly: ms b2))
|
||||
[((Poly: ns b1) (Poly: ms b2))
|
||||
(=> unmatch)
|
||||
(unless (= (length ns) (length ms))
|
||||
(unmatch))
|
||||
;(printf "Poly: ~n~a ~n~a~n" b1 (subst-all (map list ms (map make-F ns)) b2))
|
||||
(subtype* A0 b1 (subst-all (map list ms (map make-F ns)) b2))]
|
||||
[(list (Refinement: par _ _) t)
|
||||
[((Refinement: par _ _) t)
|
||||
(subtype* A0 par t)]
|
||||
;; use unification to see if we can use the polytype here
|
||||
[(list (Poly: vs b) s)
|
||||
[((Poly: vs b) s)
|
||||
(=> unmatch)
|
||||
(if (unify vs (list b) (list s)) A0 (unmatch))]
|
||||
[(list s (Poly: vs b))
|
||||
[(s (Poly: vs b))
|
||||
(=> unmatch)
|
||||
(if (null? (fv b)) (subtype* A0 s b) (unmatch))]
|
||||
;; rec types, applications and names (that aren't the same
|
||||
[(list (? needs-resolving? s) other)
|
||||
[((? needs-resolving? s) other)
|
||||
(let ([s* (resolve-once s)])
|
||||
(if (Type? s*) ;; needed in case this was a name that hasn't been resolved yet
|
||||
(subtype* A0 s* other)
|
||||
(fail! s t)))]
|
||||
[(list other (? needs-resolving? t))
|
||||
[(other (? needs-resolving? t))
|
||||
(let ([t* (resolve-once t)])
|
||||
(if (Type? t*) ;; needed in case this was a name that hasn't been resolved yet
|
||||
(subtype* A0 other t*)
|
||||
(fail! s t)))]
|
||||
;; for unions, we check the cross-product
|
||||
[(list (Union: es) t) (and (andmap (lambda (elem) (subtype* A0 elem t)) es) A0)]
|
||||
[(list s (Union: es)) (and (ormap (lambda (elem) (subtype*/no-fail A0 s elem)) es) A0)]
|
||||
[((Union: es) t) (and (andmap (lambda (elem) (subtype* A0 elem t)) es) A0)]
|
||||
[(s (Union: es)) (and (ormap (lambda (elem) (subtype*/no-fail A0 s elem)) es) A0)]
|
||||
;; subtyping on immutable structs is covariant
|
||||
[(list (Struct: nm _ flds #f _ _ _) (Struct: nm _ flds* #f _ _ _))
|
||||
[((Struct: nm _ flds #f _ _ _) (Struct: nm _ flds* #f _ _ _))
|
||||
(subtypes* A0 flds flds*)]
|
||||
[(list (Struct: nm _ flds proc _ _ _) (Struct: nm _ flds* proc* _ _ _))
|
||||
[((Struct: nm _ flds proc _ _ _) (Struct: nm _ flds* proc* _ _ _))
|
||||
(subtypes* A0 (cons proc flds) (cons proc* flds*))]
|
||||
;; subtyping on structs follows the declared hierarchy
|
||||
[(list (Struct: nm (? Type? parent) flds proc _ _ _) other)
|
||||
[((Struct: nm (? Type? parent) flds proc _ _ _) other)
|
||||
;(printf "subtype - hierarchy : ~a ~a ~a~n" nm parent other)
|
||||
(subtype* A0 parent other)]
|
||||
;; Promises are covariant
|
||||
[(list (Struct: 'Promise _ (list t) _ _ _ _) (Struct: 'Promise _ (list t*) _ _ _ _)) (subtype* A0 t t*)]
|
||||
[((Struct: 'Promise _ (list t) _ _ _ _) (Struct: 'Promise _ (list t*) _ _ _ _)) (subtype* A0 t t*)]
|
||||
;; subtyping on values is pointwise
|
||||
[(list (Values: vals1) (Values: vals2)) (subtypes* A0 vals1 vals2)]
|
||||
[((Values: vals1) (Values: vals2)) (subtypes* A0 vals1 vals2)]
|
||||
;; trivial case for Result
|
||||
[(list (Result: t f o) (Result: t* f o))
|
||||
[((Result: t f o) (Result: t* f o))
|
||||
(subtype* A0 t t*)]
|
||||
;; we can ignore interesting results
|
||||
[(list (Result: t f o) (Result: t* (LFilterSet: (list) (list)) (LEmpty:)))
|
||||
[((Result: t f o) (Result: t* (LFilterSet: (list) (list)) (LEmpty:)))
|
||||
(subtype* A0 t t*)]
|
||||
;; subtyping on other stuff
|
||||
[(list (Syntax: t) (Syntax: t*))
|
||||
[((Syntax: t) (Syntax: t*))
|
||||
(subtype* A0 t t*)]
|
||||
[(list (Instance: t) (Instance: t*))
|
||||
[((Instance: t) (Instance: t*))
|
||||
(subtype* A0 t t*)]
|
||||
;; otherwise, not a subtype
|
||||
[_ (fail! s t) #;(printf "failed")])))]))))
|
||||
[(_ _) (fail! s t) #;(printf "failed")])))]))))
|
||||
|
||||
(define (type-compare? a b)
|
||||
(and (subtype a b) (subtype b a)))
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user