From f0d314b46d90eeebd47441367e1e732d2c87312c Mon Sep 17 00:00:00 2001
From: Stephen Chang <stchang@ccs.neu.edu>
Date: Thu, 9 Jul 2015 15:30:12 -0400
Subject: [PATCH] consolidate typecheck.rkt: impl everything in terms of infer
 fn

---
 tapl/exist.rkt     |  1 -
 tapl/fomega2.rkt   |  6 +++---
 tapl/typecheck.rkt | 21 ++++++++++++++++-----
 3 files changed, 19 insertions(+), 9 deletions(-)

diff --git a/tapl/exist.rkt b/tapl/exist.rkt
index 080edd0..088de92 100644
--- a/tapl/exist.rkt
+++ b/tapl/exist.rkt
@@ -40,7 +40,6 @@
      #:when (typecheck? #'τ_e  (subst #'τ.norm #'τ_abstract #'τ_body))
      (⊢ #'e- #'∃τ)]))
 
-; TODO: the colon syntax might be misleading, since tv is not the type of x
 (define-syntax (open stx)
   (syntax-parse stx #:datum-literals (<=)
     [(_ ([(tv:id x:id) <= e_packed]) e)
diff --git a/tapl/fomega2.rkt b/tapl/fomega2.rkt
index 1cd68ea..bf094a9 100644
--- a/tapl/fomega2.rkt
+++ b/tapl/fomega2.rkt
@@ -163,8 +163,8 @@
      #:fail-unless (→? #'τ_fn)
                    (format "Type error: Attempting to apply a non-function ~a with type ~a\n"
                            (syntax->datum #'e_fn) (syntax->datum #'τ_fn))
-     #:with ((~literal #%plain-app) _ τ ... τ_res) #'τ_fn
-     #:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...))
+     #:with ((~literal #%plain-app) _ τ:type ... τ_res) #'τ_fn
+     #:with ([e_arg- τ_arg:type] ...) (infers+erase #'(e_arg ...))
      #:fail-unless (stx-length=? #'(τ_arg ...) #'(τ ...))
                    (string-append
                     (format
@@ -177,7 +177,7 @@
                       (syntax->datum #`#,(stx-map get-orig #'(τ_arg ...))))
                      ", ")
                     (format "\nexpected: ~a argument(s)." (stx-length #'(τ ...))))
-     #:fail-unless (typechecks? #'(τ_arg ...) #'(τ ...))
+     #:fail-unless (typechecks? #'(τ_arg.norm ...) #'(τ.norm ...))
                    (string-append
                     (format
                      "Arguments to function ~a have wrong type:\ngiven: "
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
index 550d6d3..2b6f3fd 100644
--- a/tapl/typecheck.rkt
+++ b/tapl/typecheck.rkt
@@ -137,12 +137,18 @@
   ;; infers type and erases types in a single expression,
   ;; in the context of the given bindings and their types
   (define (infer/type-ctxt+erase x+τs e)
-    (syntax-parse (infers/type-ctxt+erase x+τs (list e))
+    (syntax-parse (infer (list e) #:ctx x+τs)
+      [(_ xs (e+) (τ)) (list #'xs #'e+ #'τ)])
+    #;(syntax-parse (infers/type-ctxt+erase x+τs (list e))
       [(xs (e+) (τ)) (list #'xs #'e+ #'τ)]))
   ;; infers type and erases types in multiple expressions,
   ;; in the context of (one set of) given bindings and their tpyes
   (define (infers/type-ctxt+erase ctxt es)
-    (syntax-parse ctxt
+    ;(printf "~a\n" (infer es #:ctx ctxt))
+    (stx-cdr (infer es #:ctx ctxt)) ; drop (empty) tyvars from result
+    #;(syntax-parse (infer es #:ctx ctxt)
+      [(tvs xs es+ τs) (list #'xs #'es+ #'τs)])
+    #;(syntax-parse ctxt
       [(b:typed-binding ...)
        #:with (x ...) #'(b.x ...)
        #:with (τ ...) #'(b.τ ...)
@@ -168,10 +174,14 @@
     (stx-map infer+erase es))
   ;; infers and erases types in an expression, in the context of given type vars
   (define (infer/tvs+erase e tvs)
-    (syntax-parse (expand/df #`(λ #,tvs (#%expression #,e))) #:literals (#%expression)
+    (syntax-parse (infer (list e) #:tvs tvs)
+      [(tvs xs (e+) (τ)) (list #'tvs #'e+ #'τ)])
+    #;(syntax-parse (expand/df #`(λ #,tvs (#%expression #,e))) #:literals (#%expression)
       [(lam tvs+ (#%expression e+))
        (list #'tvs+ #'e+ (syntax-local-introduce (typeof #'e+)))]))
 
+  ;; This is the main "infer" function. All others are defined in terms of this.
+  ;; It should be named infer+erase but leaving it for now for backward compat.
   (define (infer es #:ctx [ctx null] #:tvs [tvs null])
     (syntax-parse ctx #:datum-literals (:)
       [([x : τ] ...) ; dont expand yet bc τ may have references to tvs
@@ -190,8 +200,9 @@
             (λ (x ...)
               (let-syntax ([x (make-rename-transformer (⊢ #'x #'τ))] ...)
                 (#%expression e) ...))))
-       (list #'tvs+ #'xs+ #'(e+ ...) (stx-map syntax-local-introduce (stx-map typeof #'(e+ ...))))]
-      [([x τ] ...) (infer+erase es #:ctx #'([x : τ] ...) #:tvs tvs)]))
+       (list #'tvs+ #'xs+ #'(e+ ...)
+             (stx-map syntax-local-introduce (stx-map typeof #'(e+ ...))))]
+      [([x τ] ...) (infer es #:ctx #'([x : τ] ...) #:tvs tvs)]))
 
   (define current-typecheck-relation (make-parameter #f))
   (define (typecheck? t1 t2) ((current-typecheck-relation) t1 t2))