adjust check function to properly deal with the store

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/1.diff

@@ -6,7 +6,7 @@
 <    (tc-down (x y Γ) M (λ y κ) σ_ans)
 ---
 >    (tc-down (x y Γ) M (λ x κ) σ_ans)
-496a497,499
+571a572,574
 > 
 > (define small-counter-example '(hd ((λ x x) 1)))
 > (test-equal (check small-counter-example) #f)

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/2.diff

@@ -16,7 +16,7 @@
 <   [(where #t (not-v? M))
 <    (tc-down Γ ((λ x N) M) κ σ_2)
 <    ---------------------------------
-496a492,497
+571a567,572
 > 
 > (define small-counter-example '(let ([x (new nil)])
 >                                  ((λ ignore

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/3.diff

@@ -6,8 +6,7 @@
 <    (where G (unify τ_2 (τ_1 → x)))
 ---
 >    (where G (unify τ_1 (τ_2 → x)))
-496a497,500
+571a572,574
-> 
 > 
 > (define small-counter-example (term (1 cons)))
 > (test-equal (check small-counter-example) #f)

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/4.diff

@@ -8,7 +8,7 @@
 <   [(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars-τ? x τ))]
 ---
 >   [(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars? x τ))]
-496a499,501
+571a574,576
 > 
 > (define small-counter-example (term ((λ x (x x)) (λ x x))))
-> (check-equal? (check small-counter-example #f))
+> (test-equal (check small-counter-example) #f)

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/5.diff

@@ -10,7 +10,7 @@
 >    (τ (eliminate-τ x τ σ) (eliminate-G x τ G))]
 >   [(eliminate-G x τ (y σ G))
 >    (y (eliminate-τ x τ σ) (eliminate-G x τ G))])
-496a499,503
+571a574,578
 > 
 > (define small-counter-example (term (cons 1)))
 > (test-equal (with-handlers ([exn:fail? (λ (x) #f)])

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/6.diff

@@ -6,7 +6,7 @@
 <   [(∨ boolean_1 boolean_2) #t])
 ---
 >   [(∨ boolean boolean) #t])
-496a497,501
+571a572,576
 > 
 > (define small-counter-example (term ((λ x x) 1)))
 > (test-equal (with-handlers ([exn:fail? (λ (x) #f)])

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/7.diff

@@ -15,7 +15,7 @@
 ---
 >    (--> (Σ (in-hole E (let ([x M]) N)))
 >         (Σ (in-hole E ((λ x N) M)))
-496a498,500
+571a573,575
 > 
 > (define small-counter-example (term (let ((x (λ y y))) (x x))))
 > (test-equal (check small-counter-example) #f)

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-1.rkt

@@ -7,7 +7,7 @@
          racket/match
          racket/list
          racket/contract
-         racket/bool
+         racket/bool racket/set
          (only-in "../stlc/tests-lib.rkt" consistent-with?))
 
 (provide (all-defined-out))
@@ -386,8 +386,8 @@ A top-level evaluator
 
 (define/contract (Eval M)
   (-> M? (or/c "error" 'list 'λ 'ref number?))
-  (define M-t (judgment-holds (typeof ,M τ) τ))
+  (define M-t (type-check M))
-  (unless (pair? M-t)
+  (unless M-t
     (error 'Eval "doesn't typecheck: ~s" M))
   (define res (apply-reduction-relation* red (term (· ,M))))
   (unless (= 1 (length res))
@@ -396,7 +396,7 @@ A top-level evaluator
   (match (car res)
     ["error" "error"]
     [`(,Σ ,N)
-     (define ans-t (judgment-holds (typeof (Σ->lets ,Σ ,N) τ) τ))
+     (define ans-t (type-check N Σ))
      (unless (equal? M-t ans-t)
        (error 'Eval "internal error: type soundness fails for ~s" M))
      (match N
@@ -411,31 +411,107 @@ A top-level evaluator
        [(? number?) N]
        [_ (error 'Eval "internal error: didn't reduce to a value ~s" M)])]))
 
-(define-metafunction stlc
-  Σ->lets : Σ M -> M
-  [(Σ->lets · M) M]
-  [(Σ->lets (x v Σ) M) (let ([x (new v)]) (Σ->lets Σ M))])
-
 #|
 
-A top-level type checker.
+A type checker; the optional argument is a store to use
+for type checking free variables in M.
 
 |#
 
-(define/contract (type-check M)
+(define/contract (type-check M [Σ (term ·)])
-  (-> M? (or/c τ? #f))
+  (->* (M?) (any/c) (or/c τ? #f))
-  (define M-t (judgment-holds (typeof ,M τ) τ))
+  (define M-ts (judgment-holds (typeof ,(Σ+M->M Σ M) τ) τ))
   (cond
-    [(empty? M-t)
+    [(null? M-ts)
      #f]
-    [(null? (cdr M-t))
+    [(null? (cdr M-ts))
-     (car M-t)]
+     (car M-ts)]
     [else
-     (error 'type-check "non-unique type: ~s : ~s" M M-t)]))
+     (error 'type-check "non-unique type: ~s : ~s" M M-ts)]))
+
+;; building an expression out of a store can be done in this model
+;; with just topological sort because there are no recursive types,
+;; so the store will not contain any cycles
+(define (Σ+M->M Σ M)
+  ;; nodes : edges[r -o> v]
+  (define nodes (make-hash))
+  (define edges (make-hash))
+  (let loop ([Σ Σ])
+    (match Σ
+      [`· (void)]
+      [`(,r ,v ,Σ) 
+       (hash-set! nodes r v)
+       (loop Σ)]))
+  
+  (for ([(n rhs) (in-hash nodes)]) (hash-set! edges n (set)))
+  (for ([(n-src rhs) (in-hash nodes)])
+    (for ([(n-dest _) (in-hash nodes)])
+      (when (mentions-node? n-dest rhs)
+        (hash-set! edges n-src (set-add (hash-ref edges n-src) n-dest)))))
+  (define rev-sorted (reverse-topo-sort (for/list ([(k v) (in-hash nodes)]) k)
+                                        edges))
+  (let loop ([sorted rev-sorted])
+    (cond
+      [(empty? sorted) M]
+      [else
+       (define r (car sorted))
+       (term (let ([,r (new ,(hash-ref nodes r))])
+               ,(loop (cdr sorted))))])))
+
+(define (mentions-node? v r)
+  (let loop ([v v])
+    (cond
+      [(symbol? v) (equal? r v)]
+      [(pair? v) (or (loop (car v)) (loop (cdr v)))]
+      [else #f])))
 
 #|
 
-Random generators
+The first algorithm from this page:
+http://en.wikipedia.org/wiki/Topological_sorting#Algorithms
+
+|#
+(define/contract (reverse-topo-sort nodes edges)
+  (-> (listof any/c) (hash/c any/c (set/c any/c)) (listof any/c))
+  
+  (for ([node (in-list nodes)])
+    (unless (hash-ref edges node #f)
+      (error 'topo-sort "no edge entry for ~s" node)))
+  
+  (define incoming-counts (build-incoming-counts nodes edges))
+  (define (remove-edge src dest)
+    (hash-set! edges src (set-remove (hash-ref edges src) dest))
+    (hash-set! incoming-counts dest (- (hash-ref incoming-counts dest) 1)))
+  
+  (define l '())
+  (define s (for/set ([(n c) (in-hash incoming-counts)]
+                      #:when (zero? c))
+              n))
+  (let loop ()
+    (unless (set-empty? s)
+      (define n (set-first s))
+      (set! s (set-remove s n))
+      (set! l (cons n l))
+      (for ([m (in-set (hash-ref edges n))])
+        (remove-edge n m)
+        (when (zero? (hash-ref incoming-counts m))
+          (set! s (set-add s m))))
+      (loop)))
+  
+  l)
+        
+(define (build-incoming-counts nodes edges)
+  (define incoming-counts (make-hash))
+  (for ([n (in-list nodes)]) (hash-set! incoming-counts n 0))
+  (for ([(n neighbors) (in-hash edges)])
+    (for ([neighbor (in-set neighbors)])
+      (hash-set! incoming-counts neighbor (+ (hash-ref incoming-counts neighbor) 1))))
+  incoming-counts)
+  
+
+#|
+
+Generators
 
 |#
 
@@ -485,8 +561,7 @@ from the given term.
         (implies
          t-type
          (let loop ([Σ+M `(· ,M)])
-           (define new-type 
+           (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0)))
-             (type-check (term (Σ->lets ,(list-ref Σ+M 0) ,(list-ref Σ+M 1)))))
            (and (consistent-with? t-type new-type)
                 (or (v? (list-ref Σ+M 1))
                     (let ([red-res (apply-reduction-relation red Σ+M)])

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-2.rkt

@@ -7,7 +7,7 @@
          racket/match
          racket/list
          racket/contract
-         racket/bool
+         racket/bool racket/set
          (only-in "../stlc/tests-lib.rkt" consistent-with?))
 
 (provide (all-defined-out))
@@ -381,8 +381,8 @@ A top-level evaluator
 
 (define/contract (Eval M)
   (-> M? (or/c "error" 'list 'λ 'ref number?))
-  (define M-t (judgment-holds (typeof ,M τ) τ))
+  (define M-t (type-check M))
-  (unless (pair? M-t)
+  (unless M-t
     (error 'Eval "doesn't typecheck: ~s" M))
   (define res (apply-reduction-relation* red (term (· ,M))))
   (unless (= 1 (length res))
@@ -391,7 +391,7 @@ A top-level evaluator
   (match (car res)
     ["error" "error"]
     [`(,Σ ,N)
-     (define ans-t (judgment-holds (typeof (Σ->lets ,Σ ,N) τ) τ))
+     (define ans-t (type-check N Σ))
      (unless (equal? M-t ans-t)
        (error 'Eval "internal error: type soundness fails for ~s" M))
      (match N
@@ -406,31 +406,107 @@ A top-level evaluator
        [(? number?) N]
        [_ (error 'Eval "internal error: didn't reduce to a value ~s" M)])]))
 
-(define-metafunction stlc
-  Σ->lets : Σ M -> M
-  [(Σ->lets · M) M]
-  [(Σ->lets (x v Σ) M) (let ([x (new v)]) (Σ->lets Σ M))])
-
 #|
 
-A top-level type checker.
+A type checker; the optional argument is a store to use
+for type checking free variables in M.
 
 |#
 
-(define/contract (type-check M)
+(define/contract (type-check M [Σ (term ·)])
-  (-> M? (or/c τ? #f))
+  (->* (M?) (any/c) (or/c τ? #f))
-  (define M-t (judgment-holds (typeof ,M τ) τ))
+  (define M-ts (judgment-holds (typeof ,(Σ+M->M Σ M) τ) τ))
   (cond
-    [(empty? M-t)
+    [(null? M-ts)
      #f]
-    [(null? (cdr M-t))
+    [(null? (cdr M-ts))
-     (car M-t)]
+     (car M-ts)]
     [else
-     (error 'type-check "non-unique type: ~s : ~s" M M-t)]))
+     (error 'type-check "non-unique type: ~s : ~s" M M-ts)]))
+
+;; building an expression out of a store can be done in this model
+;; with just topological sort because there are no recursive types,
+;; so the store will not contain any cycles
+(define (Σ+M->M Σ M)
+  ;; nodes : edges[r -o> v]
+  (define nodes (make-hash))
+  (define edges (make-hash))
+  (let loop ([Σ Σ])
+    (match Σ
+      [`· (void)]
+      [`(,r ,v ,Σ) 
+       (hash-set! nodes r v)
+       (loop Σ)]))
+  
+  (for ([(n rhs) (in-hash nodes)]) (hash-set! edges n (set)))
+  (for ([(n-src rhs) (in-hash nodes)])
+    (for ([(n-dest _) (in-hash nodes)])
+      (when (mentions-node? n-dest rhs)
+        (hash-set! edges n-src (set-add (hash-ref edges n-src) n-dest)))))
+  (define rev-sorted (reverse-topo-sort (for/list ([(k v) (in-hash nodes)]) k)
+                                        edges))
+  (let loop ([sorted rev-sorted])
+    (cond
+      [(empty? sorted) M]
+      [else
+       (define r (car sorted))
+       (term (let ([,r (new ,(hash-ref nodes r))])
+               ,(loop (cdr sorted))))])))
+
+(define (mentions-node? v r)
+  (let loop ([v v])
+    (cond
+      [(symbol? v) (equal? r v)]
+      [(pair? v) (or (loop (car v)) (loop (cdr v)))]
+      [else #f])))
 
 #|
 
-Random generators
+The first algorithm from this page:
+http://en.wikipedia.org/wiki/Topological_sorting#Algorithms
+
+|#
+(define/contract (reverse-topo-sort nodes edges)
+  (-> (listof any/c) (hash/c any/c (set/c any/c)) (listof any/c))
+  
+  (for ([node (in-list nodes)])
+    (unless (hash-ref edges node #f)
+      (error 'topo-sort "no edge entry for ~s" node)))
+  
+  (define incoming-counts (build-incoming-counts nodes edges))
+  (define (remove-edge src dest)
+    (hash-set! edges src (set-remove (hash-ref edges src) dest))
+    (hash-set! incoming-counts dest (- (hash-ref incoming-counts dest) 1)))
+  
+  (define l '())
+  (define s (for/set ([(n c) (in-hash incoming-counts)]
+                      #:when (zero? c))
+              n))
+  (let loop ()
+    (unless (set-empty? s)
+      (define n (set-first s))
+      (set! s (set-remove s n))
+      (set! l (cons n l))
+      (for ([m (in-set (hash-ref edges n))])
+        (remove-edge n m)
+        (when (zero? (hash-ref incoming-counts m))
+          (set! s (set-add s m))))
+      (loop)))
+  
+  l)
+        
+(define (build-incoming-counts nodes edges)
+  (define incoming-counts (make-hash))
+  (for ([n (in-list nodes)]) (hash-set! incoming-counts n 0))
+  (for ([(n neighbors) (in-hash edges)])
+    (for ([neighbor (in-set neighbors)])
+      (hash-set! incoming-counts neighbor (+ (hash-ref incoming-counts neighbor) 1))))
+  incoming-counts)
+  
+
+#|
+
+Generators
 
 |#
 
@@ -480,8 +556,7 @@ from the given term.
         (implies
          t-type
          (let loop ([Σ+M `(· ,M)])
-           (define new-type 
+           (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0)))
-             (type-check (term (Σ->lets ,(list-ref Σ+M 0) ,(list-ref Σ+M 1)))))
            (and (consistent-with? t-type new-type)
                 (or (v? (list-ref Σ+M 1))
                     (let ([red-res (apply-reduction-relation red Σ+M)])

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-3.rkt

@@ -7,7 +7,7 @@
          racket/match
          racket/list
          racket/contract
-         racket/bool
+         racket/bool racket/set
          (only-in "../stlc/tests-lib.rkt" consistent-with?))
 
 (provide (all-defined-out))
@@ -386,8 +386,8 @@ A top-level evaluator
 
 (define/contract (Eval M)
   (-> M? (or/c "error" 'list 'λ 'ref number?))
-  (define M-t (judgment-holds (typeof ,M τ) τ))
+  (define M-t (type-check M))
-  (unless (pair? M-t)
+  (unless M-t
     (error 'Eval "doesn't typecheck: ~s" M))
   (define res (apply-reduction-relation* red (term (· ,M))))
   (unless (= 1 (length res))
@@ -396,7 +396,7 @@ A top-level evaluator
   (match (car res)
     ["error" "error"]
     [`(,Σ ,N)
-     (define ans-t (judgment-holds (typeof (Σ->lets ,Σ ,N) τ) τ))
+     (define ans-t (type-check N Σ))
      (unless (equal? M-t ans-t)
        (error 'Eval "internal error: type soundness fails for ~s" M))
      (match N
@@ -411,31 +411,107 @@ A top-level evaluator
        [(? number?) N]
        [_ (error 'Eval "internal error: didn't reduce to a value ~s" M)])]))
 
-(define-metafunction stlc
-  Σ->lets : Σ M -> M
-  [(Σ->lets · M) M]
-  [(Σ->lets (x v Σ) M) (let ([x (new v)]) (Σ->lets Σ M))])
-
 #|
 
-A top-level type checker.
+A type checker; the optional argument is a store to use
+for type checking free variables in M.
 
 |#
 
-(define/contract (type-check M)
+(define/contract (type-check M [Σ (term ·)])
-  (-> M? (or/c τ? #f))
+  (->* (M?) (any/c) (or/c τ? #f))
-  (define M-t (judgment-holds (typeof ,M τ) τ))
+  (define M-ts (judgment-holds (typeof ,(Σ+M->M Σ M) τ) τ))
   (cond
-    [(empty? M-t)
+    [(null? M-ts)
      #f]
-    [(null? (cdr M-t))
+    [(null? (cdr M-ts))
-     (car M-t)]
+     (car M-ts)]
     [else
-     (error 'type-check "non-unique type: ~s : ~s" M M-t)]))
+     (error 'type-check "non-unique type: ~s : ~s" M M-ts)]))
+
+;; building an expression out of a store can be done in this model
+;; with just topological sort because there are no recursive types,
+;; so the store will not contain any cycles
+(define (Σ+M->M Σ M)
+  ;; nodes : edges[r -o> v]
+  (define nodes (make-hash))
+  (define edges (make-hash))
+  (let loop ([Σ Σ])
+    (match Σ
+      [`· (void)]
+      [`(,r ,v ,Σ) 
+       (hash-set! nodes r v)
+       (loop Σ)]))
+  
+  (for ([(n rhs) (in-hash nodes)]) (hash-set! edges n (set)))
+  (for ([(n-src rhs) (in-hash nodes)])
+    (for ([(n-dest _) (in-hash nodes)])
+      (when (mentions-node? n-dest rhs)
+        (hash-set! edges n-src (set-add (hash-ref edges n-src) n-dest)))))
+  (define rev-sorted (reverse-topo-sort (for/list ([(k v) (in-hash nodes)]) k)
+                                        edges))
+  (let loop ([sorted rev-sorted])
+    (cond
+      [(empty? sorted) M]
+      [else
+       (define r (car sorted))
+       (term (let ([,r (new ,(hash-ref nodes r))])
+               ,(loop (cdr sorted))))])))
+
+(define (mentions-node? v r)
+  (let loop ([v v])
+    (cond
+      [(symbol? v) (equal? r v)]
+      [(pair? v) (or (loop (car v)) (loop (cdr v)))]
+      [else #f])))
 
 #|
 
-Random generators
+The first algorithm from this page:
+http://en.wikipedia.org/wiki/Topological_sorting#Algorithms
+
+|#
+(define/contract (reverse-topo-sort nodes edges)
+  (-> (listof any/c) (hash/c any/c (set/c any/c)) (listof any/c))
+  
+  (for ([node (in-list nodes)])
+    (unless (hash-ref edges node #f)
+      (error 'topo-sort "no edge entry for ~s" node)))
+  
+  (define incoming-counts (build-incoming-counts nodes edges))
+  (define (remove-edge src dest)
+    (hash-set! edges src (set-remove (hash-ref edges src) dest))
+    (hash-set! incoming-counts dest (- (hash-ref incoming-counts dest) 1)))
+  
+  (define l '())
+  (define s (for/set ([(n c) (in-hash incoming-counts)]
+                      #:when (zero? c))
+              n))
+  (let loop ()
+    (unless (set-empty? s)
+      (define n (set-first s))
+      (set! s (set-remove s n))
+      (set! l (cons n l))
+      (for ([m (in-set (hash-ref edges n))])
+        (remove-edge n m)
+        (when (zero? (hash-ref incoming-counts m))
+          (set! s (set-add s m))))
+      (loop)))
+  
+  l)
+        
+(define (build-incoming-counts nodes edges)
+  (define incoming-counts (make-hash))
+  (for ([n (in-list nodes)]) (hash-set! incoming-counts n 0))
+  (for ([(n neighbors) (in-hash edges)])
+    (for ([neighbor (in-set neighbors)])
+      (hash-set! incoming-counts neighbor (+ (hash-ref incoming-counts neighbor) 1))))
+  incoming-counts)
+  
+
+#|
+
+Generators
 
 |#
 
@@ -485,8 +561,7 @@ from the given term.
         (implies
          t-type
          (let loop ([Σ+M `(· ,M)])
-           (define new-type 
+           (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0)))
-             (type-check (term (Σ->lets ,(list-ref Σ+M 0) ,(list-ref Σ+M 1)))))
            (and (consistent-with? t-type new-type)
                 (or (v? (list-ref Σ+M 1))
                     (let ([red-res (apply-reduction-relation red Σ+M)])
@@ -495,6 +570,5 @@ from the given term.
                              (or (equal? red-t "error")
                                  (loop red-t))))))))))))
 
-
 (define small-counter-example (term (1 cons)))
 (test-equal (check small-counter-example) #f)

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-4.rkt

@@ -9,7 +9,7 @@
          racket/match
          racket/list
          racket/contract
-         racket/bool
+         racket/bool racket/set
          (only-in "../stlc/tests-lib.rkt" consistent-with?))
 
 (provide (all-defined-out))
@@ -388,8 +388,8 @@ A top-level evaluator
 
 (define/contract (Eval M)
   (-> M? (or/c "error" 'list 'λ 'ref number?))
-  (define M-t (judgment-holds (typeof ,M τ) τ))
+  (define M-t (type-check M))
-  (unless (pair? M-t)
+  (unless M-t
     (error 'Eval "doesn't typecheck: ~s" M))
   (define res (apply-reduction-relation* red (term (· ,M))))
   (unless (= 1 (length res))
@@ -398,7 +398,7 @@ A top-level evaluator
   (match (car res)
     ["error" "error"]
     [`(,Σ ,N)
-     (define ans-t (judgment-holds (typeof (Σ->lets ,Σ ,N) τ) τ))
+     (define ans-t (type-check N Σ))
      (unless (equal? M-t ans-t)
        (error 'Eval "internal error: type soundness fails for ~s" M))
      (match N
@@ -413,31 +413,107 @@ A top-level evaluator
        [(? number?) N]
        [_ (error 'Eval "internal error: didn't reduce to a value ~s" M)])]))
 
-(define-metafunction stlc
-  Σ->lets : Σ M -> M
-  [(Σ->lets · M) M]
-  [(Σ->lets (x v Σ) M) (let ([x (new v)]) (Σ->lets Σ M))])
-
 #|
 
-A top-level type checker.
+A type checker; the optional argument is a store to use
+for type checking free variables in M.
 
 |#
 
-(define/contract (type-check M)
+(define/contract (type-check M [Σ (term ·)])
-  (-> M? (or/c τ? #f))
+  (->* (M?) (any/c) (or/c τ? #f))
-  (define M-t (judgment-holds (typeof ,M τ) τ))
+  (define M-ts (judgment-holds (typeof ,(Σ+M->M Σ M) τ) τ))
   (cond
-    [(empty? M-t)
+    [(null? M-ts)
      #f]
-    [(null? (cdr M-t))
+    [(null? (cdr M-ts))
-     (car M-t)]
+     (car M-ts)]
     [else
-     (error 'type-check "non-unique type: ~s : ~s" M M-t)]))
+     (error 'type-check "non-unique type: ~s : ~s" M M-ts)]))
+
+;; building an expression out of a store can be done in this model
+;; with just topological sort because there are no recursive types,
+;; so the store will not contain any cycles
+(define (Σ+M->M Σ M)
+  ;; nodes : edges[r -o> v]
+  (define nodes (make-hash))
+  (define edges (make-hash))
+  (let loop ([Σ Σ])
+    (match Σ
+      [`· (void)]
+      [`(,r ,v ,Σ) 
+       (hash-set! nodes r v)
+       (loop Σ)]))
+  
+  (for ([(n rhs) (in-hash nodes)]) (hash-set! edges n (set)))
+  (for ([(n-src rhs) (in-hash nodes)])
+    (for ([(n-dest _) (in-hash nodes)])
+      (when (mentions-node? n-dest rhs)
+        (hash-set! edges n-src (set-add (hash-ref edges n-src) n-dest)))))
+  (define rev-sorted (reverse-topo-sort (for/list ([(k v) (in-hash nodes)]) k)
+                                        edges))
+  (let loop ([sorted rev-sorted])
+    (cond
+      [(empty? sorted) M]
+      [else
+       (define r (car sorted))
+       (term (let ([,r (new ,(hash-ref nodes r))])
+               ,(loop (cdr sorted))))])))
+
+(define (mentions-node? v r)
+  (let loop ([v v])
+    (cond
+      [(symbol? v) (equal? r v)]
+      [(pair? v) (or (loop (car v)) (loop (cdr v)))]
+      [else #f])))
 
 #|
 
-Random generators
+The first algorithm from this page:
+http://en.wikipedia.org/wiki/Topological_sorting#Algorithms
+
+|#
+(define/contract (reverse-topo-sort nodes edges)
+  (-> (listof any/c) (hash/c any/c (set/c any/c)) (listof any/c))
+  
+  (for ([node (in-list nodes)])
+    (unless (hash-ref edges node #f)
+      (error 'topo-sort "no edge entry for ~s" node)))
+  
+  (define incoming-counts (build-incoming-counts nodes edges))
+  (define (remove-edge src dest)
+    (hash-set! edges src (set-remove (hash-ref edges src) dest))
+    (hash-set! incoming-counts dest (- (hash-ref incoming-counts dest) 1)))
+  
+  (define l '())
+  (define s (for/set ([(n c) (in-hash incoming-counts)]
+                      #:when (zero? c))
+              n))
+  (let loop ()
+    (unless (set-empty? s)
+      (define n (set-first s))
+      (set! s (set-remove s n))
+      (set! l (cons n l))
+      (for ([m (in-set (hash-ref edges n))])
+        (remove-edge n m)
+        (when (zero? (hash-ref incoming-counts m))
+          (set! s (set-add s m))))
+      (loop)))
+  
+  l)
+        
+(define (build-incoming-counts nodes edges)
+  (define incoming-counts (make-hash))
+  (for ([n (in-list nodes)]) (hash-set! incoming-counts n 0))
+  (for ([(n neighbors) (in-hash edges)])
+    (for ([neighbor (in-set neighbors)])
+      (hash-set! incoming-counts neighbor (+ (hash-ref incoming-counts neighbor) 1))))
+  incoming-counts)
+  
+
+#|
+
+Generators
 
 |#
 
@@ -487,8 +563,7 @@ from the given term.
         (implies
          t-type
          (let loop ([Σ+M `(· ,M)])
-           (define new-type 
+           (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0)))
-             (type-check (term (Σ->lets ,(list-ref Σ+M 0) ,(list-ref Σ+M 1)))))
            (and (consistent-with? t-type new-type)
                 (or (v? (list-ref Σ+M 1))
                     (let ([red-res (apply-reduction-relation red Σ+M)])

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-5.rkt

@@ -7,7 +7,7 @@
          racket/match
          racket/list
          racket/contract
-         racket/bool
+         racket/bool racket/set
          (only-in "../stlc/tests-lib.rkt" consistent-with?))
 
 (provide (all-defined-out))
@@ -388,8 +388,8 @@ A top-level evaluator
 
 (define/contract (Eval M)
   (-> M? (or/c "error" 'list 'λ 'ref number?))
-  (define M-t (judgment-holds (typeof ,M τ) τ))
+  (define M-t (type-check M))
-  (unless (pair? M-t)
+  (unless M-t
     (error 'Eval "doesn't typecheck: ~s" M))
   (define res (apply-reduction-relation* red (term (· ,M))))
   (unless (= 1 (length res))
@@ -398,7 +398,7 @@ A top-level evaluator
   (match (car res)
     ["error" "error"]
     [`(,Σ ,N)
-     (define ans-t (judgment-holds (typeof (Σ->lets ,Σ ,N) τ) τ))
+     (define ans-t (type-check N Σ))
      (unless (equal? M-t ans-t)
        (error 'Eval "internal error: type soundness fails for ~s" M))
      (match N
@@ -413,31 +413,107 @@ A top-level evaluator
        [(? number?) N]
        [_ (error 'Eval "internal error: didn't reduce to a value ~s" M)])]))
 
-(define-metafunction stlc
-  Σ->lets : Σ M -> M
-  [(Σ->lets · M) M]
-  [(Σ->lets (x v Σ) M) (let ([x (new v)]) (Σ->lets Σ M))])
-
 #|
 
-A top-level type checker.
+A type checker; the optional argument is a store to use
+for type checking free variables in M.
 
 |#
 
-(define/contract (type-check M)
+(define/contract (type-check M [Σ (term ·)])
-  (-> M? (or/c τ? #f))
+  (->* (M?) (any/c) (or/c τ? #f))
-  (define M-t (judgment-holds (typeof ,M τ) τ))
+  (define M-ts (judgment-holds (typeof ,(Σ+M->M Σ M) τ) τ))
   (cond
-    [(empty? M-t)
+    [(null? M-ts)
      #f]
-    [(null? (cdr M-t))
+    [(null? (cdr M-ts))
-     (car M-t)]
+     (car M-ts)]
     [else
-     (error 'type-check "non-unique type: ~s : ~s" M M-t)]))
+     (error 'type-check "non-unique type: ~s : ~s" M M-ts)]))
+
+;; building an expression out of a store can be done in this model
+;; with just topological sort because there are no recursive types,
+;; so the store will not contain any cycles
+(define (Σ+M->M Σ M)
+  ;; nodes : edges[r -o> v]
+  (define nodes (make-hash))
+  (define edges (make-hash))
+  (let loop ([Σ Σ])
+    (match Σ
+      [`· (void)]
+      [`(,r ,v ,Σ) 
+       (hash-set! nodes r v)
+       (loop Σ)]))
+  
+  (for ([(n rhs) (in-hash nodes)]) (hash-set! edges n (set)))
+  (for ([(n-src rhs) (in-hash nodes)])
+    (for ([(n-dest _) (in-hash nodes)])
+      (when (mentions-node? n-dest rhs)
+        (hash-set! edges n-src (set-add (hash-ref edges n-src) n-dest)))))
+  (define rev-sorted (reverse-topo-sort (for/list ([(k v) (in-hash nodes)]) k)
+                                        edges))
+  (let loop ([sorted rev-sorted])
+    (cond
+      [(empty? sorted) M]
+      [else
+       (define r (car sorted))
+       (term (let ([,r (new ,(hash-ref nodes r))])
+               ,(loop (cdr sorted))))])))
+
+(define (mentions-node? v r)
+  (let loop ([v v])
+    (cond
+      [(symbol? v) (equal? r v)]
+      [(pair? v) (or (loop (car v)) (loop (cdr v)))]
+      [else #f])))
 
 #|
 
-Random generators
+The first algorithm from this page:
+http://en.wikipedia.org/wiki/Topological_sorting#Algorithms
+
+|#
+(define/contract (reverse-topo-sort nodes edges)
+  (-> (listof any/c) (hash/c any/c (set/c any/c)) (listof any/c))
+  
+  (for ([node (in-list nodes)])
+    (unless (hash-ref edges node #f)
+      (error 'topo-sort "no edge entry for ~s" node)))
+  
+  (define incoming-counts (build-incoming-counts nodes edges))
+  (define (remove-edge src dest)
+    (hash-set! edges src (set-remove (hash-ref edges src) dest))
+    (hash-set! incoming-counts dest (- (hash-ref incoming-counts dest) 1)))
+  
+  (define l '())
+  (define s (for/set ([(n c) (in-hash incoming-counts)]
+                      #:when (zero? c))
+              n))
+  (let loop ()
+    (unless (set-empty? s)
+      (define n (set-first s))
+      (set! s (set-remove s n))
+      (set! l (cons n l))
+      (for ([m (in-set (hash-ref edges n))])
+        (remove-edge n m)
+        (when (zero? (hash-ref incoming-counts m))
+          (set! s (set-add s m))))
+      (loop)))
+  
+  l)
+        
+(define (build-incoming-counts nodes edges)
+  (define incoming-counts (make-hash))
+  (for ([n (in-list nodes)]) (hash-set! incoming-counts n 0))
+  (for ([(n neighbors) (in-hash edges)])
+    (for ([neighbor (in-set neighbors)])
+      (hash-set! incoming-counts neighbor (+ (hash-ref incoming-counts neighbor) 1))))
+  incoming-counts)
+  
+
+#|
+
+Generators
 
 |#
 
@@ -487,8 +563,7 @@ from the given term.
         (implies
          t-type
          (let loop ([Σ+M `(· ,M)])
-           (define new-type 
+           (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0)))
-             (type-check (term (Σ->lets ,(list-ref Σ+M 0) ,(list-ref Σ+M 1)))))
            (and (consistent-with? t-type new-type)
                 (or (v? (list-ref Σ+M 1))
                     (let ([red-res (apply-reduction-relation red Σ+M)])

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-6.rkt

@@ -7,7 +7,7 @@
          racket/match
          racket/list
          racket/contract
-         racket/bool
+         racket/bool racket/set
          (only-in "../stlc/tests-lib.rkt" consistent-with?))
 
 (provide (all-defined-out))
@@ -386,8 +386,8 @@ A top-level evaluator
 
 (define/contract (Eval M)
   (-> M? (or/c "error" 'list 'λ 'ref number?))
-  (define M-t (judgment-holds (typeof ,M τ) τ))
+  (define M-t (type-check M))
-  (unless (pair? M-t)
+  (unless M-t
     (error 'Eval "doesn't typecheck: ~s" M))
   (define res (apply-reduction-relation* red (term (· ,M))))
   (unless (= 1 (length res))
@@ -396,7 +396,7 @@ A top-level evaluator
   (match (car res)
     ["error" "error"]
     [`(,Σ ,N)
-     (define ans-t (judgment-holds (typeof (Σ->lets ,Σ ,N) τ) τ))
+     (define ans-t (type-check N Σ))
      (unless (equal? M-t ans-t)
        (error 'Eval "internal error: type soundness fails for ~s" M))
      (match N
@@ -411,31 +411,107 @@ A top-level evaluator
        [(? number?) N]
        [_ (error 'Eval "internal error: didn't reduce to a value ~s" M)])]))
 
-(define-metafunction stlc
-  Σ->lets : Σ M -> M
-  [(Σ->lets · M) M]
-  [(Σ->lets (x v Σ) M) (let ([x (new v)]) (Σ->lets Σ M))])
-
 #|
 
-A top-level type checker.
+A type checker; the optional argument is a store to use
+for type checking free variables in M.
 
 |#
 
-(define/contract (type-check M)
+(define/contract (type-check M [Σ (term ·)])
-  (-> M? (or/c τ? #f))
+  (->* (M?) (any/c) (or/c τ? #f))
-  (define M-t (judgment-holds (typeof ,M τ) τ))
+  (define M-ts (judgment-holds (typeof ,(Σ+M->M Σ M) τ) τ))
   (cond
-    [(empty? M-t)
+    [(null? M-ts)
      #f]
-    [(null? (cdr M-t))
+    [(null? (cdr M-ts))
-     (car M-t)]
+     (car M-ts)]
     [else
-     (error 'type-check "non-unique type: ~s : ~s" M M-t)]))
+     (error 'type-check "non-unique type: ~s : ~s" M M-ts)]))
+
+;; building an expression out of a store can be done in this model
+;; with just topological sort because there are no recursive types,
+;; so the store will not contain any cycles
+(define (Σ+M->M Σ M)
+  ;; nodes : edges[r -o> v]
+  (define nodes (make-hash))
+  (define edges (make-hash))
+  (let loop ([Σ Σ])
+    (match Σ
+      [`· (void)]
+      [`(,r ,v ,Σ) 
+       (hash-set! nodes r v)
+       (loop Σ)]))
+  
+  (for ([(n rhs) (in-hash nodes)]) (hash-set! edges n (set)))
+  (for ([(n-src rhs) (in-hash nodes)])
+    (for ([(n-dest _) (in-hash nodes)])
+      (when (mentions-node? n-dest rhs)
+        (hash-set! edges n-src (set-add (hash-ref edges n-src) n-dest)))))
+  (define rev-sorted (reverse-topo-sort (for/list ([(k v) (in-hash nodes)]) k)
+                                        edges))
+  (let loop ([sorted rev-sorted])
+    (cond
+      [(empty? sorted) M]
+      [else
+       (define r (car sorted))
+       (term (let ([,r (new ,(hash-ref nodes r))])
+               ,(loop (cdr sorted))))])))
+
+(define (mentions-node? v r)
+  (let loop ([v v])
+    (cond
+      [(symbol? v) (equal? r v)]
+      [(pair? v) (or (loop (car v)) (loop (cdr v)))]
+      [else #f])))
 
 #|
 
-Random generators
+The first algorithm from this page:
+http://en.wikipedia.org/wiki/Topological_sorting#Algorithms
+
+|#
+(define/contract (reverse-topo-sort nodes edges)
+  (-> (listof any/c) (hash/c any/c (set/c any/c)) (listof any/c))
+  
+  (for ([node (in-list nodes)])
+    (unless (hash-ref edges node #f)
+      (error 'topo-sort "no edge entry for ~s" node)))
+  
+  (define incoming-counts (build-incoming-counts nodes edges))
+  (define (remove-edge src dest)
+    (hash-set! edges src (set-remove (hash-ref edges src) dest))
+    (hash-set! incoming-counts dest (- (hash-ref incoming-counts dest) 1)))
+  
+  (define l '())
+  (define s (for/set ([(n c) (in-hash incoming-counts)]
+                      #:when (zero? c))
+              n))
+  (let loop ()
+    (unless (set-empty? s)
+      (define n (set-first s))
+      (set! s (set-remove s n))
+      (set! l (cons n l))
+      (for ([m (in-set (hash-ref edges n))])
+        (remove-edge n m)
+        (when (zero? (hash-ref incoming-counts m))
+          (set! s (set-add s m))))
+      (loop)))
+  
+  l)
+        
+(define (build-incoming-counts nodes edges)
+  (define incoming-counts (make-hash))
+  (for ([n (in-list nodes)]) (hash-set! incoming-counts n 0))
+  (for ([(n neighbors) (in-hash edges)])
+    (for ([neighbor (in-set neighbors)])
+      (hash-set! incoming-counts neighbor (+ (hash-ref incoming-counts neighbor) 1))))
+  incoming-counts)
+  
+
+#|
+
+Generators
 
 |#
 
@@ -485,8 +561,7 @@ from the given term.
         (implies
          t-type
          (let loop ([Σ+M `(· ,M)])
-           (define new-type 
+           (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0)))
-             (type-check (term (Σ->lets ,(list-ref Σ+M 0) ,(list-ref Σ+M 1)))))
            (and (consistent-with? t-type new-type)
                 (or (v? (list-ref Σ+M 1))
                     (let ([red-res (apply-reduction-relation red Σ+M)])

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-7.rkt

@@ -9,7 +9,7 @@
          racket/match
          racket/list
          racket/contract
-         racket/bool
+         racket/bool racket/set
          (only-in "../stlc/tests-lib.rkt" consistent-with?))
 
 (provide (all-defined-out))
@@ -387,8 +387,8 @@ A top-level evaluator
 
 (define/contract (Eval M)
   (-> M? (or/c "error" 'list 'λ 'ref number?))
-  (define M-t (judgment-holds (typeof ,M τ) τ))
+  (define M-t (type-check M))
-  (unless (pair? M-t)
+  (unless M-t
     (error 'Eval "doesn't typecheck: ~s" M))
   (define res (apply-reduction-relation* red (term (· ,M))))
   (unless (= 1 (length res))
@@ -397,7 +397,7 @@ A top-level evaluator
   (match (car res)
     ["error" "error"]
     [`(,Σ ,N)
-     (define ans-t (judgment-holds (typeof (Σ->lets ,Σ ,N) τ) τ))
+     (define ans-t (type-check N Σ))
      (unless (equal? M-t ans-t)
        (error 'Eval "internal error: type soundness fails for ~s" M))
      (match N
@@ -412,31 +412,107 @@ A top-level evaluator
        [(? number?) N]
        [_ (error 'Eval "internal error: didn't reduce to a value ~s" M)])]))
 
-(define-metafunction stlc
-  Σ->lets : Σ M -> M
-  [(Σ->lets · M) M]
-  [(Σ->lets (x v Σ) M) (let ([x (new v)]) (Σ->lets Σ M))])
-
 #|
 
-A top-level type checker.
+A type checker; the optional argument is a store to use
+for type checking free variables in M.
 
 |#
 
-(define/contract (type-check M)
+(define/contract (type-check M [Σ (term ·)])
-  (-> M? (or/c τ? #f))
+  (->* (M?) (any/c) (or/c τ? #f))
-  (define M-t (judgment-holds (typeof ,M τ) τ))
+  (define M-ts (judgment-holds (typeof ,(Σ+M->M Σ M) τ) τ))
   (cond
-    [(empty? M-t)
+    [(null? M-ts)
      #f]
-    [(null? (cdr M-t))
+    [(null? (cdr M-ts))
-     (car M-t)]
+     (car M-ts)]
     [else
-     (error 'type-check "non-unique type: ~s : ~s" M M-t)]))
+     (error 'type-check "non-unique type: ~s : ~s" M M-ts)]))
+
+;; building an expression out of a store can be done in this model
+;; with just topological sort because there are no recursive types,
+;; so the store will not contain any cycles
+(define (Σ+M->M Σ M)
+  ;; nodes : edges[r -o> v]
+  (define nodes (make-hash))
+  (define edges (make-hash))
+  (let loop ([Σ Σ])
+    (match Σ
+      [`· (void)]
+      [`(,r ,v ,Σ) 
+       (hash-set! nodes r v)
+       (loop Σ)]))
+  
+  (for ([(n rhs) (in-hash nodes)]) (hash-set! edges n (set)))
+  (for ([(n-src rhs) (in-hash nodes)])
+    (for ([(n-dest _) (in-hash nodes)])
+      (when (mentions-node? n-dest rhs)
+        (hash-set! edges n-src (set-add (hash-ref edges n-src) n-dest)))))
+  (define rev-sorted (reverse-topo-sort (for/list ([(k v) (in-hash nodes)]) k)
+                                        edges))
+  (let loop ([sorted rev-sorted])
+    (cond
+      [(empty? sorted) M]
+      [else
+       (define r (car sorted))
+       (term (let ([,r (new ,(hash-ref nodes r))])
+               ,(loop (cdr sorted))))])))
+
+(define (mentions-node? v r)
+  (let loop ([v v])
+    (cond
+      [(symbol? v) (equal? r v)]
+      [(pair? v) (or (loop (car v)) (loop (cdr v)))]
+      [else #f])))
 
 #|
 
-Random generators
+The first algorithm from this page:
+http://en.wikipedia.org/wiki/Topological_sorting#Algorithms
+
+|#
+(define/contract (reverse-topo-sort nodes edges)
+  (-> (listof any/c) (hash/c any/c (set/c any/c)) (listof any/c))
+  
+  (for ([node (in-list nodes)])
+    (unless (hash-ref edges node #f)
+      (error 'topo-sort "no edge entry for ~s" node)))
+  
+  (define incoming-counts (build-incoming-counts nodes edges))
+  (define (remove-edge src dest)
+    (hash-set! edges src (set-remove (hash-ref edges src) dest))
+    (hash-set! incoming-counts dest (- (hash-ref incoming-counts dest) 1)))
+  
+  (define l '())
+  (define s (for/set ([(n c) (in-hash incoming-counts)]
+                      #:when (zero? c))
+              n))
+  (let loop ()
+    (unless (set-empty? s)
+      (define n (set-first s))
+      (set! s (set-remove s n))
+      (set! l (cons n l))
+      (for ([m (in-set (hash-ref edges n))])
+        (remove-edge n m)
+        (when (zero? (hash-ref incoming-counts m))
+          (set! s (set-add s m))))
+      (loop)))
+  
+  l)
+        
+(define (build-incoming-counts nodes edges)
+  (define incoming-counts (make-hash))
+  (for ([n (in-list nodes)]) (hash-set! incoming-counts n 0))
+  (for ([(n neighbors) (in-hash edges)])
+    (for ([neighbor (in-set neighbors)])
+      (hash-set! incoming-counts neighbor (+ (hash-ref incoming-counts neighbor) 1))))
+  incoming-counts)
+  
+
+#|
+
+Generators
 
 |#
 
@@ -486,8 +562,7 @@ from the given term.
         (implies
          t-type
          (let loop ([Σ+M `(· ,M)])
-           (define new-type 
+           (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0)))
-             (type-check (term (Σ->lets ,(list-ref Σ+M 0) ,(list-ref Σ+M 1)))))
            (and (consistent-with? t-type new-type)
                 (or (v? (list-ref Σ+M 1))
                     (let ([red-res (apply-reduction-relation red Σ+M)])

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-base.rkt

@@ -7,7 +7,7 @@
          racket/match
          racket/list
          racket/contract
-         racket/bool
+         racket/bool racket/set
          (only-in "../stlc/tests-lib.rkt" consistent-with?))
 
 (provide (all-defined-out))
@@ -386,8 +386,8 @@ A top-level evaluator
 
 (define/contract (Eval M)
   (-> M? (or/c "error" 'list 'λ 'ref number?))
-  (define M-t (judgment-holds (typeof ,M τ) τ))
+  (define M-t (type-check M))
-  (unless (pair? M-t)
+  (unless M-t
     (error 'Eval "doesn't typecheck: ~s" M))
   (define res (apply-reduction-relation* red (term (· ,M))))
   (unless (= 1 (length res))
@@ -396,7 +396,7 @@ A top-level evaluator
   (match (car res)
     ["error" "error"]
     [`(,Σ ,N)
-     (define ans-t (judgment-holds (typeof (Σ->lets ,Σ ,N) τ) τ))
+     (define ans-t (type-check N Σ))
      (unless (equal? M-t ans-t)
        (error 'Eval "internal error: type soundness fails for ~s" M))
      (match N
@@ -411,31 +411,107 @@ A top-level evaluator
        [(? number?) N]
        [_ (error 'Eval "internal error: didn't reduce to a value ~s" M)])]))
 
-(define-metafunction stlc
-  Σ->lets : Σ M -> M
-  [(Σ->lets · M) M]
-  [(Σ->lets (x v Σ) M) (let ([x (new v)]) (Σ->lets Σ M))])
-
 #|
 
-A top-level type checker.
+A type checker; the optional argument is a store to use
+for type checking free variables in M.
 
 |#
 
-(define/contract (type-check M)
+(define/contract (type-check M [Σ (term ·)])
-  (-> M? (or/c τ? #f))
+  (->* (M?) (any/c) (or/c τ? #f))
-  (define M-t (judgment-holds (typeof ,M τ) τ))
+  (define M-ts (judgment-holds (typeof ,(Σ+M->M Σ M) τ) τ))
   (cond
-    [(empty? M-t)
+    [(null? M-ts)
      #f]
-    [(null? (cdr M-t))
+    [(null? (cdr M-ts))
-     (car M-t)]
+     (car M-ts)]
     [else
-     (error 'type-check "non-unique type: ~s : ~s" M M-t)]))
+     (error 'type-check "non-unique type: ~s : ~s" M M-ts)]))
+
+;; building an expression out of a store can be done in this model
+;; with just topological sort because there are no recursive types,
+;; so the store will not contain any cycles
+(define (Σ+M->M Σ M)
+  ;; nodes : edges[r -o> v]
+  (define nodes (make-hash))
+  (define edges (make-hash))
+  (let loop ([Σ Σ])
+    (match Σ
+      [`· (void)]
+      [`(,r ,v ,Σ) 
+       (hash-set! nodes r v)
+       (loop Σ)]))
+  
+  (for ([(n rhs) (in-hash nodes)]) (hash-set! edges n (set)))
+  (for ([(n-src rhs) (in-hash nodes)])
+    (for ([(n-dest _) (in-hash nodes)])
+      (when (mentions-node? n-dest rhs)
+        (hash-set! edges n-src (set-add (hash-ref edges n-src) n-dest)))))
+  (define rev-sorted (reverse-topo-sort (for/list ([(k v) (in-hash nodes)]) k)
+                                        edges))
+  (let loop ([sorted rev-sorted])
+    (cond
+      [(empty? sorted) M]
+      [else
+       (define r (car sorted))
+       (term (let ([,r (new ,(hash-ref nodes r))])
+               ,(loop (cdr sorted))))])))
+
+(define (mentions-node? v r)
+  (let loop ([v v])
+    (cond
+      [(symbol? v) (equal? r v)]
+      [(pair? v) (or (loop (car v)) (loop (cdr v)))]
+      [else #f])))
 
 #|
 
-Random generators
+The first algorithm from this page:
+http://en.wikipedia.org/wiki/Topological_sorting#Algorithms
+
+|#
+(define/contract (reverse-topo-sort nodes edges)
+  (-> (listof any/c) (hash/c any/c (set/c any/c)) (listof any/c))
+  
+  (for ([node (in-list nodes)])
+    (unless (hash-ref edges node #f)
+      (error 'topo-sort "no edge entry for ~s" node)))
+  
+  (define incoming-counts (build-incoming-counts nodes edges))
+  (define (remove-edge src dest)
+    (hash-set! edges src (set-remove (hash-ref edges src) dest))
+    (hash-set! incoming-counts dest (- (hash-ref incoming-counts dest) 1)))
+  
+  (define l '())
+  (define s (for/set ([(n c) (in-hash incoming-counts)]
+                      #:when (zero? c))
+              n))
+  (let loop ()
+    (unless (set-empty? s)
+      (define n (set-first s))
+      (set! s (set-remove s n))
+      (set! l (cons n l))
+      (for ([m (in-set (hash-ref edges n))])
+        (remove-edge n m)
+        (when (zero? (hash-ref incoming-counts m))
+          (set! s (set-add s m))))
+      (loop)))
+  
+  l)
+        
+(define (build-incoming-counts nodes edges)
+  (define incoming-counts (make-hash))
+  (for ([n (in-list nodes)]) (hash-set! incoming-counts n 0))
+  (for ([(n neighbors) (in-hash edges)])
+    (for ([neighbor (in-set neighbors)])
+      (hash-set! incoming-counts neighbor (+ (hash-ref incoming-counts neighbor) 1))))
+  incoming-counts)
+  
+
+#|
+
+Generators
 
 |#
 
@@ -485,8 +561,7 @@ from the given term.
         (implies
          t-type
          (let loop ([Σ+M `(· ,M)])
-           (define new-type 
+           (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0)))
-             (type-check (term (Σ->lets ,(list-ref Σ+M 0) ,(list-ref Σ+M 1)))))
            (and (consistent-with? t-type new-type)
                 (or (v? (list-ref Σ+M 1))
                     (let ([red-res (apply-reduction-relation red Σ+M)])

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/tests.rkt

@@ -1,7 +1,51 @@
 #lang racket/base
 (require "let-poly-base.rkt" 
          (only-in "../stlc/tests-lib.rkt" consistent-with?)
-         redex/reduction-semantics)
+         redex/reduction-semantics
+         racket/set)
+
+(test-equal (build-incoming-counts '(x y z) 
+                                   (make-hash (list (cons 'x (set 'y 'z))
+                                                    (cons 'y (set 'z))
+                                                    (cons 'z (set)))))
+            (make-hash (list (cons 'x 0)
+                             (cons 'y 1)
+                             (cons 'z 2))))
+(test-equal (reverse-topo-sort '() (make-hash)) '())
+(test-equal (reverse-topo-sort '(x) 
+                               (make-hash (list (cons 'x (set)))))
+            '(x))
+(test-equal (reverse-topo-sort '(x y) 
+                               (make-hash (list (cons 'y (set))
+                                                (cons 'x (set 'y)))))
+            '(y x))
+(test-equal (reverse-topo-sort '(y x) 
+                               (make-hash (list (cons 'y (set))
+                                                (cons 'x (set 'y)))))
+            '(y x))
+(test-equal (reverse-topo-sort '(x y z) 
+                               (make-hash (list (cons 'x (set 'y))
+                                                (cons 'y (set 'z))
+                                                (cons 'z (set)))))
+            '(z y x))
+(test-equal (reverse-topo-sort '(x y z) 
+                               (make-hash (list (cons 'x (set 'y 'z))
+                                                (cons 'y (set 'z))
+                                                (cons 'z (set)))))
+            '(z y x))
+(define (one-of? a . bs) (for/or ([b (in-list bs)]) (equal? a b)))
+(test-equal (one-of? (reverse-topo-sort '(x y z) 
+                                        (make-hash (list (cons 'x (set 'z))
+                                                         (cons 'y (set 'z))
+                                                         (cons 'z (set)))))
+                     '(z x y)
+                     '(z y x))
+            #t)
+
+(test-equal (Σ+M->M (term (r1 r2 (r2 1 ·))) (term 2))
+            (term (let ([r2 (new 1)]) (let ([r1 (new r2)]) 2))))
+(test-equal (Σ+M->M (term (r2 1 (r1 r2 ·))) (term 2))
+            (term (let ([r2 (new 1)]) (let ([r1 (new r2)]) 2))))
 
 (test-equal (term (subst ((+ 1) 1) x 2))
             (term ((+ 1) 1)))
@@ -192,3 +236,10 @@
             (term int))
 (test-equal (type-check (term (5 5)))
             #f)
+(test-equal (type-check (term r1) (term (r1 r (r 1 ·))))
+            (term (ref (ref int))))
+(test-equal (type-check (term r1) (term (r 1 (r1 r ·))))
+            (term (ref (ref int))))
+
+(test-equal (check (term 1)) #t)
+(test-equal (check (term (new (new hd)))) #t)