diff --git a/collects/typed-scheme/private/base-env-numeric.ss b/collects/typed-scheme/private/base-env-numeric.ss new file mode 100644 index 00000000..682cb7a2 --- /dev/null +++ b/collects/typed-scheme/private/base-env-numeric.ss @@ -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 diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss index 2f60de6a..1c7f92a6 100644 --- a/collects/typed-scheme/private/base-env.ss +++ b/collects/typed-scheme/private/base-env.ss @@ -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 diff --git a/collects/typed-scheme/private/base-types.ss b/collects/typed-scheme/private/base-types.ss index 32e03043..bd9a6089 100644 --- a/collects/typed-scheme/private/base-types.ss +++ b/collects/typed-scheme/private/base-types.ss @@ -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] diff --git a/collects/typed-scheme/typecheck/tc-expr-unit.ss b/collects/typed-scheme/typecheck/tc-expr-unit.ss index b57abb2f..85a5b9d8 100644 --- a/collects/typed-scheme/typecheck/tc-expr-unit.ss +++ b/collects/typed-scheme/typecheck/tc-expr-unit.ss @@ -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))] diff --git a/collects/typed-scheme/types/abbrev.ss b/collects/typed-scheme/types/abbrev.ss index 27e9ed6e..164483b0 100644 --- a/collects/typed-scheme/types/abbrev.ss +++ b/collects/typed-scheme/types/abbrev.ss @@ -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 diff --git a/collects/typed-scheme/types/subtype.ss b/collects/typed-scheme/types/subtype.ss index 3bbb1d6d..04de5214 100644 --- a/collects/typed-scheme/types/subtype.ss +++ b/collects/typed-scheme/types/subtype.ss @@ -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)))