suzanne.soy/typed-racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Add tests for make-predicate and cast, also add support for the top-level.

Browse Source 
Closes PR 12939.
Closes PR 12201.

original commit: 533920480e4b9878a18febdc616429623bb58f50
This commit is contained in:
Eric Dobson 2012-07-29 12:00:55 -07:00 committed by Sam Tobin-Hochstadt
parent 9d60643a65
commit 20da55c55d
17 changed files with 178 additions and 56 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
collects/tests/typed-racket/fail/cast-mod1.rkt Normal file
View File

@ -0,0 +1,6 @@
#;
(exn-pred exn:fail:contract? #rx".*produced: 3" #rx".*promised: String.*" )
#lang typed/racket/base
(cast 3 String)

7
collects/tests/typed-racket/fail/cast-mod2.rkt Normal file
View File

@ -0,0 +1,7 @@
#;
(exn-pred exn:fail:contract? #rx".*produced: 3" #rx".*promised: String.*" )
#lang typed/racket/base
((cast (lambda () 3) (-> String)))

7
collects/tests/typed-racket/fail/cast-mod3.rkt Normal file
View File

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

8
collects/tests/typed-racket/fail/cast-top-level1.rkt Normal file
View File

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

9
collects/tests/typed-racket/fail/cast-top-level2.rkt Normal file
View File

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

6
collects/tests/typed-racket/fail/make-predicate-mod1.rkt Normal file
View File

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

7
collects/tests/typed-racket/fail/make-predicate-mod2.rkt Normal file
View File

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

7
collects/tests/typed-racket/fail/make-predicate-top-level1.rkt Normal file
View File

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

8
collects/tests/typed-racket/fail/make-predicate-top-level2.rkt Normal file
View File

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

9
collects/tests/typed-racket/succeed/cast-mod.rkt Normal file
View File

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

11
collects/tests/typed-racket/succeed/cast-top-level.rkt Normal file
View File

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

7
collects/tests/typed-racket/succeed/make-predicate-mod.rkt Normal file
View File

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

9
collects/tests/typed-racket/succeed/make-predicate-top-level.rkt Normal file
View File

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

121
collects/typed-racket/base-env/prims.rkt
View File

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

3
collects/typed-racket/core.rkt
View File

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

2
collects/typed-racket/typecheck/tc-expr-unit.rkt
View File

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

7
collects/typed-racket/typecheck/tc-toplevel.rkt
View File

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