From da3ecfa7803d998c7da7f3446e2bba15e2711f10 Mon Sep 17 00:00:00 2001
From: AlexKnauth <alexander@knauth.org>
Date: Fri, 24 Jun 2016 12:25:07 -0400
Subject: [PATCH] refactor type-constraints a bit

---
 macrotypes/examples/infer.rkt   |  2 +-
 macrotypes/examples/mlish.rkt   |  2 +-
 macrotypes/type-constraints.rkt | 27 ++++++++++++++++++++-------
 turnstile/examples/mlish.rkt    |  2 +-
 4 files changed, 23 insertions(+), 10 deletions(-)

diff --git a/macrotypes/examples/infer.rkt b/macrotypes/examples/infer.rkt
index 333e2a0..370e5d1 100644
--- a/macrotypes/examples/infer.rkt
+++ b/macrotypes/examples/infer.rkt
@@ -47,7 +47,7 @@
   (define (solve Xs args expected-τs)
     (let-values
         ([(cs e+τs)
-          (for/fold ([cs #'()] [e+τs #'()])
+          (for/fold ([cs '()] [e+τs #'()])
                     ([e_arg (syntax->list args)]
                      [τ_inX (syntax->list expected-τs)])
             (define τ_in (inst-type/cs Xs cs τ_inX))
diff --git a/macrotypes/examples/mlish.rkt b/macrotypes/examples/mlish.rkt
index 37ab703..8c5dbcb 100644
--- a/macrotypes/examples/mlish.rkt
+++ b/macrotypes/examples/mlish.rkt
@@ -90,7 +90,7 @@
        (define initial-cs
          (if (and (syntax-e #'expected-ty) (stx-null? #'Vs))
              (add-constraints Xs '() (list (list #'expected-ty #'τ_outX)))
-             #'()))
+             '()))
        (syntax-parse stx
          [(_ e_fn . args)
           (define-values (as- cs)
diff --git a/macrotypes/type-constraints.rkt b/macrotypes/type-constraints.rkt
index 34d6e88..8d6fd33 100644
--- a/macrotypes/type-constraints.rkt
+++ b/macrotypes/type-constraints.rkt
@@ -43,17 +43,13 @@
                #'rst)
          orig-cs)]
        [else
+        (define entry (list #'a #'b))
         (add-constraints
          Xs*
          ;; Add the mapping #'a -> #'b to the substitution,
-         (cons (list #'a #'b)
-               (for/list ([subst (in-list (stx->list substs))])
-                 (list (stx-car subst)
-                       (inst-type (list #'b) (list #'a) (stx-cadr subst)))))
+         (add-substitution-entry entry substs)
          ;; and substitute that in each of the constraints.
-         (for/list ([c (in-list (syntax->list #'rst))])
-           (list (inst-type (list #'b) (list #'a) (stx-car c))
-                 (inst-type (list #'b) (list #'a) (stx-cadr c))))
+         (cs-substitute-entry entry #'rst)
          orig-cs)])]
     [([a b:var] . rst)
      (add-constraints Xs*
@@ -104,6 +100,23 @@
                                      (string-join (map type->str (stx-map stx-cadr orig-cs)) ", "))
                        #'a #'b)])])]))
 
+;; add-substitution-entry : (List Id Type) (Listof (List Id Type)) -> (Listof (List Id Type))
+;; Adds the mapping a -> b to the substitution and substitutes for it in the other entries
+(define (add-substitution-entry entry substs)
+  (match-define (list a b) entry)
+  (cons entry
+        (for/list ([subst (in-list substs)])
+          (list (first subst)
+                (inst-type (list b) (list a) (second subst))))))
+
+;; cs-substitute-entry : (List Id Type) (Stx-Listof (Stx-List Stx Stx)) -> (Listof (List Stx Stx))
+;; substitute a -> b in each of the constraints
+(define (cs-substitute-entry entry cs)
+  (match-define (list a b) entry)
+  (for/list ([c (in-list (stx->list cs))])
+    (list (inst-type (list b) (list a) (stx-car c))
+          (inst-type (list b) (list a) (stx-cadr c)))))
+
 (define (lookup x substs)
   (syntax-parse substs
     [((y:id τ) . rst)
diff --git a/turnstile/examples/mlish.rkt b/turnstile/examples/mlish.rkt
index 71ec1cd..d6bc275 100644
--- a/turnstile/examples/mlish.rkt
+++ b/turnstile/examples/mlish.rkt
@@ -90,7 +90,7 @@
        (define initial-cs
          (if (and (syntax-e #'expected-ty) (stx-null? #'Vs))
              (add-constraints Xs '() (list (list #'expected-ty #'τ_outX)))
-             #'()))
+             '()))
        (syntax-parse stx
          [(_ e_fn . args)
           (define-values (as- cs)