Improve scoping structure of for-clauses

racket/typed/for-loops.rkt

@@ -26,17 +26,19 @@
     (pattern (~seq #:break pred:expr)
              #:attr parend #'(#:break pred))))
 
+;; a Binding is a (SyntaxList Id Id Type), i.e. #'(x x- τ-x)
 (begin-for-syntax
   (struct loop-clause (exp bindings) #:transparent)
   (struct directive (kw exp) #:transparent))
 
 
+;; (SyntaxListOf LoopClause) -> (Syntax LoopClause- (Binding ...))
 (define-for-syntax (analyze-for-clauses clauses)
   (define-values (br binds)
     (for/fold ([body-rev '()]
                [bindings '()])
               ([clause (in-syntax clauses)])
-      (match (analyze-for-clause clause)
+      (match (analyze-for-clause clause bindings)
         [(loop-clause exp bs)
          (values (cons exp body-rev)
                  (append bindings bs))]
@@ -46,34 +48,44 @@
   #`(#,(reverse br)
      #,binds))
 
-;; iter-clause -> (U iter-clause directive)
+;; iter-clause (Listof Binding) -> (U iter-clause directive)
-(define-for-syntax (analyze-for-clause clause)
+(define-for-syntax (analyze-for-clause clause ctx)
+  (define/with-syntax ([y y- τ-y] ...) ctx)
   (syntax-parse clause
     #:datum-literals (:)
     [[x:id seq:expr]
      #:and (~typecheck
-             [⊢ seq ≫ seq- (⇒ : τ-seq)])
+             [[y ≫ y-- : τ-y] ... ⊢ seq ≫ seq- (⇒ : τ-seq)])
      #:fail-unless (pure? #'seq-) "pure"
+     #:with x- (generate-temporary #'x)
      #:do [(define-values (seq-- τ-elems) (make-sequence #'seq- #'τ-seq))]
-     (loop-clause #`[x #,seq--]
+     (loop-clause (substs #'(y- ...) #'(y-- ...)
-                  (list #`(x #,τ-elems)))]
+                          #`[x- #,seq--]
+                          free-identifier=?)
+                  (list #`(x x- #,τ-elems)))]
     [[x:id : τ:type seq:expr]
-     #:do [(match-define (list seq- (list (list y τ-elems)))
+     #:with seq+ (add-expected-type #'seq #'τ.norm)
-             (analyze-for-clause (syntax/loc clause [x seq])))]
+     #:do [(match-define (list seq- (list (list x- τ-elems)))
+             (analyze-for-clause (syntax/loc clause [x seq+])))]
      #:fail-unless (<: τ-elems #'τ.norm) "unexpected type"
-     (loop-clause #`[#,y #,seq-]
+     (loop-clause #`[#,x- #,seq-]
-                  (list #`(#,y τ.norm)))]
+                  (list #`(x #,x- τ.norm)))]
     [[(k:id v:id) hash-seq:expr]
      #:and (~typecheck
-            [⊢ hash-seq ≫ hash-seq- (⇒ : (~Hash K V))])
+            [[y ≫ y-- : τ-y] ... ⊢ hash-seq ≫ hash-seq- (⇒ : (~Hash K V))])
      #:fail-unless (pure? #'hash-seq-) "pure"
-     (loop-clause #`[(k v) (in-hash- hash-seq-)]
+     #:with (k- v-) (generate-temporaries #'(k v))
-                  (list #'(k K) #'(v V)))]
+     (loop-clause (substs #'(y- ...) #'(y-- ...)
+                          #`[(k- v-) (in-hash- hash-seq-)]
+                          free-identifier=?)
+                  (list #'(k k- K) #'(v v- V)))]
     [(dir:keyword pred)
      #:and (~typecheck
-            [⊢ pred ≫ pred- (⇐ : Bool)])
+            [[y ≫ y-- : τ-y] ... ⊢ pred ≫ pred- (⇐ : Bool)])
      #:fail-unless (pure? #'pred-) "pure"
-     (directive #'dir #'pred-)]))
+     (directive #'dir (substs #'(y- ...) #'(y-- ...)
+                              #'pred-
+                              free-identifier=?))]))
 
 ;; Expression Type -> (Values Expression Type)
 ;; Determine what kind of sequence we're dealing with;
@@ -100,18 +112,29 @@
      e-body ...+) ≫
   [⊢ init ≫ init- (⇐ : τ-acc)]
   #:fail-unless (pure? #'init-) "expression must be pure"
-  #:with (clauses- ([x τ] ...)) (analyze-for-clauses #'(clause.parend ...))
+  #:with (clauses- ([x x- τ] ...)) (analyze-for-clauses #'(clause.parend ...))
-  [[x ≫ x- : τ] ...
+  [[x ≫ x-- : τ] ...
    [acc ≫ acc- : τ-acc] ⊢ (begin e-body ...) ≫ e-body-
                            (⇐ : τ-acc)
                            (⇒ ν-ep (~effs τ-ep ...))
                            (⇒ ν-s (~effs τ-s ...))
                            (⇒ ν-f (~effs τ-f ...))]
-  #:with clauses-- (substs #'(x- ...) #'(x ...) #'clauses-)
+  #:with e-body-- (substs #'(x- ...) #'(x-- ...) #'e-body- free-identifier=?)
+  ;; #:with y (stx-car #'(x ...))
+  ;; #:with y- (stx-car #'(x- ...))
+  ;; #:with y-- (stx-car #'(x-- ...))
+  ;; #:with (_ (_ dbg1)) #'e-body-
+  ;; #:with (_ (_ dbg2)) #'e-body--
+  ;; #:do [(printf "y/dbg1 ~a, ~a\n" (free-identifier=? #'y #'dbg1) (bound-identifier=? #'y #'dbg1))
+  ;;       (printf "y/dbg2 ~a, ~a\n" (free-identifier=? #'y #'dbg2) (bound-identifier=? #'y #'dbg2))
+  ;;       (printf "y-/dbg1 ~a, ~a\n" (free-identifier=? #'y- #'dbg1) (bound-identifier=? #'y- #'dbg1))
+  ;;       (printf "y-/dbg2 ~a, ~a\n" (free-identifier=? #'y- #'dbg2) (bound-identifier=? #'y- #'dbg2))
+  ;;       (printf "y--/dbg1 ~a, ~a\n" (free-identifier=? #'y-- #'dbg1) (bound-identifier=? #'y-- #'dbg1))
+  ;;       (printf "y--/dbg2 ~a, ~a\n" (free-identifier=? #'y-- #'dbg2) (bound-identifier=? #'y- #'dbg2))]
   -------------------------------------------------------
   [⊢ (for/fold- ([acc- init-])
-                (#,@#'clauses--)
+                (#,@#'clauses-)
-                e-body-)
+                e-body--)
      (⇒ : τ-acc)
      (⇒ ν-ep (τ-ep ...))
      (⇒ ν-s (τ-s ...))

racket/typed/tests/for-loops.rkt

@@ -57,8 +57,7 @@
             : (List (Tuple Int Int))
             ⇒ (list (tuple 1 4) (tuple 2 5) (tuple 3 6)))
 
-;; binding in #:when isn't handled
+(define (zip-even [xs : (List Int)]
-#;(define (zip-even [xs : (List Int)]
                   [ys : (List Int)])
   ((inst reverse (Tuple Int Int))
    (for/fold ([acc : (List (Tuple Int Int))
@@ -66,5 +65,9 @@
              ([x xs]
               #:when (even? x)
               [y ys]
-              #:when (even? y))
+              #:unless (odd? y))
      (cons (tuple x y) acc))))
+
+(check-type (zip-even (list 1 2 3) (list 5 6 7))
+            : (List (Tuple Int Int))
+            ⇒ (list (tuple 2 6)))