Re-enable typechecking of auto-language.ss

Add `syntax-e' as a path. Turn on contracts for objects. Refactor Noel's additions. Fix `require/typed' at the REPL. svn: r18345 original commit: 2e90dfc081a3160abaa49aff9f535a901999c6a5
2010-02-26 00:25:23 +00:00 · 2010-02-26 00:25:23 +00:00 · 56732a6d6e
commit 56732a6d6e
parent bb22e41f6d
8 changed files with 163 additions and 139 deletions
--- a/collects/typed-scheme/private/base-env-numeric.ss
+++ b/collects/typed-scheme/private/base-env-numeric.ss
@ -16,9 +16,24 @@
  
  (define-for-syntax all-num-types (list -Pos -Nat -Integer -ExactRational -Flonum -Real N))

-  (define-for-syntax fl-comp (-> -Flonum -Flonum B))
-  (define-for-syntax fl-op (-> -Flonum -Flonum -Flonum))
-  (define-for-syntax fl-unop (-> -Flonum -Flonum))
+  (define-for-syntax binop 
+    (lambda (t [r t])
+      (t t . -> . r)))
+  
+  (define-for-syntax (unop t) (-> t t))
+  
+  (define-for-syntax fl-comp (binop -Flonum B))
+  (define-for-syntax fl-op (binop -Flonum))
+  (define-for-syntax fl-unop (unop -Flonum))
+  
+  
+  (define-for-syntax int-op (binop -Integer))
+  (define-for-syntax nat-op (binop -Nat))
+  
+  (define-for-syntax fx-comp (binop -Integer B))
+  (define-for-syntax fx-op (cl->* nat-op int-op))
+  (define-for-syntax fx-intop int-op)
+  (define-for-syntax fx-unop (unop -Integer))

  (define-for-syntax real-comp (->* (list R R) R B))
  )
@ -159,6 +174,56 @@
 [unsafe-fl> fl-comp]
 [unsafe-fl< fl-comp]

+
+[unsafe-fx+ fx-op]
+[unsafe-fx- fx-intop]
+[unsafe-fx* fx-op]
+[unsafe-fxquotient fx-intop]
+[unsafe-fxremainder fx-intop]
+[unsafe-fxmodulo fx-intop]
+[unsafe-fxabs (-Integer . -> . -Nat)]
+
+[unsafe-fxand fx-intop]
+[unsafe-fxior fx-intop]
+[unsafe-fxxor fx-intop]
+[unsafe-fxnot fx-unop]
+[unsafe-fxlshift fx-intop]
+[unsafe-fxrshift fx-intop]
+
+[unsafe-fx= fx-comp]
+[unsafe-fx< fx-comp]
+[unsafe-fx> fx-comp]
+[unsafe-fx<= fx-comp]
+[unsafe-fx>= fx-comp]
+[unsafe-fxmin fx-op]
+[unsafe-fxmax fx-op]
+
+;; scheme/fixnum
+
+[fx+ fx-op]
+[fx- fx-intop]
+[fx* fx-op]
+[fxquotient fx-intop]
+[fxremainder fx-intop]
+[fxmodulo fx-intop]
+[fxabs (-Integer . -> . -Nat)]
+
+[fxand fx-intop]
+[fxior fx-intop]
+[fxxor fx-intop]
+[fxnot fx-unop]
+[fxlshift fx-intop]
+[fxrshift fx-intop]
+
+[fx= fx-comp]
+[fx< fx-comp]
+[fx> fx-comp]
+[fx<= fx-comp]
+[fx>= fx-comp]
+[fxmin fx-op]
+[fxmax fx-op]
+
+
 ;; safe flonum ops
 [flabs fl-unop]
 [flsqrt fl-unop]
--- a/collects/typed-scheme/private/base-env.ss
+++ b/collects/typed-scheme/private/base-env.ss
@ -16,6 +16,19 @@
             (only-in (rep type-rep) make-HashtableTop make-MPairTop make-BoxTop make-VectorTop)))

 [raise (Univ . -> . (Un))]
