From 20da55c55d5ac163672d4a669f14d4bb7f795331 Mon Sep 17 00:00:00 2001 From: Eric Dobson Date: Sun, 29 Jul 2012 12:00:55 -0700 Subject: [PATCH] Add tests for make-predicate and cast, also add support for the top-level. Closes PR 12939. Closes PR 12201. original commit: 533920480e4b9878a18febdc616429623bb58f50 --- .../tests/typed-racket/fail/cast-mod1.rkt | 6 + .../tests/typed-racket/fail/cast-mod2.rkt | 7 + .../tests/typed-racket/fail/cast-mod3.rkt | 7 + .../typed-racket/fail/cast-top-level1.rkt | 8 ++ .../typed-racket/fail/cast-top-level2.rkt | 9 ++ .../typed-racket/fail/make-predicate-mod1.rkt | 6 + .../typed-racket/fail/make-predicate-mod2.rkt | 7 + .../fail/make-predicate-top-level1.rkt | 7 + .../fail/make-predicate-top-level2.rkt | 8 ++ .../tests/typed-racket/succeed/cast-mod.rkt | 9 ++ .../typed-racket/succeed/cast-top-level.rkt | 11 ++ .../succeed/make-predicate-mod.rkt | 7 + .../succeed/make-predicate-top-level.rkt | 9 ++ collects/typed-racket/base-env/prims.rkt | 121 +++++++++++------- collects/typed-racket/core.rkt | 3 +- .../typed-racket/typecheck/tc-expr-unit.rkt | 2 +- .../typed-racket/typecheck/tc-toplevel.rkt | 7 +- 17 files changed, 178 insertions(+), 56 deletions(-) create mode 100644 collects/tests/typed-racket/fail/cast-mod1.rkt create mode 100644 collects/tests/typed-racket/fail/cast-mod2.rkt create mode 100644 collects/tests/typed-racket/fail/cast-mod3.rkt create mode 100644 collects/tests/typed-racket/fail/cast-top-level1.rkt create mode 100644 collects/tests/typed-racket/fail/cast-top-level2.rkt create mode 100644 collects/tests/typed-racket/fail/make-predicate-mod1.rkt create mode 100644 collects/tests/typed-racket/fail/make-predicate-mod2.rkt create mode 100644 collects/tests/typed-racket/fail/make-predicate-top-level1.rkt create mode 100644 collects/tests/typed-racket/fail/make-predicate-top-level2.rkt create mode 100644 collects/tests/typed-racket/succeed/cast-mod.rkt create mode 100644 collects/tests/typed-racket/succeed/cast-top-level.rkt create mode 100644 collects/tests/typed-racket/succeed/make-predicate-mod.rkt create mode 100644 collects/tests/typed-racket/succeed/make-predicate-top-level.rkt diff --git a/collects/tests/typed-racket/fail/cast-mod1.rkt b/collects/tests/typed-racket/fail/cast-mod1.rkt new file mode 100644 index 00000000..09c5ddff --- /dev/null +++ b/collects/tests/typed-racket/fail/cast-mod1.rkt @@ -0,0 +1,6 @@ +#; +(exn-pred exn:fail:contract? #rx".*produced: 3" #rx".*promised: String.*" ) + +#lang typed/racket/base + +(cast 3 String) diff --git a/collects/tests/typed-racket/fail/cast-mod2.rkt b/collects/tests/typed-racket/fail/cast-mod2.rkt new file mode 100644 index 00000000..3cf60802 --- /dev/null +++ b/collects/tests/typed-racket/fail/cast-mod2.rkt @@ -0,0 +1,7 @@ +#; +(exn-pred exn:fail:contract? #rx".*produced: 3" #rx".*promised: String.*" ) + +#lang typed/racket/base + +((cast (lambda () 3) (-> String))) + diff --git a/collects/tests/typed-racket/fail/cast-mod3.rkt b/collects/tests/typed-racket/fail/cast-mod3.rkt new file mode 100644 index 00000000..741e2899 --- /dev/null +++ b/collects/tests/typed-racket/fail/cast-mod3.rkt @@ -0,0 +1,7 @@ +#; +(exn-pred exn:fail:syntax? #rx".*free variables.*") + +#lang typed/racket/base + +(: f (All (a) (Number -> a))) +(define (f x) (cast x a)) diff --git a/collects/tests/typed-racket/fail/cast-top-level1.rkt b/collects/tests/typed-racket/fail/cast-top-level1.rkt new file mode 100644 index 00000000..0b1b10d3 --- /dev/null +++ b/collects/tests/typed-racket/fail/cast-top-level1.rkt @@ -0,0 +1,8 @@ +#; +(exn-pred exn:fail:syntax? #rx".*could not be converted.*") + +#lang racket/load + +(require typed/racket) + +(cast 2 (All (a) (Ephemeronof a))) diff --git a/collects/tests/typed-racket/fail/cast-top-level2.rkt b/collects/tests/typed-racket/fail/cast-top-level2.rkt new file mode 100644 index 00000000..cb92cba3 --- /dev/null +++ b/collects/tests/typed-racket/fail/cast-top-level2.rkt @@ -0,0 +1,9 @@ +#; +(exn-pred exn:fail:syntax? #rx".*Unbound type.*") + +#lang racket/load + +(require typed/racket/base) + +(define: (a) (f (x : Number)) : a + (cast x a)) diff --git a/collects/tests/typed-racket/fail/make-predicate-mod1.rkt b/collects/tests/typed-racket/fail/make-predicate-mod1.rkt new file mode 100644 index 00000000..0eea5b32 --- /dev/null +++ b/collects/tests/typed-racket/fail/make-predicate-mod1.rkt @@ -0,0 +1,6 @@ +#; +(exn-pred exn:fail:syntax? #rx".*could not be converted to a contract.*") + +#lang typed/racket/base + +(make-predicate (Number -> Number)) diff --git a/collects/tests/typed-racket/fail/make-predicate-mod2.rkt b/collects/tests/typed-racket/fail/make-predicate-mod2.rkt new file mode 100644 index 00000000..eaa8ebbe --- /dev/null +++ b/collects/tests/typed-racket/fail/make-predicate-mod2.rkt @@ -0,0 +1,7 @@ +#; +(exn-pred exn:fail:syntax? #rx".*free variables.*") + +#lang typed/racket/base + +(: f (All (a) (Number -> (Any -> Boolean : a)))) +(define (f x) (make-predicate a)) diff --git a/collects/tests/typed-racket/fail/make-predicate-top-level1.rkt b/collects/tests/typed-racket/fail/make-predicate-top-level1.rkt new file mode 100644 index 00000000..4b4de096 --- /dev/null +++ b/collects/tests/typed-racket/fail/make-predicate-top-level1.rkt @@ -0,0 +1,7 @@ +#; +(exn-pred exn:fail:syntax? #rx".*could not be converted to a predicate.*") + +#lang racket/load +(require typed/racket/base) + +(make-predicate (Number -> Number)) diff --git a/collects/tests/typed-racket/fail/make-predicate-top-level2.rkt b/collects/tests/typed-racket/fail/make-predicate-top-level2.rkt new file mode 100644 index 00000000..bb68446c --- /dev/null +++ b/collects/tests/typed-racket/fail/make-predicate-top-level2.rkt @@ -0,0 +1,8 @@ +#; +(exn-pred exn:fail:syntax? #rx".*Unbound type name.*") + +#lang racket/load +(require typed/racket/base) + +(: f (All (a) (Number -> (Any -> Boolean : a)))) +(define (f x) (make-predicate a)) diff --git a/collects/tests/typed-racket/succeed/cast-mod.rkt b/collects/tests/typed-racket/succeed/cast-mod.rkt new file mode 100644 index 00000000..2b3c4758 --- /dev/null +++ b/collects/tests/typed-racket/succeed/cast-mod.rkt @@ -0,0 +1,9 @@ +#lang typed/racket/base + +(cast 2 Number) +(cast 2 Integer) +(cast (list 2 4) (Listof Byte)) +(cast (vector 2 4) (Vectorof Byte)) + + +((cast (lambda (x) 7) (String -> Number)) "seven") diff --git a/collects/tests/typed-racket/succeed/cast-top-level.rkt b/collects/tests/typed-racket/succeed/cast-top-level.rkt new file mode 100644 index 00000000..b55f91f7 --- /dev/null +++ b/collects/tests/typed-racket/succeed/cast-top-level.rkt @@ -0,0 +1,11 @@ +#lang racket/load + +(require typed/racket/base) + +(cast 2 Number) +(cast 2 Integer) +(cast (list 2 4) (Listof Byte)) +(cast (vector 2 4) (Vectorof Byte)) + + +((cast (lambda (x) 7) (String -> Number)) "seven") diff --git a/collects/tests/typed-racket/succeed/make-predicate-mod.rkt b/collects/tests/typed-racket/succeed/make-predicate-mod.rkt new file mode 100644 index 00000000..8756c800 --- /dev/null +++ b/collects/tests/typed-racket/succeed/make-predicate-mod.rkt @@ -0,0 +1,7 @@ +#lang typed/racket/base + +(: f (Any -> Boolean : Number)) +(define f (make-predicate Number)) + +(: g (Listof Number)) +(define g (filter f '(1 2 3 4 "5"))) diff --git a/collects/tests/typed-racket/succeed/make-predicate-top-level.rkt b/collects/tests/typed-racket/succeed/make-predicate-top-level.rkt new file mode 100644 index 00000000..ff21ea8d --- /dev/null +++ b/collects/tests/typed-racket/succeed/make-predicate-top-level.rkt @@ -0,0 +1,9 @@ +#lang racket/load + +(require typed/racket) + +(: f (Any -> Boolean : Number)) +(define f (make-predicate Number)) + +(: g (Listof Number)) +(define g (filter f '(1 2 3 4 "5"))) diff --git a/collects/typed-racket/base-env/prims.rkt b/collects/typed-racket/base-env/prims.rkt index 41ec6ccd..70205d1f 100644 --- a/collects/typed-racket/base-env/prims.rkt +++ b/collects/typed-racket/base-env/prims.rkt @@ -176,21 +176,17 @@ This file defines two sorts of primitives. All of them are provided into any mod (begin (require-typed-struct nm . rest) (provide (struct-out nm)))])) +;; Conversion of types to contracts +;; define-predicate +;; make-predicate +;; cast (define-syntax (define-predicate stx) (syntax-parse stx [(_ name:id ty:expr) #`(begin #,(syntax-property (if (eq? (syntax-local-context) 'top-level) - (let ([typ (parse-type #'ty)]) - #`(define name - #,(type->contract - typ - ;; must be a flat contract - #:flat #t - ;; 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 predicate." typ))))) + #'(define name (procedure-rename (make-predicate ty) 'name)) (syntax-property #'(define name #f) 'typechecker:flat-contract-def #'ty)) 'typechecker:ignore #t) @@ -200,52 +196,81 @@ This file defines two sorts of primitives. All of them are provided into any mod (define-syntax (make-predicate stx) (syntax-parse stx [(_ ty:expr) - (let ((name (syntax-local-lift-expression - (syntax-property #'#f 'typechecker:flat-contract-def #'ty)))) - (define (check-valid-type _) - (define type (parse-type #'ty)) - (define vars (fv type)) - ;; If there was an error don't create another one - (unless (or (Error? type) (null? vars)) - (tc-error/delayed - "Type ~a could not be converted to a predicate because it contains free variables." - type))) + (if (syntax-transforming-module-expression?) + (let ((name (syntax-local-lift-expression + (syntax-property #'#f 'typechecker:flat-contract-def #'ty)))) + (define (check-valid-type _) + (define type (parse-type #'ty)) + (define vars (fv type)) + ;; If there was an error don't create another one + (unless (or (Error? type) (null? vars)) + (tc-error/delayed + "Type ~a could not be converted to a predicate because it contains free variables." + type))) - #`(ann - #,(syntax-property - (syntax-property name 'typechecker:ignore-some #t) - 'typechecker:external-check check-valid-type) + #`(ann + #,(syntax-property + (syntax-property name 'typechecker:ignore-some #t) + 'typechecker:external-check check-valid-type) - (Any -> Boolean : ty)))])) + (Any -> Boolean : ty))) + (let ([typ (parse-type #'ty)]) + (if (Error? typ) + ;; This code should never get run, typechecking will have an error earlier + #`(error 'make-predicate "Couldn't parse type") + #`(ann + #,(syntax-property + (type->contract + typ + ;; must be a flat contract + #:flat #t + ;; the value is not from the typed side + #:typed-side #f + (lambda () (tc-error/stx #'ty "Type ~a could not be converted to a predicate." typ))) + 'typechecker:ignore-some #t) + (Any -> Boolean : ty)))))])) (define-syntax (cast stx) (syntax-parse stx [(_ v:expr ty:expr) - (let ((ctc (syntax-local-lift-expression - (syntax-property #'#f 'typechecker:contract-def #'ty)))) - (define (check-valid-type _) - (define type (parse-type #'ty)) - (define vars (fv type)) - ;; If there was an error don't create another one - (unless (or (Error? type) (null? vars)) - (tc-error/delayed - "Type ~a could not be converted to a contract because it contains free variables." - type))) - (define body - (syntax-property - #`(let ((val #,(syntax-property #'(ann v Any) 'with-type #t))) - (contract - #,(syntax-property ctc 'typechecker:external-check check-valid-type) - val - 'cast - 'typed-world - val - (quote-syntax #,stx))) - 'typechecker:ignore-some #t)) - - #`(ann #,body ty))])) - + (define (apply-contract ctc-expr) + #`(ann + #,(syntax-property + #`(let-values (((val) #,(syntax-property #'(ann v Any) 'with-type #t))) + (contract + #,ctc-expr + val + 'cast + 'typed-world + val + (quote-syntax #,stx))) + 'typechecker:ignore-some #t) + ty)) + (if (syntax-transforming-module-expression?) + (let ((ctc (syntax-local-lift-expression + (syntax-property #'#f 'typechecker:contract-def #'ty)))) + (define (check-valid-type _) + (define type (parse-type #'ty)) + (define vars (fv type)) + ;; If there was an error don't create another one + (unless (or (Error? type) (null? vars)) + (tc-error/delayed + "Type ~a could not be converted to a contract because it contains free variables." + type))) + (syntax-property (apply-contract ctc) + 'typechecker:external-check check-valid-type)) + (let ([typ (parse-type #'ty)]) + (if (Error? typ) + ;; This code should never get run, typechecking will have an error earlier + #`(error 'cast "Couldn't parse type") + (apply-contract + (type->contract + typ + ;; 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)))))))])) (define-syntax (:type stx) diff --git a/collects/typed-racket/core.rkt b/collects/typed-racket/core.rkt index 57e5d92e..ed8c4610 100644 --- a/collects/typed-racket/core.rkt +++ b/collects/typed-racket/core.rkt @@ -90,8 +90,9 @@ (format "~a\n" cleaned)])))] [_ (error (format "~a: not a function" (syntax->datum #'op) ))])))] [(_ . form) + (init) (tc-setup - stx #'form 'top-level body2 init tc-toplevel-form before type + stx #'form 'top-level body2 void tc-toplevel-form before type (with-syntax* ([optimized-body (car (maybe-optimize #`(#,body2)))]) (syntax-parse body2 diff --git a/collects/typed-racket/typecheck/tc-expr-unit.rkt b/collects/typed-racket/typecheck/tc-expr-unit.rkt index 0f032ef7..2a7bcead 100644 --- a/collects/typed-racket/typecheck/tc-expr-unit.rkt +++ b/collects/typed-racket/typecheck/tc-expr-unit.rkt @@ -404,7 +404,7 @@ [stx #:when (syntax-property form 'typechecker:ignore-some) (check-subforms/ignore form) - Univ] + (ret Univ)] ;; explicit failure [(quote-syntax ((~literal typecheck-fail-internal) stx msg var)) (explicit-fail #'stx #'msg #'var)] diff --git a/collects/typed-racket/typecheck/tc-toplevel.rkt b/collects/typed-racket/typecheck/tc-toplevel.rkt index bee996f0..ee052c95 100644 --- a/collects/typed-racket/typecheck/tc-toplevel.rkt +++ b/collects/typed-racket/typecheck/tc-toplevel.rkt @@ -186,11 +186,6 @@ (syntax-property form 'typechecker:ignore) (void)] - ;; this is a form that we mostly ignore, but we check some interior parts - [stx - (syntax-property form 'typechecker:ignore-some) - (check-subforms/ignore form)] - ;; these forms should always be ignored [(#%require . _) (void)] [(#%provide . _) (void)] @@ -372,7 +367,7 @@ ;; typecheck a top-level form ;; used only from #%top-interaction -;; syntax -> void +;; syntax -> (values #f (or/c void? tc-results?)) (define (tc-toplevel-form form) (tc-toplevel/pass1 form) (begin0 (values #f (tc-toplevel/pass2 form))