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

Add `define-predicate'

Browse Source 
svn: r18497
This commit is contained in:
Sam Tobin-Hochstadt 2010-03-10 00:10:03 +00:00
parent 89aa9b6ed5
commit c24daa5dbb
6 changed files with 64 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
collects/tests/typed-scheme/succeed/def-pred.ss Normal file
View File

@ -0,0 +1,5 @@
#lang typed/scheme
(define-predicate int-or-bool? (U Integer Boolean))
(int-or-bool? 7)

4
collects/tests/typed-scheme/succeed/fix.ss
View File

@ -9,7 +9,7 @@
(: fact : (Number -> Number))
(define fact (make-recursive
(lambda: ([fact : (Number -> Number)])
(lambda: ([n : Number])
(if (zero? n)
(lambda: ([n : Number])
(if (zero? n)
1
(* n (fact (- n 1))))))))

25
collects/typed-scheme/private/prims.ss
View File

@ -109,6 +109,31 @@ This file defines two sorts of primitives. All of them are provided into any mod
#,(syntax-property #'(require/contract nm.spec cnt* lib)
'typechecker:ignore #t)))))]))
(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)))))
(syntax-property #'(define name #f)
'typechecker:flat-contract-def #'ty))
'typechecker:ignore #t)
;; not a require, this is just the unchecked declaration syntax
#,(internal #'(require/typed-internal name (Any -> Boolean : ty))))]))
(define-syntax (:type stx)
(syntax-parse stx
[(_ ty:expr)
#`(display #,(format "~a\n" (parse-type #'ty)))]))
(define-syntax (require/opaque-type stx)
(define-syntax-class name-exists-kw
(pattern #:name-exists))

19
collects/typed-scheme/private/type-contract.ss
View File

@ -4,6 +4,7 @@
(require
"../utils/utils.ss"
syntax/parse
(rep type-rep filter-rep object-rep)
(typecheck internal-forms)
(utils tc-utils require-contract)
@ -18,15 +19,16 @@
(define (define/fixup-contract? stx)
(or (syntax-property stx 'typechecker:contract-def)
(syntax-property stx 'typechecker:flat-contract-def)
(syntax-property stx 'typechecker:contract-def/maker)))
(define (generate-contract-def stx)
(define prop (or (syntax-property stx 'typechecker:contract-def)
(syntax-property stx 'typechecker:contract-def/maker)))
(define prop (define/fixup-contract? stx))
(define maker? (syntax-property stx 'typechecker:contract-def/maker))
(define flat? (syntax-property stx 'typechecker:flat-contract-def))
(define typ (parse-type prop))
(syntax-case stx (define-values)
[(_ (n) __)
(syntax-parse stx #:literals (define-values)
[(define-values (n) _)
(let ([typ (if maker?
((Struct-flds (lookup-type-name (Name-id typ))) #f . t:->* . typ)
typ)])
@ -34,6 +36,7 @@
typ
;; this is for a `require/typed', so the value is not from the typed side
#:typed-side #f
#:flat flat?
(lambda () (tc-error/stx prop "Type ~a could not be converted to a contract." typ)))])
(syntax/loc stx (define-values (n) cnt))))]
[_ (int-err "should never happen - not a define-values: ~a" (syntax->datum stx))]))
@ -49,7 +52,7 @@
(= (length l) (length (remove-duplicates l))))
(define (type->contract ty fail #:out [out? #f] #:typed-side [from-typed? #t])
(define (type->contract ty fail #:out [out? #f] #:typed-side [from-typed? #t] #:flat [flat? #f])
(define vars (make-parameter '()))
(let/ec exit
(let loop ([ty ty] [pos? #t] [from-typed? from-typed?] [structs-seen null])
@ -59,6 +62,7 @@
(match f
[(Function: (list (top-arr:))) #'procedure?]
[(Function: arrs)
(when flat? (exit (fail)))
(let ()
(define (f a)
(define-values (dom* opt-dom* rngs* rst)
@ -129,6 +133,7 @@
[(F: v) (cond [(assoc v (vars)) => second]
[else (int-err "unknown var: ~a" v)])]
[(Poly: vs (and b (Function: _)))
(when flat? (exit (fail)))
(match-let ([(Poly-names: vs-nm _) ty])
(with-syntax ([(v ...) (generate-temporaries vs-nm)])
(parameterize ([vars (append (map list vs (syntax->list #'(v ...)))
@ -139,13 +144,15 @@
(with-syntax ([(n*) (generate-temporaries (list n-nm))])
(parameterize ([vars (cons (list n #'n* #'n*) (vars))])
#`(flat-rec-contract n* #,(t->c b)))))]
[(Value: #f) #'false/c]
[(Value: #f) #'false/c]
[(Instance: (Class: _ _ (list (list name fcn) ...)))
(when flat? (exit (fail)))
(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) ...))
(when flat? (exit (fail)))
(with-syntax ([(fcn-cnts ...) (for/list ([f fcn]) (t->c/fun f #:method #t))]
[(names ...) name])
#'class?

18
collects/typed-scheme/rep/rep-utils.ss
View File

@ -249,4 +249,20 @@
(p/c (struct Rep ([seq exact-nonnegative-integer?]
[free-vars (hash/c symbol? variance?)]
[free-idxs (hash/c exact-nonnegative-integer? variance?)]
[stx (or/c #f syntax?)])))
[stx (or/c #f syntax?)]))
[replace-syntax (Rep? syntax? . -> . Rep?)])
(define (list-update l k v)
(if (zero? k)
(cons v (cdr l))
(cons (car l) (list-update (cdr l) (sub1 k) v))))
(define (replace-field val new-val idx)
(define-values (type skipped) (struct-info val))
(define maker (struct-type-make-constructor type))
(define flds (cdr (vector->list (struct->vector val))))
(apply maker (list-update flds idx new-val)))
(define (replace-syntax rep stx)
(replace-field rep stx 3))

3
collects/typed/scheme/base.ss
View File

@ -16,6 +16,7 @@
typed-scheme/private/base-env-indexing
typed-scheme/private/extra-procs
(for-syntax typed-scheme/private/base-types-extra))
(provide (rename-out [with-handlers: with-handlers])
(provide (rename-out [with-handlers: with-handlers]
[define-type-alias define-type])
assert with-type
(for-syntax (all-from-out typed-scheme/private/base-types-extra)))