www

commit 0ffbdffc8b627e4cc3e8d116d542ee29e694d347
parent c4ab4510eeb5d11b41cb1a74067db29753aa3e41
Author: AlexKnauth <alexander@knauth.org>
Date:   Mon, 13 Jun 2016 10:49:59 -0400

infer.rkt: use find-free-Xs, propagate expected type more

Diffstat:
M
tapl/infer.rkt
 | 
28
+++++++++++++++-------------

1 file changed, 15 insertions(+), 13 deletions(-)
diff --git a/tapl/infer.rkt b/tapl/infer.rkt
@@ -30,6 +30,13 @@
 (define-primop abs : (→ Int Int))
 
 (begin-for-syntax
+  ;; find-free-Xs : (Stx-Listof Id) Type -> (Listof Id)
+  ;; finds the free Xs in the type
+  (define (find-free-Xs Xs ty)
+    (for/list ([X (in-list (stx->list Xs))]
+               #:when (stx-contains-id? ty X))
+      X))
+
   ;; solve : (Stx-Listof Id) (Stx-Listof Stx) (Stx-Listof Type-Stx)
   ;;         -> (List Constraints (Listof (Stx-List Stx Type-Stx)))
   ;; Solves for the Xs by inferring the type of each arg and unifying it against
@@ -43,19 +50,14 @@
           (for/fold ([cs #'()] [e+τs #'()])
                     ([e_arg (syntax->list args)]
                      [τ_inX (syntax->list expected-τs)])
-            (define/with-syntax τs_solved (stx-map (λ (y) (lookup y cs)) Xs))
-            (cond
-              [(andmap syntax-e (syntax->list #'τs_solved)) ; all tyvars X have mapping
-               ; TODO: substs is not properly transferring #%type property
-               ;               (stx-map displayln #'τs_solved)
-               (define e+τ (infer+erase #`(add-expected #,e_arg #,(substs #'τs_solved Xs τ_inX))))
-               ;              (displayln e+τ)
-               (values cs (cons e+τ e+τs))]
-              [else
-               (define/with-syntax [e τ] (infer+erase e_arg))
-               ;             (displayln #'(e τ))
-               (define cs* (add-constraints Xs cs #`([#,τ_inX τ])))
-               (values cs* (cons #'[e τ] e+τs))]))])
+            (define τ_in (inst-type/cs Xs cs τ_inX))
+            (define/with-syntax [e τ]
+              (infer+erase (if (empty? (find-free-Xs Xs τ_in))
+                               (add-expected-ty e_arg τ_in)
+                               e_arg)))
+            ;             (displayln #'(e τ))
+            (define cs* (add-constraints Xs cs #`([#,τ_in τ])))
+            (values cs* (cons #'[e τ] e+τs)))])
       (list cs (reverse (stx->list e+τs))))))
 
 (define-typed-syntax define