From 56732a6d6ed98a3fb51a4b2737ed485a41b028ef Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Fri, 26 Feb 2010 00:25:23 +0000 Subject: [PATCH] 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 --- .../typed-scheme/private/base-env-numeric.ss | 71 ++++++++++- collects/typed-scheme/private/base-env.ss | 87 +++----------- collects/typed-scheme/private/prims.ss | 14 ++- .../typed-scheme/private/type-contract.ss | 111 +++++++++--------- collects/typed-scheme/rep/object-rep.ss | 1 + collects/typed-scheme/typecheck/tc-envops.ss | 8 +- collects/typed-scheme/types/abbrev.ss | 1 + collects/typed-scheme/types/convenience.ss | 9 +- 8 files changed, 163 insertions(+), 139 deletions(-) diff --git a/collects/typed-scheme/private/base-env-numeric.ss b/collects/typed-scheme/private/base-env-numeric.ss index b123827e..e415a8de 100644 --- 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] diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss index 9d52f629..5649c444 100644 --- 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 diff --git a/collects/typed-scheme/private/prims.ss b/collects/typed-scheme/private/prims.ss index c85eb34c..b364c7b0 100644 --- 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) diff --git a/collects/typed-scheme/private/type-contract.ss b/collects/typed-scheme/private/type-contract.ss index bad2a41d..aaf679b6 100644 --- 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 diff --git a/collects/typed-scheme/rep/object-rep.ss b/collects/typed-scheme/rep/object-rep.ss index 9c7f93b5..9c5214b3 100644 --- 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)]) diff --git a/collects/typed-scheme/typecheck/tc-envops.ss b/collects/typed-scheme/typecheck/tc-envops.ss index e2ee9b83..832e6875 100644 --- 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)) diff --git a/collects/typed-scheme/types/abbrev.ss b/collects/typed-scheme/types/abbrev.ss index 49c7d942..c7af888c 100644 --- 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?)) diff --git a/collects/typed-scheme/types/convenience.ss b/collects/typed-scheme/types/convenience.ss index 4bcc4540..c4e9e96b 100644 --- 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)