From 1b2527920e47014b00d4b8949231d80de2205b21 Mon Sep 17 00:00:00 2001
From: Sam Caldwell <samc@ccs.neu.edu>
Date: Tue, 30 Apr 2019 17:42:03 -0400
Subject: [PATCH] start on for loops

---
 racket/typed/core-types.rkt      |   2 +-
 racket/typed/for-loops.rkt       | 125 +++++++++++++++++++++++++++++++
 racket/typed/list.rkt            |  38 +---------
 racket/typed/prim.rkt            |   2 +
 racket/typed/roles.rkt           |   3 +
 racket/typed/tests/for-loops.rkt |  69 +++++++++++++++++
 6 files changed, 204 insertions(+), 35 deletions(-)
 create mode 100644 racket/typed/for-loops.rkt
 create mode 100644 racket/typed/tests/for-loops.rkt

diff --git a/racket/typed/core-types.rkt b/racket/typed/core-types.rkt
index 6fbbdc1..6585473 100644
--- a/racket/typed/core-types.rkt
+++ b/racket/typed/core-types.rkt
@@ -717,7 +717,7 @@
       (free-identifier=? #'X #'Y)]
      [((~∀ (X:id ...) τ1) (~∀ (Y:id ...) τ2))
       #:when (stx-length=? #'(X ...) #'(Y ...))
-      #:with τ2-X/Y (substs #'(X ...) #'(Y ...) #'τ2)
+      #:with τ2-X/Y (substs #'(Y ...) #'(X ...) #'τ2)
       (<: #'τ1 #'τ2-X/Y)]
      [((~Base τ1:id) (~Base τ2:id))
       (free-identifier=? #'τ1 #'τ2)]
diff --git a/racket/typed/for-loops.rkt b/racket/typed/for-loops.rkt
new file mode 100644
index 0000000..4e42ef2
--- /dev/null
+++ b/racket/typed/for-loops.rkt
@@ -0,0 +1,125 @@
+#lang turnstile
+
+(provide for/fold)
+
+(require "core-types.rkt")
+(require "sequence.rkt")
+(require (only-in "list.rkt" List ~List))
+(require (only-in "set.rkt" Set ~Set))
+(require (only-in "hash.rkt" Hash ~Hash))
+
+(begin-for-syntax
+  (define-splicing-syntax-class iter-clause
+    #:attributes (parend)
+    #:datum-literals (:)
+    (pattern [x:id seq:expr]
+             #:attr parend #'[x seq])
+    (pattern [x:id : τ:type seq:expr]
+             #:attr parend #'[x : τ seq])
+    (pattern [(k:id v:id) hash-seq:expr]
+             #:attr parend #'[(k v) hash-seq])
+    (pattern (~seq #:when pred:expr)
+             #:attr parend #'(#:when pred))
+    (pattern (~seq #:unless pred:expr)
+             #:attr parend #'(#:unless pred))
+    (pattern (~seq #:break pred:expr)
+             #:attr parend #'(#:break pred))))
+
+(begin-for-syntax
+  (struct loop-clause (exp bindings) #:transparent)
+  (struct directive (kw exp) #:transparent))
+
+
+(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)
+        [(loop-clause exp bs)
+         (values (cons exp body-rev)
+                 (append bindings bs))]
+        [(directive kw exp)
+         (values (list* exp kw body-rev)
+                 bindings)])))
+  #`(#,(reverse br)
+     #,binds))
+
+;; iter-clause -> (U iter-clause directive)
+(define-for-syntax (analyze-for-clause clause)
+  (syntax-parse clause
+    #:datum-literals (:)
+    [[x:id seq:expr]
+     #:and (~typecheck
+             [⊢ seq ≫ seq- (⇒ : τ-seq)])
+     #:fail-unless (pure? #'seq-) "pure"
+     #:do [(define-values (seq-- τ-elems) (make-sequence #'seq- #'τ-seq))]
+     (loop-clause #`[x #,seq--]
+                  (list #`(x #,τ-elems)))]
+    [[x:id : τ:type seq:expr]
+     #:do [(match-define (list seq- (list (list y τ-elems)))
+             (analyze-for-clause (syntax/loc clause [x seq])))]
+     #:fail-unless (<: τ-elems #'τ.norm) "unexpected type"
+     (loop-clause #`[#,y #,seq-]
+                  (list #`(#,y τ.norm)))]
+    [[(k:id v:id) hash-seq:expr]
+     #:and (~typecheck
+            [⊢ hash-seq ≫ hash-seq- (⇒ : (~Hash K V))])
+     #:fail-unless (pure? #'hash-seq-) "pure"
+     (loop-clause #`[(k v) (in-hash- hash-seq-)]
+                  (list #'(k K) #'(v V)))]
+    [(dir:keyword pred)
+     #:and (~typecheck
+            [⊢ pred ≫ pred- (⇐ : Bool)])
+     #:fail-unless (pure? #'pred-) "pure"
+     (directive #'dir #'pred-)]))
+
+;; Expression Type -> (Values Expression Type)
+;; Determine what kind of sequence we're dealing with;
+;; if it's not already in Sequence form, wrap the expression in the appropriate in-* form
+;; also figure out what the type of elements are to associate with the loop variable
+;; hashes handled separately
+(define-for-syntax (make-sequence e τ)
+  (syntax-parse τ
+    [(~Sequence t)
+     (values e #'t)]
+    [(~List t)
+     (values #`(in-list- #,e) #'t)]
+    [(~Set t)
+     (values #`(in-set- #,e) #'t)]
+    [_
+     (type-error #:src e
+                 #:msg "not an iterable type: " τ)]))
+
+
+(define-typed-syntax for/fold
+  [(for/fold ([acc:id (~optional (~datum :)) τ-acc init])
+             (clause:iter-clause
+              ...)
+     e-body ...+) ≫
+  [⊢ init ≫ init- (⇐ : τ-acc)]
+  #:fail-unless (pure? #'init-) "expression must be pure"
+  #:with (clauses- ([x τ] ...)) (analyze-for-clauses #'(clause.parend ...))
+  [[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-)
+  -------------------------------------------------------
+  [⊢ (for/fold- ([acc- init-])
+                (#,@#'clauses--)
+                e-body-)
+     (⇒ : τ-acc)
+     (⇒ ν-ep (τ-ep ...))
+     (⇒ ν-s (τ-s ...))
+     (⇒ ν-f (τ-f ...))]]
+  [(for/fold ([acc:id init])
+             clauses
+     e-body ...+) ≫
+   [⊢ init ≫ _ (⇒ : τ-acc)]
+   ---------------------------------------------------
+   [≻ (for/fold ([acc τ-acc init])
+                clauses
+        e-body ...)]])
diff --git a/racket/typed/list.rkt b/racket/typed/list.rkt
index f5ed0d9..c6cba1f 100644
--- a/racket/typed/list.rkt
+++ b/racket/typed/list.rkt
@@ -8,8 +8,7 @@
          rest
          member?
          empty?
-         for
-         for/fold)
+         reverse)
 
 (require "core-types.rkt")
 (require (postfix-in - racket/list))
@@ -35,38 +34,6 @@
   ----------------------------------------
   [⊢ (cons- e1- e2-) ⇒ τ-l])
 
-(define-typed-syntax (for/fold [acc:id e-acc]
-                               [x:id e-list]
-                       e-body ...+) ≫
-  [⊢ e-list ≫ e-list- ⇒ (~List τ-l)]
-  #:fail-unless (pure? #'e-list-) "expression must be pure"
-  [⊢ e-acc ≫ e-acc- ⇒ τ-a]
-  #:fail-unless (pure? #'e-acc-) "expression must be pure"
-  [[x ≫ x- : τ-l] [acc ≫ acc- : τ-a] ⊢ (begin e-body ...) ≫ e-body- ⇒ τ-b]
-  #:fail-unless (pure? #'e-body-) "body must be pure"
-  #:fail-unless (<: #'τ-b #'τ-a)
-    "loop body doesn't match accumulator"
-  -------------------------------------------------------
-  [⊢ (for/fold- ([acc- e-acc-])
-                ([x- (in-list- e-list-)])
-       e-body-)
-     ⇒ τ-b])
-
-(define-typed-syntax (for ([x:id e-list] ...)
-                       e-body ...+) ≫
-  [⊢ e-list ≫ e-list- ⇒ (~List τ-l)] ...
-  #:fail-unless (all-pure? #'(e-list- ...)) "expressions must be pure"
-  [[x ≫ x- : τ-l] ... ⊢ (begin e-body ...) ≫ e-body- (⇒ : τ-b)
-                  (⇒ ν-ep (~effs eps ...))
-                  (⇒ ν-f (~effs fs ...))
-                  (⇒ ν-s (~effs ss ...))]
-  -------------------------------------------------------
-  [⊢ (for- ([x- (in-list- e-list-)] ...)
-       e-body-) (⇒ : ★/t)
-                (⇒ ν-ep (eps ...))
-                (⇒ ν-f (fs ...))
-                (⇒ ν-s (ss ...))])
-
 (define-typed-syntax (empty? e) ≫
   [⊢ e ≫ e- ⇒ (~List _)]
   #:fail-unless (pure? #'e-) "expression must be pure"
@@ -96,3 +63,6 @@
 
 (define- (member?- v l)
   (and- (member- v l) #t))
+
+(require/typed racket/base
+  [reverse : (∀ (X) (→fn (List X) (List X)))])
diff --git a/racket/typed/prim.rkt b/racket/typed/prim.rkt
index b557d59..83a8e74 100644
--- a/racket/typed/prim.rkt
+++ b/racket/typed/prim.rkt
@@ -22,6 +22,8 @@
 (define-primop <= (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
 (define-primop >= (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
 (define-primop = (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
+(define-primop even? (→fn Int Bool))
+(define-primop odd? (→fn Int Bool))
 
 (define-primop bytes->string/utf-8 (→ ByteString (Computation (Value String) (Endpoints) (Roles) (Spawns))))
 (define-primop string->bytes/utf-8 (→ String (Computation (Value ByteString) (Endpoints) (Roles) (Spawns))))
diff --git a/racket/typed/roles.rkt b/racket/typed/roles.rkt
index 07fec22..5ddb407 100644
--- a/racket/typed/roles.rkt
+++ b/racket/typed/roles.rkt
@@ -41,6 +41,8 @@
          (all-from-out "sequence.rkt")
          ;; hash tables
          (all-from-out "hash.rkt")
+         ;; for loops
+         (all-from-out "for-loops.rkt")
          ;; DEBUG and utilities
          print-type print-role
          ;; Extensions
@@ -57,6 +59,7 @@
 (require "prim.rkt")
 (require "sequence.rkt")
 (require "hash.rkt")
+(require "for-loops.rkt")
 
 (require (prefix-in syndicate: syndicate/actor-lang))
 
diff --git a/racket/typed/tests/for-loops.rkt b/racket/typed/tests/for-loops.rkt
new file mode 100644
index 0000000..8cf24ed
--- /dev/null
+++ b/racket/typed/tests/for-loops.rkt
@@ -0,0 +1,69 @@
+#lang typed/syndicate/roles
+
+(require rackunit/turnstile)
+
+
+(check-type (for/fold ([x 0])
+                      ([y (list 1 2 3)])
+              x)
+            : Int
+            ⇒ 0)
+
+(check-type (for/fold ([x 0])
+                      ([y (list 1 2 3)])
+              y)
+            : Int
+            ⇒ 3)
+
+(define-type-alias Inventory (List (Tuple String Int)))
+
+(define inventory0 (list (tuple "The Wind in the Willows" 5)
+                           (tuple "Catch 22" 2)
+                           (tuple "Candide" 33)))
+(check-type (for/fold ([stock 0])
+                      ([item inventory0])
+              (select 1 item))
+            : Int
+            ⇒ 33)
+
+(check-type (for/fold ([stock 0])
+                      ([item inventory0])
+              (if (equal? "Catch 22" (select 0 item))
+                  (select 1 item)
+                  stock))
+            : Int
+            ⇒ 2)
+
+(define (lookup [title : String]
+                [inv : Inventory] -> Int)
+  (for/fold ([stock 0])
+            ([item inv])
+    (if (equal? title (select 0 item))
+        (select 1 item)
+        stock)))
+
+(check-type lookup : (→fn String Inventory Int))
+
+(define (zip [xs : (List Int)]
+             [ys : (List Int)])
+  ((inst reverse (Tuple Int Int))
+   (for/fold ([acc : (List (Tuple Int Int))
+                   (list)])
+             ([x xs]
+              [y ys])
+     (cons (tuple x y) acc))))
+
+(check-type (zip (list 1 2 3) (list 4 5 6))
+            : (List (Tuple Int Int))
+            ⇒ (list (tuple 1 4) (tuple 2 5) (tuple 3 6)))
+
+(define (zip-even [xs : (List Int)]
+                  [ys : (List Int)])
+  ((inst reverse (Tuple Int Int))
+   (for/fold ([acc : (List (Tuple Int Int))
+                   (list)])
+             ([x xs]
+              #:when (even? x)
+              [y ys]
+              #:when (even? y))
+     (cons (tuple x y) acc))))