From 1c4fab4bfdb50e515875bf595b3b228e1823b898 Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Fri, 30 May 2008 20:03:54 +0000 Subject: [PATCH] Add a cert to go with the struct predicate. svn: r10061 --- collects/typed-scheme/private/base-env.ss | 2 +- collects/typed-scheme/private/infer-ops.ss | 2 +- collects/typed-scheme/private/infer.ss | 2 +- collects/typed-scheme/private/init-envs.ss | 4 ++-- collects/typed-scheme/private/subtype.ss | 8 ++++---- collects/typed-scheme/private/tc-app-unit.ss | 2 +- collects/typed-scheme/private/tc-structs.ss | 4 ++-- collects/typed-scheme/private/type-contract.ss | 2 +- collects/typed-scheme/private/type-effect-convenience.ss | 2 +- collects/typed-scheme/private/type-effect-printer.ss | 4 ++-- collects/typed-scheme/private/type-rep.ss | 8 ++++++-- collects/typed-scheme/private/unify.ss | 2 +- 12 files changed, 23 insertions(+), 19 deletions(-) diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss index a210f85d50..5e49e8f7af 100644 --- a/collects/typed-scheme/private/base-env.ss +++ b/collects/typed-scheme/private/base-env.ss @@ -366,7 +366,7 @@ [current-error-port (-Param -Output-Port -Output-Port)] [current-input-port (-Param -Input-Port -Input-Port)] [round (N . -> . N)] - [seconds->date (N . -> . (make-Struct 'date #f (list N N N N N N N N B N) #f #f #'date?))] + [seconds->date (N . -> . (make-Struct 'date #f (list N N N N N N N N B N) #f #f #'date? values))] [current-seconds (-> N)] [sqrt (-> N N)] [path->string (-> -Path -String)] diff --git a/collects/typed-scheme/private/infer-ops.ss b/collects/typed-scheme/private/infer-ops.ss index 97f42cc91c..33fcbddd03 100644 --- a/collects/typed-scheme/private/infer-ops.ss +++ b/collects/typed-scheme/private/infer-ops.ss @@ -188,7 +188,7 @@ (cgen V X S e))) (fail! S T))] - [((Struct: nm p flds proc _ _) (Struct: nm p flds* proc* _ _)) + [((Struct: nm p flds proc _ _ _) (Struct: nm p flds* proc* _ _ _)) (let-values ([(flds flds*) (cond [(and proc proc*) (values (cons proc flds) (cons proc* flds*))] diff --git a/collects/typed-scheme/private/infer.ss b/collects/typed-scheme/private/infer.ss index a7733ce2f8..295c38599c 100644 --- a/collects/typed-scheme/private/infer.ss +++ b/collects/typed-scheme/private/infer.ss @@ -287,7 +287,7 @@ [(list (Syntax: s1) (Syntax: s2)) (infer/int s1 s2 mapping flag)] ;; structs just recur - [(list (Struct: nm p flds proc _ _) (Struct: nm p flds* proc* _ _)) + [(list (Struct: nm p flds proc _ _ _) (Struct: nm p flds* proc* _ _ _)) (cond [(and proc proc*) (infer/int/list (cons proc flds) (cons proc* flds*) mapping flag)] [(or proc proc*) diff --git a/collects/typed-scheme/private/init-envs.ss b/collects/typed-scheme/private/init-envs.ss index f1821d2bd2..9974a4ce57 100644 --- a/collects/typed-scheme/private/init-envs.ss +++ b/collects/typed-scheme/private/init-envs.ss @@ -19,8 +19,8 @@ (match v [(Union: elems) `(make-Union (list ,@(map sub elems)))] [(Name: stx) `(make-Name (quote-syntax ,stx))] - [(Struct: name parent flds proc poly? pred-id) - `(make-Struct ,(sub name) ,(sub parent) ,(sub flds) ,(sub proc) ,(sub poly?) (quote-syntax ,pred-id))] + [(Struct: name parent flds proc poly? pred-id cert) + `(make-Struct ,(sub name) ,(sub parent) ,(sub flds) ,(sub proc) ,(sub poly?) (quote-syntax ,pred-id) (syntax-local-certifier))] [(App: rator rands stx) `(make-App ,(sub rator) ,(sub rands) (quote-syntax ,stx))] [(Opaque: pred cert) `(make-Opaque (quote-syntax ,pred) (syntax-local-certifier))] [(Mu-name: n b) `(make-Mu ,(sub n) ,(sub b))] diff --git a/collects/typed-scheme/private/subtype.ss b/collects/typed-scheme/private/subtype.ss index 655c9a9d80..91f0accfb1 100644 --- a/collects/typed-scheme/private/subtype.ss +++ b/collects/typed-scheme/private/subtype.ss @@ -214,12 +214,12 @@ [(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)] ;; subtyping on immutable structs is covariant - [(list (Struct: nm _ flds #f _ _) (Struct: nm _ flds* #f _ _)) + [(list (Struct: nm _ flds #f _ _ _) (Struct: nm _ flds* #f _ _ _)) (subtypes* A0 flds flds*)] - [(list (Struct: nm _ flds proc _ _) (Struct: nm _ flds* proc* _ _)) + [(list (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) + [(list (Struct: nm (? Type? parent) flds proc _ _ _) other) ;(printf "subtype - hierarchy : ~a ~a ~a~n" nm parent other) (subtype* A0 parent other)] ;; applications and names are structs too @@ -261,7 +261,7 @@ (subtype* A0 t other) (fail! s t)))] ;; Promises are covariant - [(list (Struct: 'Promise _ (list t) _ _ _) (Struct: 'Promise _ (list t*) _ _ _)) (subtype* A0 t t*)] + [(list (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)] ;; single values shouldn't actually happen, but they're just like the type diff --git a/collects/typed-scheme/private/tc-app-unit.ss b/collects/typed-scheme/private/tc-app-unit.ss index 9fa1dadea9..64f7a486d1 100644 --- a/collects/typed-scheme/private/tc-app-unit.ss +++ b/collects/typed-scheme/private/tc-app-unit.ss @@ -204,7 +204,7 @@ [arg-els-effs arg-els-effs] [args args-stx]) (match ftype - [(tc-result: (and sty (Struct: _ _ _ (? Type? proc-ty) _ _)) thn-eff els-eff) + [(tc-result: (and sty (Struct: _ _ _ (? Type? proc-ty) _ _ _)) thn-eff els-eff) (outer-loop (ret proc-ty thn-eff els-eff) (cons (tc-result-t ftype0) argtypes) (cons (list) arg-thn-effs) diff --git a/collects/typed-scheme/private/tc-structs.ss b/collects/typed-scheme/private/tc-structs.ss index a3ebef229e..eeb760ee56 100644 --- a/collects/typed-scheme/private/tc-structs.ss +++ b/collects/typed-scheme/private/tc-structs.ss @@ -80,7 +80,7 @@ ;; Option[Struct-Ty] -> Listof[Type] (define (get-parent-flds p) (match p - [(Struct: _ _ flds _ _ _) flds] + [(Struct: _ _ flds _ _ _ _) flds] [(Name: n) (get-parent-flds (lookup-type-name n))] [#f null])) @@ -99,7 +99,7 @@ (define-values (maker pred getters setters) (struct-names nm flds setters?)) (let* ([name (syntax-e nm)] [fld-types (append parent-field-types types)] - [sty (make-Struct name parent fld-types proc-ty poly? pred)] + [sty (make-Struct name parent fld-types proc-ty poly? pred (syntax-local-certifier))] [external-fld-types/no-parent types] [external-fld-types fld-types]) (register-struct-types nm sty flds external-fld-types external-fld-types/no-parent setters? diff --git a/collects/typed-scheme/private/type-contract.ss b/collects/typed-scheme/private/type-contract.ss index 3e9f4a7968..ea9ea6b671 100644 --- a/collects/typed-scheme/private/type-contract.ss +++ b/collects/typed-scheme/private/type-contract.ss @@ -117,7 +117,7 @@ [(Instance: _) #'(is-a?/c object%)] [(Class: _ _ _) #'(subclass?/c object%)] [(Value: '()) #'null?] - [(Struct: _ _ _ _ #f pred?) pred?] + [(Struct: _ _ _ _ #f pred? cert) (cert pred?)] [(Syntax: (Base: 'Symbol)) #'identifier?] [(Syntax: t) (if (equal? ty Any-Syntax) diff --git a/collects/typed-scheme/private/type-effect-convenience.ss b/collects/typed-scheme/private/type-effect-convenience.ss index 000c832533..bbf6008860 100644 --- a/collects/typed-scheme/private/type-effect-convenience.ss +++ b/collects/typed-scheme/private/type-effect-convenience.ss @@ -72,7 +72,7 @@ [(dom rng rest eff1 eff2) (make-arr dom rng rest eff1 eff2)])) (define (make-promise-ty t) - (make-Struct (string->uninterned-symbol "Promise") #f (list t) #f #f #'promise?)) + (make-Struct (string->uninterned-symbol "Promise") #f (list t) #f #f #'promise? values)) (define N (make-Base 'Number)) (define -Integer (make-Base 'Integer)) diff --git a/collects/typed-scheme/private/type-effect-printer.ss b/collects/typed-scheme/private/type-effect-printer.ss index cf5314c50d..22cccaab76 100644 --- a/collects/typed-scheme/private/type-effect-printer.ss +++ b/collects/typed-scheme/private/type-effect-printer.ss @@ -84,8 +84,8 @@ (fp "~a" (cons 'List (tuple-elems t)))] [(Base: n) (fp "~a" n)] [(Opaque: pred _) (fp "(Opaque ~a)" (syntax->datum pred))] - [(Struct: 'Promise par (list fld) proc _ _) (fp "(Promise ~a)" fld)] - [(Struct: nm par flds proc _ _) + [(Struct: 'Promise par (list fld) proc _ _ _) (fp "(Promise ~a)" fld)] + [(Struct: nm par flds proc _ _ _) (fp "#(struct:~a ~a" nm flds) (when proc (fp " ~a" proc)) diff --git a/collects/typed-scheme/private/type-rep.ss b/collects/typed-scheme/private/type-rep.ss index a09b1a669a..4c36abdf7f 100644 --- a/collects/typed-scheme/private/type-rep.ss +++ b/collects/typed-scheme/private/type-rep.ss @@ -66,7 +66,10 @@ ;; parent : Struct ;; flds : Listof[Type] ;; proc : Function Type - (dt Struct (name parent flds proc poly? pred-id) + ;; poly? : is this a polymorphic type? + ;; pred-id : identifier for the predicate of the struct + ;; cert : syntax certifier for pred-id + (dt Struct (name parent flds proc poly? pred-id cert) [#:intern (list name parent flds proc)] [#:frees (combine-frees (map free-vars* (append (if proc (list proc) null) (if parent (list parent) null) flds))) (combine-frees (map free-idxs* (append (if proc (list proc) null) (if parent (list parent) null) flds)))] @@ -75,7 +78,8 @@ (map type-rec-id flds) (and proc (type-rec-id proc)) poly? - pred-id)]) + pred-id + cert)]) ;; dom : Listof[Type] ;; rng : Type diff --git a/collects/typed-scheme/private/unify.ss b/collects/typed-scheme/private/unify.ss index afbc39504e..f1ebfd6193 100644 --- a/collects/typed-scheme/private/unify.ss +++ b/collects/typed-scheme/private/unify.ss @@ -72,7 +72,7 @@ [(list (list (Param: t1 t2) (Param: s1 s2)) rest ...) (unify/acc (list* (list t1 s1) (list t2 s2) rest) acc)] ;; structs - [(list (list (Struct: nm p elems proc _ _) (Struct: nm p elems* proc* _ _)) rest ...) + [(list (list (Struct: nm p elems proc _ _ _) (Struct: nm p elems* proc* _ _ _)) rest ...) (cond [(and proc proc*) (unify/acc (append rest (map list elems elems*) (list (list proc proc*))) acc)] [(or proc proc*) #f]