checkpoint

svn: r12954

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)]))
 

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-Restrict-Effect b 0))
-                          (list (make-Latent-Remove-Effect b)))
+                          (list (make-Latent-Remove-Effect b 0)))
                        (-lst a)
                        . -> .
                        (-lst 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)
+  (match* (e1 e2)
-    [(list e e) #t]
+    [(e e) #t]
-    [(list (Latent-Restrict-Effect: t) (Latent-Restrict-Effect: 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)
 

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-True-Effect: k) (-vet v)]
-    [(Latent-Var-False-Effect:) (-vef v)]
+    [(Latent-Var-False-Effect: k) (-vef v)]
-    [(Latent-Restrict-Effect: t) (make-Restrict-Effect t v)]
+    [(Latent-Restrict-Effect: t k) (make-Restrict-Effect t v)]
-    [(Latent-Remove-Effect: t) (make-Remove-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))

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-Restrict-Effect: t k) (fp "(restrict ~a ~a)" t k)]
-    [(Latent-Remove-Effect: t) (fp "(remove ~a)" t)]
+    [(Latent-Remove-Effect: t k) (fp "(remove ~a ~a)" t k)]
-    [(Latent-Var-True-Effect:) (fp "(var #t)")]
+    [(Latent-Var-True-Effect: k) (fp "(var #t ~a)" k)]
-    [(Latent-Var-False-Effect:) (fp "(var #f)")]
+    [(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)

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

collects/typed-scheme/utils/unit-utils.ss

@@ -12,8 +12,8 @@
 (define-signature-form (cnt stx)
   (syntax-case stx ()
     [(_ nm cnt)
-     #;(list #'nm)
+     (list #'nm)
-     (list #'[contracted nm cnt])]))
+     #;(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