Add way for code to attach typechecks to itself, and implemented make-predicate.

This commit is contained in:
Eric Dobson 2012-07-26 23:37:23 -07:00 committed by Sam Tobin-Hochstadt
parent 115345300d
commit cc52e56fe6
2 changed files with 33 additions and 3 deletions

View File

@ -50,12 +50,13 @@ This file defines two sorts of primitives. All of them are provided into any mod
"annotate-classes.rkt" "annotate-classes.rkt"
"internal.rkt" "internal.rkt"
"../utils/tc-utils.rkt" "../utils/tc-utils.rkt"
"../types/utils.rkt"
"for-clauses.rkt") "for-clauses.rkt")
"../types/numeric-predicates.rkt") "../types/numeric-predicates.rkt")
(provide index?) ; useful for assert, and racket doesn't have it (provide index?) ; useful for assert, and racket doesn't have it
(begin-for-syntax (begin-for-syntax
(lazy-require ["../rep/type-rep.rkt" (make-Opaque)] (lazy-require ["../rep/type-rep.rkt" (make-Opaque Error?)]
[syntax/define (normalize-definition)])) [syntax/define (normalize-definition)]))
(define-for-syntax (ignore stx) (syntax-property stx 'typechecker:ignore #t)) (define-for-syntax (ignore stx) (syntax-property stx 'typechecker:ignore #t))
@ -196,6 +197,28 @@ This file defines two sorts of primitives. All of them are provided into any mod
;; not a require, this is just the unchecked declaration syntax ;; not a require, this is just the unchecked declaration syntax
#,(internal #'(require/typed-internal name (Any -> Boolean : ty))))])) #,(internal #'(require/typed-internal name (Any -> Boolean : ty))))]))
(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)))
#`(ann
#,(syntax-property
(syntax-property name 'typechecker:ignore-some #t)
'typechecker:external-check check-valid-type)
(Any -> Boolean : ty)))]))
(define-syntax (:type stx) (define-syntax (:type stx)
(error ":type is only valid at the top-level of an interaction")) (error ":type is only valid at the top-level of an interaction"))
(define-syntax (:print-type stx) (define-syntax (:print-type stx)

View File

@ -239,6 +239,13 @@
(check-below ts** expected))] (check-below ts** expected))]
;; no annotations possible on dotted results ;; no annotations possible on dotted results
[ty (add-typeof-expr form ty) ty])] [ty (add-typeof-expr form ty) ty])]
[(syntax-property form* 'typechecker:external-check)
=>
(lambda (check)
(check form*)
(loop (syntax-property form* 'typechecker:external-check #f)
expected
checked?))]
;; nothing to see here ;; nothing to see here
[checked? expected] [checked? expected]
[else [else