From ed48078523c1282d0df9f2133cfca50102f8849b Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Tue, 30 Dec 2008 19:47:21 +0000 Subject: [PATCH] checkpoint svn: r12954 --- collects/typed-scheme/infer/infer-unit.ss | 4 ++-- collects/typed-scheme/private/base-env.ss | 4 ++-- collects/typed-scheme/private/subtype.ss | 10 +++++----- .../private/type-effect-convenience.ss | 10 +++++----- .../typed-scheme/private/type-effect-printer.ss | 13 +++++++------ collects/typed-scheme/rep/effect-rep.ss | 14 ++++++++++---- collects/typed-scheme/utils/unit-utils.ss | 4 ++-- 7 files changed, 33 insertions(+), 26 deletions(-) diff --git a/collects/typed-scheme/infer/infer-unit.ss b/collects/typed-scheme/infer/infer-unit.ss index bcfc0e85fb..99e7e42675 100644 --- a/collects/typed-scheme/infer/infer-unit.ss +++ b/collects/typed-scheme/infer/infer-unit.ss @@ -100,9 +100,9 @@ (define (cgen/eff V X t s) (match* (t s) [(e e) (empty-cset X)] - [((Latent-Restrict-Effect: t) (Latent-Restrict-Effect: s)) + [((Latent-Restrict-Effect: t k) (Latent-Restrict-Effect: s k)) (cset-meet (cgen V X t s) (cgen V X s t))] - [((Latent-Remove-Effect: t) (Latent-Remove-Effect: s)) + [((Latent-Remove-Effect: t k) (Latent-Remove-Effect: s k)) (cset-meet (cgen V X t s) (cgen V X s t))] [(_ _) (fail! t s)])) diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss index aaad95ba84..48449b6a2b 100644 --- a/collects/typed-scheme/private/base-env.ss +++ b/collects/typed-scheme/private/base-env.ss @@ -107,8 +107,8 @@ [filter (-poly (a b) (cl->* ((a . -> . B : - (list (make-Latent-Restrict-Effect b)) - (list (make-Latent-Remove-Effect b))) + (list (make-Latent-Restrict-Effect b 0)) + (list (make-Latent-Remove-Effect b 0))) (-lst a) . -> . (-lst b)) diff --git a/collects/typed-scheme/private/subtype.ss b/collects/typed-scheme/private/subtype.ss index 7263ca8618..6373823824 100644 --- a/collects/typed-scheme/private/subtype.ss +++ b/collects/typed-scheme/private/subtype.ss @@ -81,15 +81,15 @@ (ormap (lambda (e) (arr-subtype*/no-fail A e s)) ts)) (define (sub-eff e1 e2) - (match (list e1 e2) - [(list e e) #t] - [(list (Latent-Restrict-Effect: t) (Latent-Restrict-Effect: t*)) + (match* (e1 e2) + [(e e) #t] + [((Latent-Restrict-Effect: t k) (Latent-Restrict-Effect: t* k)) (and (subtype t t*) (subtype t* t))] - [(list (Latent-Remove-Effect: t) (Latent-Remove-Effect: t*)) + [((Latent-Remove-Effect: t k) (Latent-Remove-Effect: t* k)) (and (subtype t t*) (subtype t* t))] - [else #f])) + [(_ _) #f])) ;(trace sub-eff) diff --git a/collects/typed-scheme/private/type-effect-convenience.ss b/collects/typed-scheme/private/type-effect-convenience.ss index 49f21dd872..2a6752941d 100644 --- a/collects/typed-scheme/private/type-effect-convenience.ss +++ b/collects/typed-scheme/private/type-effect-convenience.ss @@ -38,10 +38,10 @@ (define ((add-var v) eff) (match eff - [(Latent-Var-True-Effect:) (-vet v)] - [(Latent-Var-False-Effect:) (-vef v)] - [(Latent-Restrict-Effect: t) (make-Restrict-Effect t v)] - [(Latent-Remove-Effect: t) (make-Remove-Effect t v)] + [(Latent-Var-True-Effect: k) (-vet v)] + [(Latent-Var-False-Effect: k) (-vef v)] + [(Latent-Restrict-Effect: t k) (make-Restrict-Effect t v)] + [(Latent-Remove-Effect: t k) (make-Remove-Effect t v)] [(True-Effect:) eff] [(False-Effect:) eff] [_ (int-err "can't add var ~a to effect ~a" v eff)])) @@ -208,7 +208,7 @@ (define make-pred-ty (case-lambda [(in out t) - (->* in out : (list (make-Latent-Restrict-Effect t)) (list (make-Latent-Remove-Effect t)))] + (->* in out : (list (make-Latent-Restrict-Effect t 0)) (list (make-Latent-Remove-Effect t 0)))] [(t) (make-pred-ty (list Univ) B t)])) (define -Pathlike (*Un -Path -String)) diff --git a/collects/typed-scheme/private/type-effect-printer.ss b/collects/typed-scheme/private/type-effect-printer.ss index 37f248c391..0ba7cacd5e 100644 --- a/collects/typed-scheme/private/type-effect-printer.ss +++ b/collects/typed-scheme/private/type-effect-printer.ss @@ -32,10 +32,10 @@ (match c [(Restrict-Effect: t v) (fp "(restrict ~a ~a)" t (syntax-e v))] [(Remove-Effect: t v) (fp "(remove ~a ~a)" t (syntax-e v))] - [(Latent-Restrict-Effect: t) (fp "(restrict ~a)" t)] - [(Latent-Remove-Effect: t) (fp "(remove ~a)" t)] - [(Latent-Var-True-Effect:) (fp "(var #t)")] - [(Latent-Var-False-Effect:) (fp "(var #f)")] + [(Latent-Restrict-Effect: t k) (fp "(restrict ~a ~a)" t k)] + [(Latent-Remove-Effect: t k) (fp "(remove ~a ~a)" t k)] + [(Latent-Var-True-Effect: k) (fp "(var #t ~a)" k)] + [(Latent-Var-False-Effect: k) (fp "(var #f ~a)" k)] [(True-Effect:) (fp "T")] [(False-Effect:) (fp "F")] [(Var-True-Effect: v) (fp "(var #t ~a)" (syntax-e v))] @@ -64,9 +64,10 @@ (when drest (fp "~a ... ~a " (car drest) (cdr drest))) (fp "-> ~a" rng) - (match* (thn-eff els-eff) + (match* (thn-eff els-eff) [((list) (list)) (void)] - [((list (Latent-Restrict-Effect: t)) (list (Latent-Remove-Effect: t))) (fp " : ~a" t)] + [((list (Latent-Restrict-Effect: t 0)) (list (Latent-Remove-Effect: t 0))) (fp " : ~a" t)] + [((list (Latent-Restrict-Effect: t k)) (list (Latent-Remove-Effect: t k))) (fp " : ~a_~a" t k)] [(_ _) (fp " : ~a ~a" thn-eff els-eff)]) (fp ")")])) (define (tuple? t) diff --git a/collects/typed-scheme/rep/effect-rep.ss b/collects/typed-scheme/rep/effect-rep.ss index 892c889584..d7b3745521 100644 --- a/collects/typed-scheme/rep/effect-rep.ss +++ b/collects/typed-scheme/rep/effect-rep.ss @@ -27,13 +27,19 @@ [#:fold-rhs (*Remove-Effect (type-rec-id t) v)]) ;; t is a Type -(de Latent-Restrict-Effect (t)) +;; k is a nat +(de Latent-Restrict-Effect (t k) [#:frees (free-vars* t) (free-idxs* t)] + [#:fold-rhs (*Latent-Restrict-Effect (type-rec-id t) k)]) ;; t is a Type -(de Latent-Remove-Effect (t)) +;; k is a nat +(de Latent-Remove-Effect (t k) [#:frees (free-vars* t) (free-idxs* t)] + [#:fold-rhs (*Latent-Remove-Effect (type-rec-id t) k)]) -(de Latent-Var-True-Effect () [#:frees #f] [#:fold-rhs #:base]) +;; k is a nat +(de Latent-Var-True-Effect (k) [#:frees #f] [#:fold-rhs #:base]) -(de Latent-Var-False-Effect () [#:frees #f] [#:fold-rhs #:base]) +;; k is a nat +(de Latent-Var-False-Effect (k) [#:frees #f] [#:fold-rhs #:base]) ;; could also have latent true/false effects, but seems pointless diff --git a/collects/typed-scheme/utils/unit-utils.ss b/collects/typed-scheme/utils/unit-utils.ss index e5f4eb0a37..bbd8ab138d 100644 --- a/collects/typed-scheme/utils/unit-utils.ss +++ b/collects/typed-scheme/utils/unit-utils.ss @@ -12,8 +12,8 @@ (define-signature-form (cnt stx) (syntax-case stx () [(_ nm cnt) - #;(list #'nm) - (list #'[contracted nm cnt])])) + (list #'nm) + #;(list #'[contracted nm cnt])])) (define-syntax (define-values/link-units/infer stx) ;; construct something we can put in the imports/exports clause from the datum