+[raise-syntax-error (cl->* 
+                     (-> (Un (-val #f) -Symbol)
+                               -String
+                               (Un))
+                     (-> (Un (-val #f) -Symbol)
+                               -String
+                               Univ
+                               (Un))
+                     (-> (Un (-val #f) -Symbol)
+                               -String
+                               Univ
+                               Univ
+                               (Un)))]

 [car   (-poly (a b) 
              (cl->*
@ -512,7 +525,7 @@

 [syntax->datum (cl->* (-> Any-Syntax -Sexp)
                      (-> (-Syntax Univ) Univ))]
-[syntax-e (-poly (a) (-> (-Syntax a) a))]
+[syntax-e (-poly (a) (->acc (list (-Syntax a)) a (list -syntax-e)))]
 [syntax-original? (-poly (a) (-> (-Syntax a) B))]
 [identifier? (make-pred-ty (-Syntax Sym))]
 [syntax? (make-pred-ty (-Syntax Univ))]
@ -651,78 +664,6 @@
              (cl->*
               (->acc (list (-pair a b)) b (list -cdr))))]

-[unsafe-fx+
- (cl->
-  [(-Nat -Nat) -Nat]
-  [(-Integer -Integer) -Integer])]
-[unsafe-fx- (-Integer -Integer . -> . -Integer)]
-[unsafe-fx*
- (cl->
-  [(-Nat -Nat) -Nat]
-  [(-Integer -Integer) -Integer])]
-[unsafe-fxquotient (-Integer -Integer . -> . -Integer)]
-[unsafe-fxremainder (-Integer -Integer . -> . -Integer)]
-[unsafe-fxmodulo (-Integer -Integer . -> . -Integer)]
-[unsafe-fxabs (-Integer . -> . -Nat)]
-
-[unsafe-fxand (-Integer -Integer . -> . -Integer)]
-[unsafe-fxior (-Integer -Integer . -> . -Integer)]
-[unsafe-fxxor (-Integer -Integer . -> . -Integer)]
-[unsafe-fxnot (-Integer . -> . -Integer)]
-[unsafe-fxlshift (-Integer -Integer . -> . -Integer)]
-[unsafe-fxrshift (-Integer -Integer . -> . -Integer)]
-
-[unsafe-fx= (-Integer -Integer . -> . -Boolean)]
-[unsafe-fx< (-Integer -Integer . -> . -Boolean)]
-[unsafe-fx> (-Integer -Integer . -> . -Boolean)]
-[unsafe-fx<= (-Integer -Integer . -> . -Boolean)]
-[unsafe-fx>= (-Integer -Integer . -> . -Boolean)]
-[unsafe-fxmin
- (cl->
-  [(-Nat -Nat) -Nat]
-  [(-Integer -Integer) -Integer])]
-[unsafe-fxmax
- (cl->
-  [(-Nat -Nat) -Nat]
-  [(-Integer -Integer) -Integer])]
-
-;; scheme/fixnum
-
-[fx+
- (cl->
-  [(-Nat -Nat) -Nat]
-  [(-Integer -Integer) -Integer])]
-[fx- (-Integer -Integer . -> . -Integer)]
-[fx*
- (cl->
-  [(-Nat -Nat) -Nat]
-  [(-Integer -Integer) -Integer])]
-[fxquotient (-Integer -Integer . -> . -Integer)]
-[fxremainder (-Integer -Integer . -> . -Integer)]
-[fxmodulo (-Integer -Integer . -> . -Integer)]
-[fxabs (-Integer . -> . -Nat)]
-
-[fxand (-Integer -Integer . -> . -Integer)]
-[fxior (-Integer -Integer . -> . -Integer)]
-[fxxor (-Integer -Integer . -> . -Integer)]
-[fxnot (-Integer . -> . -Integer)]
-[fxlshift (-Integer -Integer . -> . -Integer)]
-[fxrshift (-Integer -Integer . -> . -Integer)]
-
-[fx= (-Integer -Integer . -> . -Boolean)]
-[fx< (-Integer -Integer . -> . -Boolean)]
-[fx> (-Integer -Integer . -> . -Boolean)]
-[fx<= (-Integer -Integer . -> . -Boolean)]
-[fx>= (-Integer -Integer . -> . -Boolean)]
-[fxmin
- (cl->
-  [(-Nat -Nat) -Nat]
-  [(-Integer -Integer) -Integer])]
-[fxmax
- (cl->
-  [(-Nat -Nat) -Nat]
-  [(-Integer -Integer) -Integer])]
-
 ;; scheme/vector
 [vector-count (-polydots (a b)
                         ((list
--- a/collects/typed-scheme/private/prims.ss
+++ b/collects/typed-scheme/private/prims.ss
@ -94,11 +94,19 @@ This file defines two sorts of primitives. All of them are provided into any mod
                            'typechecker:contract-def)])
         (quasisyntax/loc stx 
           (begin 
-             #,(syntax-property (syntax-property #'(define cnt #f)
-                                                 prop-name #'ty)
+             #,(syntax-property (if (eq? (syntax-local-context) 'top-level)
+                                    (let ([typ (parse-type #'ty)])
+                                      #`(define cnt* 
+                                          #,(type->contract 
+                                             typ 
+                                             ;; this is for a `require/typed', so the value is not from the typed side
+                                             #:typed-side #f 
+                                             (lambda () (tc-error/stx #'ty "Type ~a could not be converted to a contract." typ)))))
+                                    (syntax-property #'(define cnt* #f)
+                                                 prop-name #'ty))
                                'typechecker:ignore #t)
             #,(internal #'(require/typed-internal nm.nm ty . sm))
-             #,(syntax-property #'(require/contract nm.spec cnt lib)
+             #,(syntax-property #'(require/contract nm.spec cnt* lib)
                                'typechecker:ignore #t)))))]))

 (define-syntax (require/opaque-type stx)
--- a/collects/typed-scheme/private/type-contract.ss
+++ b/collects/typed-scheme/private/type-contract.ss
@ -1,6 +1,6 @@
 #lang scheme/base

-(provide type->contract define/fixup-contract? generate-contract-def change-contract-fixups)
+(provide type->contract define/fixup-contract? change-contract-fixups)

 (require
 "../utils/utils.ss"
@ -11,10 +11,10 @@
 (types resolve utils)
 (prefix-in t: (types convenience))
 (private parse-type)
- scheme/match syntax/struct syntax/stx mzlib/trace unstable/syntax scheme/list
+ scheme/match syntax/struct syntax/stx mzlib/trace unstable/syntax scheme/list 
 (only-in scheme/contract -> ->* case-> cons/c flat-rec-contract provide/contract any/c)
 (for-template scheme/base scheme/contract unstable/poly-c (utils any-wrap)
-	       (only-in scheme/class object% is-a?/c subclass?/c object-contract)))
+	       (only-in scheme/class object% is-a?/c subclass?/c object-contract class/c object/c class?)))

 (define (define/fixup-contract? stx)
  (or (syntax-property stx 'typechecker:contract-def)
@ -55,12 +55,50 @@
    (let loop ([ty ty] [pos? #t] [from-typed? from-typed?] [structs-seen null])
      (define (t->c t #:seen [structs-seen structs-seen]) (loop t pos? from-typed? structs-seen))
      (define (t->c/neg t #:seen [structs-seen structs-seen]) (loop t (not pos?) (not from-typed?) structs-seen))
+      (define (t->c/fun f #:method [method? #f])
+        (match f
+          [(Function: arrs)
+           (let ()           
+             (define (f a)
+               (define-values (dom* opt-dom* rngs* rst)
+                 (match a
+                   ;; functions with no filters or objects
+                   [(arr: dom (Values: (list (Result: rngs (LFilterSet: '() '()) (LEmpty:)) ...)) rst #f kws)
+                    (let-values ([(mand-kws opt-kws) (partition (match-lambda [(Keyword: _ _ mand?) mand?]) kws)]
+                                 [(conv) (match-lambda [(Keyword: kw kty _) (list kw (t->c/neg kty))])])
+                      (values (append (map t->c/neg dom) (append-map conv mand-kws))
+                              (append-map conv opt-kws)
+                              (map t->c rngs) 
+                              (and rst (t->c/neg rst))))]
+                   ;; functions with filters or objects
+                   [(arr: dom (Values: (list (Result: rngs _ _) ...)) rst #f '())
+                    (if (and out? pos?)
+                        (values (map t->c/neg dom)
+                                null
+                                (map t->c rngs)
+                                (and rst (t->c/neg rst)))
+                        (exit (fail)))]
+                   [_ (exit (fail))]))
+               (with-syntax 
+                   ([(dom* ...) (if method? (cons #'any/c dom*) dom*)]
+                    [(opt-dom* ...) opt-dom*]
+                    [rng* (match rngs*
+                            [(list r) r]
+                            [_ #`(values #,@rngs*)])]
+                    [rst* rst])
+                 (if (or rst (pair? (syntax-e #'(opt-dom* ...))))
+                     #'((dom* ...) (opt-dom* ...) #:rest (listof rst*) . ->* . rng*)
+                     #'(dom* ... . -> . rng*))))
+             (unless (no-duplicates (for/list ([t arrs])
+                                      (match t [(arr: dom _ _ _ _) (length dom)])))
+               (exit (fail)))
+             (match (map f arrs)
+               [(list e) e]
+               [l #`(case-> #,@l)]))]))
      (match ty
        [(or (App: _ _ _) (Name: _)) (t->c (resolve-once ty))]
        ;; any/c doesn't provide protection in positive position
-        [(Univ:) (if from-typed? 
-                     #'any-wrap/c
-                     #'any/c)]
+        [(Univ:) (if from-typed? #'any-wrap/c #'any/c)]
        ;; we special-case lists:
        [(Mu: var (Union: (list (Value: '()) (Pair: elem-ty (F: var)))))
         #`(listof #,(t->c elem-ty))]
@ -69,51 +107,12 @@
        [(Refinement: par p? cert)
         #`(and/c #,(t->c par) (flat-contract #,(cert p?)))]
        [(Union: elems)         
-         (let-values ([(vars notvars)
-                       (partition F? elems)])
+         (let-values ([(vars notvars) (partition F? elems)])
           (unless (>= 1 (length vars)) (exit (fail)))
           (with-syntax 
               ([cnts (append (map t->c vars) (map t->c notvars))])
             #'(or/c . cnts)))]
-        [(Function: arrs)
-         (let ()           
-           (define (f a)
-             (define-values (dom* opt-dom* rngs* rst)
-               (match a
-                 ;; functions with no filters or objects
-                 [(arr: dom (Values: (list (Result: rngs (LFilterSet: '() '()) (LEmpty:)) ...)) rst #f kws)
-                  (let-values ([(mand-kws opt-kws) (partition (match-lambda [(Keyword: _ _ mand?) mand?]) kws)]
-                               [(conv) (match-lambda [(Keyword: kw kty _) (list kw (t->c/neg kty))])])
-                    (values (append (map t->c/neg dom) (append-map conv mand-kws))
-                            (append-map conv opt-kws)
-                            (map t->c rngs) 
-                            (and rst (t->c/neg rst))))]
-                 ;; functions with filters or objects
-                 [(arr: dom (Values: (list (Result: rngs _ _) ...)) rst #f '())
-                  (if (and out? pos?)
-                      (values (map t->c/neg dom)
-                              null
-                              (map t->c rngs)
-                              (and rst (t->c/neg rst)))
-                      (exit (fail)))]
-                 [_ (exit (fail))]))
-             (trace f)
-             (with-syntax 
-                 ([(dom* ...) dom*]
-                  [(opt-dom* ...) opt-dom*]
-                  [rng* (match rngs*
-                          [(list r) r]
-                          [_ #`(values #,@rngs*)])]
-                  [rst* rst])
-               (if (or rst (pair? (syntax-e #'(opt-dom* ...))))
-                   #'((dom* ...) (opt-dom* ...) #:rest (listof rst*) . ->* . rng*)
-                   #'(dom* ... . -> . rng*))))
-           (unless (no-duplicates (for/list ([t arrs])
-                                    (match t [(arr: dom _ _ _ _) (length dom)])))
-             (exit (fail)))
-	   (match (map f arrs)
-	     [(list e) e]
-	     [l #`(case-> #,@l)]))]
+        [(and t (Function: _)) (t->c/fun t)]
        [(Vector: t)
         #`(vectorof #,(t->c t))]
        [(Box: t)
@ -129,7 +128,7 @@
           (with-syntax ([(v ...) (generate-temporaries vs-nm)])
             (parameterize ([vars (append (map list vs (syntax->list #'(v ...)))
 					  (vars))])
-               #`(poly/c (v ...) #,(t->c b)))))]
+               #`(parametric/c (v ...) #,(t->c b)))))]
        [(Mu: n b)
         (match-let ([(Mu-name: n-nm _) ty])
           (with-syntax ([(n*) (generate-temporaries (list n-nm))])
@ -137,12 +136,16 @@
               #`(flat-rec-contract n* #,(t->c b)))))]
        [(Value: #f) #'false/c]    
        [(Instance: (Class: _ _ (list (list name fcn) ...)))
-         #'(is-a?/c object%)
-         #;
-	 (with-syntax ([(fcn-cnts ...) (map t->c fcn)]
-		       [(names ...) name])
-		      #'(object-contract (names fcn-cnts) ...))]
-        [(Class: _ _ _) #'(subclass?/c object%)]
+         (with-syntax ([(fcn-cnts ...) (for/list ([f fcn]) (t->c/fun f #:method #t))]
+                       [(names ...) name])
+           #'(object/c (names fcn-cnts) ...))]
+        ;; init args not currently handled by class/c
+        [(Class: _ _ (list (list name fcn) ...))
+         (with-syntax ([(fcn-cnts ...) (for/list ([f fcn]) (t->c/fun f #:method #t))]
+                       [(names ...) name])
+           #'class?
+           #;
+           #'(class/c (names fcn-cnts) ...))]
        [(Value: '()) #'null?]
        [(Struct: nm par flds proc poly? pred? cert acc-ids)
         (cond 
--- a/collects/typed-scheme/rep/object-rep.ss
+++ b/collects/typed-scheme/rep/object-rep.ss
@ -4,6 +4,7 @@

 (dpe CarPE () [#:fold-rhs #:base])
 (dpe CdrPE () [#:fold-rhs #:base])
+(dpe SyntaxPE () [#:fold-rhs #:base])
 (dpe StructPE ([t Type?] [idx natural-number/c])     
    [#:frees (free-vars* t) (free-idxs* t)]
    [#:fold-rhs (*StructPE (type-rec-id t) idx)])
--- a/collects/typed-scheme/typecheck/tc-envops.ss
+++ b/collects/typed-scheme/typecheck/tc-envops.ss
@ -6,7 +6,7 @@
                    [->* -->*]
                    [one-of/c -one-of/c])
         (infer-in infer)
-         (rep type-rep)
+         (rep type-rep object-rep)
         (utils tc-utils)
         (types resolve)
         (only-in (env type-environments lexical-env) env? update-type/lexical env-map env-props replace-props)
@ -37,6 +37,12 @@
    [((Pair: t s) (NotTypeFilter: u (list rst ... (CdrPE:)) x))
     (make-Pair t (update s (make-NotTypeFilter u rst x)))]
    
+    ;; syntax ops
+    [((Syntax: t) (TypeFilter: u (list rst ... (SyntaxPE:)) x))
+     (make-Syntax (update t (make-TypeFilter u rst x)))]
+    [((Syntax: t) (NotTypeFilter: u (list rst ... (SyntaxPE:)) x))
+     (make-Syntax (update t (make-NotTypeFilter u rst x)))]
+    
    ;; struct ops
    [((Struct: nm par flds proc poly pred cert acc-ids) 
      (TypeFilter: u (list rst ... (StructPE: (? (lambda (s) (subtype t s)) s) idx)) x))     
--- a/collects/typed-scheme/types/abbrev.ss
+++ b/collects/typed-scheme/types/abbrev.ss
@ -119,6 +119,7 @@

 (define -car (make-CarPE))
 (define -cdr (make-CdrPE))
+(define -syntax-e (make-SyntaxPE))

 ;; Numeric hierarchy
 (define -Number (make-Base 'Number #'number?))
--- a/collects/typed-scheme/types/convenience.ss
+++ b/collects/typed-scheme/types/convenience.ss
@ -47,13 +47,12 @@

 (define In-Syntax
  (-mu e
-       (*Un -Boolean -Symbol -String -Keyword -Char -Number
+       (*Un -Boolean -Symbol -String -Keyword -Char -Number (-val null)
            (make-Vector (-Syntax e))
            (make-Box (-Syntax e))
-            (-mu list
-                 (*Un (-val '())
-                      (-pair (-Syntax e)
-                             (*Un (-Syntax e) list)))))))
+            (-lst (-Syntax e))
+            (-pair (-Syntax e) (-Syntax e)))))
+
 (define Any-Syntax (-Syntax In-Syntax))

 (define (-Sexpof t)