First step to polymorphic functions in typed/untyped interface

- poly/c contract from Carl/Stevie
- generate the contracts
- test
- use in typed/srfi/14

svn: r14241
This commit is contained in:
Sam Tobin-Hochstadt 2009-03-23 18:29:07 +00:00
parent 6108dc873c
commit 60e096913d
5 changed files with 124 additions and 28 deletions

View File

@ -0,0 +1,15 @@
#;
(exn-pred exn:fail:contract? ".*interface for bad-map.*")
#lang scheme/load
(module bad-map scheme
(provide bad-map)
(define (bad-map f l)
(list (f 'quux))))
(module use-bad-map typed-scheme
(require/typed 'bad-map
[bad-map (All (A B) ((A -> B) (Listof A) -> (Listof B)))])
(bad-map add1 (list 12 13 14)))
(require 'use-bad-map)

View File

@ -20,7 +20,7 @@
mzlib/trace mzlib/trace
scheme/list scheme/list
(only-in scheme/contract -> ->* case-> cons/c flat-rec-contract provide/contract any/c) (only-in scheme/contract -> ->* case-> cons/c flat-rec-contract provide/contract any/c)
(for-template scheme/base scheme/contract (only-in scheme/class object% is-a?/c subclass?/c))) (for-template scheme/base scheme/contract (utils poly-c) (only-in scheme/class object% is-a?/c subclass?/c)))
(define (define/fixup-contract? stx) (define (define/fixup-contract? stx)
(or (syntax-property stx 'typechecker:contract-def) (or (syntax-property stx 'typechecker:contract-def)
@ -54,7 +54,9 @@
(define (type->contract ty fail) (define (type->contract ty fail)
(define vars (make-parameter '())) (define vars (make-parameter '()))
(let/cc exit (let/cc exit
(let t->c ([ty ty]) (let loop ([ty ty] [pos? #t])
(define (t->c t) (loop t pos?))
(define (t->c/neg t) (loop t (not pos?)))
(match ty (match ty
[(or (App: _ _ _) (Name: _)) (t->c (resolve-once ty))] [(or (App: _ _ _) (Name: _)) (t->c (resolve-once ty))]
[(Univ:) #'any/c] [(Univ:) #'any/c]
@ -74,13 +76,13 @@
(define-values (dom* rngs* rst) (define-values (dom* rngs* rst)
(match a (match a
[(arr: dom (Values: rngs) #f #f '() _ _) [(arr: dom (Values: rngs) #f #f '() _ _)
(values (map t->c dom) (map t->c rngs) #f)] (values (map t->c/neg dom) (map t->c rngs) #f)]
[(arr: dom rng #f #f '() _ _) [(arr: dom rng #f #f '() _ _)
(values (map t->c dom) (list (t->c rng)) #f)] (values (map t->c/neg dom) (list (t->c rng)) #f)]
[(arr: dom (Values: rngs) rst #f '() _ _) [(arr: dom (Values: rngs) rst #f '() _ _)
(values (map t->c dom) (map t->c rngs) (t->c rst))] (values (map t->c/neg dom) (map t->c rngs) (t->c/neg rst))]
[(arr: dom rng rst #f '() _ _) [(arr: dom rng rst #f '() _ _)
(values (map t->c dom) (list (t->c rng)) (t->c rst))])) (values (map t->c/neg dom) (list (t->c rng)) (t->c/neg rst))]))
(with-syntax (with-syntax
([(dom* ...) dom*] ([(dom* ...) dom*]
[rng* (match rngs* [rng* (match rngs*
@ -102,12 +104,22 @@
#`(cons/c #,(t->c t1) #,(t->c t2))] #`(cons/c #,(t->c t1) #,(t->c t2))]
[(Opaque: p? cert) [(Opaque: p? cert)
#`(flat-contract #,(cert p?))] #`(flat-contract #,(cert p?))]
[(F: v) (cond [(assoc v (vars)) => cadr] [(F: v) (cond [(assoc v (vars)) => (if pos? second third)]
[else (int-err "unknown var: ~a" v)])] [else (int-err "unknown var: ~a" v)])]
[(Poly: vs (and b (Function: _)))
(match-let ([(Poly-names: vs-nm _) ty])
(with-syntax ([(vs+ ...) (generate-temporaries (for/list ([v vs-nm]) (symbol-append v '+)))]
[(vs- ...) (generate-temporaries (for/list ([v vs-nm]) (symbol-append v '-)))])
(parameterize ([vars (append (map list
vs
(syntax->list #'(vs+ ...))
(syntax->list #'(vs- ...)))
(vars))])
#`(poly/c ([vs- vs+] ...) #,(t->c b)))))]
[(Mu: n b) [(Mu: n b)
(match-let ([(Mu-name: n-nm _) ty]) (match-let ([(Mu-name: n-nm _) ty])
(with-syntax ([(n*) (generate-temporaries (list n-nm))]) (with-syntax ([(n*) (generate-temporaries (list n-nm))])
(parameterize ([vars (cons (list n #'n*) (vars))]) (parameterize ([vars (cons (list n #'n* #'n*) (vars))])
#`(flat-rec-contract n* #,(t->c b)))))] #`(flat-rec-contract n* #,(t->c b)))))]
[(Value: #f) #'false/c] [(Value: #f) #'false/c]
[(Instance: _) #'(is-a?/c object%)] [(Instance: _) #'(is-a?/c object%)]
@ -115,10 +127,7 @@
[(Value: '()) #'null?] [(Value: '()) #'null?]
[(Struct: _ _ _ _ #f pred? cert) (cert pred?)] [(Struct: _ _ _ _ #f pred? cert) (cert pred?)]
[(Syntax: (Base: 'Symbol _)) #'identifier?] [(Syntax: (Base: 'Symbol _)) #'identifier?]
[(Syntax: t) [(Syntax: t) #`(syntax/c #,(t->c t))]
(if (equal? ty Any-Syntax)
#`syntax?
#`(syntax/c #,(t->c t)))]
[(Value: v) #`(flat-named-contract #,(format "~a" v) (lambda (x) (equal? x '#,v)))] [(Value: v) #`(flat-named-contract #,(format "~a" v) (lambda (x) (equal? x '#,v)))]
[(Param: in out) #`(parameter/c #,(t->c out))] [(Param: in out) #`(parameter/c #,(t->c out))]
[(Hashtable: k v) #`hash?] [(Hashtable: k v) #`hash?]

View File

@ -0,0 +1,70 @@
#lang scheme/base
(require scheme/contract (for-syntax scheme/base))
(provide memory/c apply/c poly/c)
(with-contract
poly-internals
([memory/c
(->*
[]
[ #:name any/c
#:to any/c
#:from any/c
#:weak boolean?
#:equal (or/c 'eq 'eqv 'equal)
#:table (-> (and/c hash? (not/c immutable?))) ]
(values flat-contract? flat-contract?))]
[apply/c (->* [any/c] [#:name any/c] contract?)])
(define (memory/c
#:name [name "memory/c"]
#:to [to (format "~a:to" name)]
#:from [from (format "~a:from" name)]
#:weak [weak? #t]
#:equal [equal 'eq]
#:table [make-table
(case equal
[(eq) (if weak? make-weak-hasheq make-hasheq)]
[(eqv) (if weak? make-weak-hasheqv make-hasheqv)]
[(equal) (if weak? make-weak-hash make-hash)])])
(let* ([table (make-table)])
(values
(flat-named-contract from
(lambda (v) (hash-set! table v #t) #t))
(flat-named-contract to
(lambda (v) (hash-ref table v #f))))))
(define (apply/c c
#:name [name (build-compound-type-name 'apply/c c)])
(make-proj-contract
name
(lambda (pos neg src name2)
(lambda (p)
(let* ([ctc (coerce-contract 'apply/c c)]
[thunk (lambda () ((((proj-get ctc) ctc) pos neg src name2) p))])
(make-keyword-procedure
(lambda (keys vals . args) (keyword-apply (thunk) keys vals args))
(case-lambda
[() ((thunk))]
[(a) ((thunk) a)]
[(a b) ((thunk) a b)]
[(a b c) ((thunk) a b c)]
[(a b c d) ((thunk) a b c d)]
[(a b c d e) ((thunk) a b c d e)]
[(a b c d e f) ((thunk) a b c d e f)]
[(a b c d e f g) ((thunk) a b c d e f g)]
[(a b c d e f g h) ((thunk) a b c d e f g h)]
[args (apply (thunk) args)])))))
procedure?)))
(define-syntax (poly/c stx)
(syntax-case stx ()
[(_ opts ... ([c- c+] ...) c)
(quasisyntax/loc stx
(apply/c
#:name (quote #,stx)
(recursive-contract
(let-values ([(c- c+) (memory/c #:from 'c- #:to 'c+ opts ...)] ...)
c))))]))

View File

@ -19,6 +19,7 @@
extend extend
debug debug
in-syntax in-syntax
symbol-append
;; require macros ;; require macros
rep utils typecheck infer env private) rep utils typecheck infer env private)

View File

@ -91,23 +91,28 @@
[char-set:ascii Char-Set] [char-set:ascii Char-Set]
[char-set:empty Char-Set] [char-set:empty Char-Set]
[char-set:full Char-Set] [char-set:full Char-Set]
[char-set-fold (All (A) ((Char A -> A) A Char-Set -> A))]
[char-set-unfold
(All (A)
(case-lambda
((A -> Any) (A -> Char) (A -> A) A -> Char-Set)
((A -> Any) (A -> Char) (A -> A) A Char-Set -> Char-Set)))]
[char-set-unfold!
(All (A) ((A -> Any) (A -> Char) (A -> A) A Char-Set -> Char-Set))]
[char-set-for-each (All (A) ((Char -> A) Char-Set -> (U A Void)))]
[char-set-any (All (A) ((Char -> A) Char-Set -> (U A #f)))]
[char-set-every (All (A) ((Char -> A) Char-Set -> (U A Boolean)))]
) ; end of require/typed ) ; end of require/typed
;; Definitions provided here for polymorphism ;; Definitions provided here for polymorphism
#;
(: char-set-fold (All (A) ((Char A -> A) A Char-Set -> A)))
(define (char-set-fold comb base cs) (define (char-set-fold comb base cs)
(let loop ((c (char-set-cursor cs)) (b base)) (let loop ((c (char-set-cursor cs)) (b base))
(cond [(end-of-char-set? c) b] (cond [(end-of-char-set? c) b]
[else [else
(loop (char-set-cursor-next cs c) (loop (char-set-cursor-next cs c)
(comb (char-set-ref cs c) b))]))) (comb (char-set-ref cs c) b))])))
#;
(: char-set-unfold
(All (A)
(case-lambda
((A -> Any) (A -> Char) (A -> A) A -> Char-Set)
((A -> Any) (A -> Char) (A -> A) A Char-Set -> Char-Set))))
(define char-set-unfold (define char-set-unfold
(pcase-lambda: (A) (pcase-lambda: (A)
[([p : (A -> Any)] [f : (A -> Char)] [g : (A -> A)] [seed : A]) [([p : (A -> Any)] [f : (A -> Char)] [g : (A -> A)] [seed : A])
@ -115,29 +120,25 @@
[([p : (A -> Any)] [f : (A -> Char)] [g : (A -> A)] [seed : A] [([p : (A -> Any)] [f : (A -> Char)] [g : (A -> A)] [seed : A]
[base-cs : Char-Set]) [base-cs : Char-Set])
(char-set-unfold! p f g seed (char-set-copy base-cs))])) (char-set-unfold! p f g seed (char-set-copy base-cs))]))
#;
(: char-set-unfold!
(All (A) ((A -> Any) (A -> Char) (A -> A) A Char-Set -> Char-Set)))
(define (char-set-unfold! p f g seed base-cs) (define (char-set-unfold! p f g seed base-cs)
(let lp ((seed seed) (cs base-cs)) (let lp ((seed seed) (cs base-cs))
(if (p seed) cs ; P says we are done. (if (p seed) cs ; P says we are done.
(lp (g seed) ; Loop on (G SEED). (lp (g seed) ; Loop on (G SEED).
(char-set-adjoin! cs (f seed)))))) (char-set-adjoin! cs (f seed))))))
(: char-set-for-each (All (A) ((Char -> A) Char-Set -> (U A Void)))) #;
(define (char-set-for-each f cs) (define (char-set-for-each f cs)
(char-set-fold (lambda: ([c : Char] [b : (U A Void)]) (f c)) (char-set-fold (lambda: ([c : Char] [b : (U A Void)]) (f c))
(void) (void)
cs)) cs))
#;
(: char-set-any (All (A) ((Char -> A) Char-Set -> (U A #f))))
(define (char-set-any pred cs) (define (char-set-any pred cs)
(let loop ((c (char-set-cursor cs))) (let loop ((c (char-set-cursor cs)))
(and (not (end-of-char-set? c)) (and (not (end-of-char-set? c))
(or (pred (char-set-ref cs c)) (or (pred (char-set-ref cs c))
(loop (char-set-cursor-next cs c)))))) (loop (char-set-cursor-next cs c))))))
#;
(: char-set-every (All (A) ((Char -> A) Char-Set -> (U A Boolean))))
(define (char-set-every pred cs) (define (char-set-every pred cs)
(let loop ((c (char-set-cursor cs)) (b (ann #t (U #t A)))) (let loop ((c (char-set-cursor cs)) (b (ann #t (U #t A))))
(cond [(end-of-char-set? c) b] (cond [(end-of-char-set? c) b]