From e70c2dea514cb15d5b60b1f73c4196352101dab1 Mon Sep 17 00:00:00 2001 From: Eric Dobson Date: Thu, 26 Jul 2012 23:37:23 -0700 Subject: [PATCH] Add way for code to attach typechecks to itself, and implemented make-predicate. original commit: cc52e56fe6749bba71dbae5e56c0a58d90ac119b --- collects/typed-racket/base-env/prims.rkt | 29 +++++++++++++++++-- .../typed-racket/typecheck/tc-expr-unit.rkt | 7 +++++ 2 files changed, 33 insertions(+), 3 deletions(-) diff --git a/collects/typed-racket/base-env/prims.rkt b/collects/typed-racket/base-env/prims.rkt index f7e6e339..11864c67 100644 --- a/collects/typed-racket/base-env/prims.rkt +++ b/collects/typed-racket/base-env/prims.rkt @@ -39,7 +39,7 @@ This file defines two sorts of primitives. All of them are provided into any mod (rename-in racket/contract/base [-> c->] [case-> c:case->]) "base-types.rkt" "base-types-extra.rkt" - racket/flonum ; for for/flvector and for*/flvector + racket/flonum ; for for/flvector and for*/flvector (for-syntax unstable/lazy-require syntax/parse @@ -50,12 +50,13 @@ This file defines two sorts of primitives. All of them are provided into any mod "annotate-classes.rkt" "internal.rkt" "../utils/tc-utils.rkt" + "../types/utils.rkt" "for-clauses.rkt") "../types/numeric-predicates.rkt") (provide index?) ; useful for assert, and racket doesn't have it (begin-for-syntax - (lazy-require ["../rep/type-rep.rkt" (make-Opaque)] + (lazy-require ["../rep/type-rep.rkt" (make-Opaque Error?)] [syntax/define (normalize-definition)])) (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 #,(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) (error ":type is only valid at the top-level of an interaction")) (define-syntax (:print-type stx) @@ -855,7 +878,7 @@ This file defines two sorts of primitives. All of them are provided into any mod (define ((mk l/c) stx) (syntax-parse stx [(_ (~var k (param-annotated-name (lambda (s) #`(#,s -> (U))))) . body) - (quasisyntax/loc stx (#,l/c k.ann-name . body))])) + (quasisyntax/loc stx (#,l/c k.ann-name . body))])) (values (mk #'let/cc) (mk #'let/ec)))) ;; annotation to help tc-expr pick out keyword functions diff --git a/collects/typed-racket/typecheck/tc-expr-unit.rkt b/collects/typed-racket/typecheck/tc-expr-unit.rkt index e4a18662..0f032ef7 100644 --- a/collects/typed-racket/typecheck/tc-expr-unit.rkt +++ b/collects/typed-racket/typecheck/tc-expr-unit.rkt @@ -239,6 +239,13 @@ (check-below ts** expected))] ;; no annotations possible on dotted results [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 [checked? expected] [else