Use let/ec instead of let/cc

let/ec: and let/cc:
type for call-with-current-continuation
Start on ImpFilters

svn: r15220
This commit is contained in:
Sam Tobin-Hochstadt 2009-06-19 18:01:33 +00:00
parent 181ad3fee0
commit 5b79cd7c0c
7 changed files with 44 additions and 5 deletions

View File

@ -275,6 +275,8 @@
[call/cc (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (Un a b)))] [call/cc (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (Un a b)))]
[call/ec (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (Un a b)))] [call/ec (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (Un a b)))]
[call-with-current-continuation (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (Un a b)))]
[call-with-escape-continuation (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (Un a b)))]
[quotient (-Integer -Integer . -> . -Integer)] [quotient (-Integer -Integer . -> . -Integer)]
[remainder (-Integer -Integer . -> . -Integer)] [remainder (-Integer -Integer . -> . -Integer)]

View File

@ -428,4 +428,14 @@ This file defines two sorts of primitives. All of them are provided into any mod
(define-syntax (declare-refinement stx) (define-syntax (declare-refinement stx)
(syntax-parse stx (syntax-parse stx
[(_ p:id) [(_ p:id)
(quasisyntax/loc stx #,(internal #'(declare-refinement-internal p)))])) (quasisyntax/loc stx #,(internal #'(declare-refinement-internal p)))]))
(define-syntaxes (let/cc: let/ec:)
(let ()
(define ((mk l/c) stx)
(syntax-parse stx
#:literals (:)
[(_ k:id : t . body)
(quasisyntax/loc stx
(let/cc #,(annotate-names #'([k : t]) stx) . body))]))
(values (mk #'let/cc) (mk #'let/ec))))

View File

@ -50,7 +50,7 @@
(define (type->contract ty fail) (define (type->contract ty fail)
(define vars (make-parameter '())) (define vars (make-parameter '()))
(let/cc exit (let/ec exit
(let loop ([ty ty] [pos? #t]) (let loop ([ty ty] [pos? #t])
(define (t->c t) (loop t pos?)) (define (t->c t) (loop t pos?))
(define (t->c/neg t) (loop t (not pos?))) (define (t->c/neg t) (loop t (not pos?)))

View File

@ -7,7 +7,7 @@
(flat-named-contract (flat-named-contract
'Filter 'Filter
(λ (e) (λ (e)
(and (Filter? e) (not (FilterSet? e)))))) (and (Filter? e) (not (NoFilter? e)) (not (FilterSet? e))))))
(define LatentFilter/c (define LatentFilter/c
(flat-named-contract (flat-named-contract
@ -31,6 +31,9 @@
(combine-frees (map free-idxs* (cons t p)))] (combine-frees (map free-idxs* (cons t p)))]
[#:fold-rhs (*NotTypeFilter (type-rec-id t) (map pathelem-rec-id p) v)]) [#:fold-rhs (*NotTypeFilter (type-rec-id t) (map pathelem-rec-id p) v)])
;; implication
(df ImpFilter ([a (listof Filter/c)] [c (listof Filter/c)]))
(df FilterSet (thn els) (df FilterSet (thn els)
[#:frees (combine-frees (map free-vars* (append thn els))) [#:frees (combine-frees (map free-vars* (append thn els)))
(combine-frees (map free-idxs* (append thn els)))] (combine-frees (map free-idxs* (append thn els)))]
@ -64,6 +67,9 @@
[#:frees (lambda (frees*) (combine-frees (map (compose make-invariant frees*) (cons t p))))] [#:frees (lambda (frees*) (combine-frees (map (compose make-invariant frees*) (cons t p))))]
[#:fold-rhs (*LNotTypeFilter (type-rec-id t) (map pathelem-rec-id p) idx)]) [#:fold-rhs (*LNotTypeFilter (type-rec-id t) (map pathelem-rec-id p) idx)])
;; implication
(df LImpFilter ([a (listof LatentFilter/c)] [c (listof LatentFilter/c)]))
(dlf LFilterSet (thn els) (dlf LFilterSet (thn els)
[#:frees (combine-frees (map free-vars* (append thn els))) [#:frees (combine-frees (map free-vars* (append thn els)))
(combine-frees (map free-idxs* (append thn els)))] (combine-frees (map free-idxs* (append thn els)))]

View File

@ -129,6 +129,11 @@ result of @scheme[_loop] (and thus the result of the entire
@defform[(let*: ([v : t e] ...) . body)]]]{Type-annotated versions of @defform[(let*: ([v : t e] ...) . body)]]]{Type-annotated versions of
@scheme[letrec] and @scheme[let*].} @scheme[letrec] and @scheme[let*].}
@deftogether[[
@defform[(let/cc: v : t . body)]
@defform[(let/ec: v : t . body)]]]{Type-annotated versions of
@scheme[let/cc] and @scheme[let/ec].}
@subsection{Anonymous Functions} @subsection{Anonymous Functions}
@defform/subs[(lambda: formals . body) @defform/subs[(lambda: formals . body)

View File

@ -77,6 +77,10 @@
[(Bot:) (list (make-LBot))] [(Bot:) (list (make-LBot))]
[(TypeFilter: t p (lookup: idx)) (list (make-LTypeFilter t p idx))] [(TypeFilter: t p (lookup: idx)) (list (make-LTypeFilter t p idx))]
[(NotTypeFilter: t p (lookup: idx)) (list (make-LNotTypeFilter t p idx))] [(NotTypeFilter: t p (lookup: idx)) (list (make-LNotTypeFilter t p idx))]
[(ImpFilter: a c)
(match* [(abo a) (abo c)]
[((list a*) (list c*)) (list (make-LImpFilter a* c*))]
[(_ _) null])]
[_ null])) [_ null]))
(define (merge-filter-sets fs) (define (merge-filter-sets fs)
@ -95,6 +99,12 @@
(d/c (apo lf s o) (d/c (apo lf s o)
(-> LatentFilter/c Type/c Object? (or/c '() (list/c Filter/c))) (-> LatentFilter/c Type/c Object? (or/c '() (list/c Filter/c)))
(match* (lf s o) (match* (lf s o)
[((ImpFilter: as cs) _ _)
(match* [(for/list ([a as]) (apo a s o))
(for/list ([c cs]) (apo c s o))]
[((list (list a*) ...)
(list (list c*) ...)) (list (make-ImpFilter a* c*))]
[(_ _) null])]
[((LBot:) _ _) (list (make-Bot))] [((LBot:) _ _) (list (make-Bot))]
[((LNotTypeFilter: (? (lambda (t) (subtype s t)) t) (list) _) _ _) (list (make-Bot))] [((LNotTypeFilter: (? (lambda (t) (subtype s t)) t) (list) _) _ _) (list (make-Bot))]
[((LTypeFilter: (? (lambda (t) (not (overlap s t))) t) (list) _) _ _) (list (make-Bot))] [((LTypeFilter: (? (lambda (t) (not (overlap s t))) t) (list) _) _ _) (list (make-Bot))]
@ -135,7 +145,13 @@
[((FilterSet: f1+ f1-) (T-FS:) (FilterSet: f3+ f3-)) (mk (combine null (append f1- f3-)))] [((FilterSet: f1+ f1-) (T-FS:) (FilterSet: f3+ f3-)) (mk (combine null (append f1- f3-)))]
;; and ;; and
[((FilterSet: f1+ f1-) (FilterSet: f2+ f2-) (F-FS:)) [((FilterSet: f1+ f1-) (FilterSet: f2+ f2-) (F-FS:))
(mk (combine (append f1+ f2+) null))] (mk (combine (append f1+ f2+)
null
#;
(append (for/list ([f f1-])
(make-ImpFilter f2+ f))
(for/list ([f f2-])
(make-ImpFilter f1+ f)))))]
[(f f* f*) (mk f*)] [(f f* f*) (mk f*)]
;; the student expansion ;; the student expansion
[(f (T-FS:) (F-FS:)) (mk f)] [(f (T-FS:) (F-FS:)) (mk f)]

View File

@ -15,7 +15,7 @@
;; has-name : Type -> Maybe[Symbol] ;; has-name : Type -> Maybe[Symbol]
(define (has-name? t) (define (has-name? t)
(define ns ((current-type-names))) (define ns ((current-type-names)))
(let/cc return (let/ec return
(unless print-aliases (unless print-aliases
(return #f)) (return #f))
(for-each (for-each