Add a cert to go with the struct predicate.

svn: r10061

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)]       

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*))]

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*)

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)
+    [(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))]
+     `(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))]

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

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)

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? 

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)

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))

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: 'Promise par (list fld) proc _ _ _) (fp "(Promise ~a)" fld)]      
-    [(Struct: nm par flds proc _ _) 
+    [(Struct: nm par flds proc _ _ _) 
      (fp "#(struct:~a ~a" nm flds)
      (when proc
        (fp " ~a" proc))

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

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]