From c5e442a44248b55893063ad8fa32f6ec01b8ad02 Mon Sep 17 00:00:00 2001
From: Asumu Takikawa <asumu@ccs.neu.edu>
Date: Tue, 28 Jan 2014 11:10:52 -0500
Subject: [PATCH] Check kw function definitions w/o type annotations

Instead of trying to check the expansion as-is (which
always fails), check the core function and reconstruct the
keyword function type.

Closes PR 11253

original commit: dc41219463e43457dac6de873440036c6e8c5c3d
---
 .../typed-racket/typecheck/tc-expr-unit.rkt   |  17 +++
 .../typed-racket/types/kw-types.rkt           | 112 +++++++++++++++++-
 .../unit-tests/typecheck-tests.rkt            |  29 +++++
 3 files changed, 156 insertions(+), 2 deletions(-)

diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
index 77a27ae4..cf45102d 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
@@ -365,6 +365,23 @@
                    ignore-this-case
                    (#%plain-app _ _ _arg-var2 ...))))))
        (tc/send #'find-app #'rcvr #'meth #'(args ...))]
+      ;; kw function def
+      [(~and _:kw-lambda^
+             (let-values ([(f) fun])
+               (let-values _
+                 (#%plain-app
+                  maker
+                  lambda-for-kws
+                  (case-lambda ; wrapper function
+                    (formals . cl-body) ...)
+                  (~or (quote (mand-kw:keyword ...))
+                       (~and _ (~bind [(mand-kw 1) '()])))
+                  (quote (all-kw:keyword ...))
+                  . rst))))
+       (ret (kw-unconvert (tc-expr/t #'fun)
+                          (syntax->list #'(formals ...))
+                          (syntax->datum #'(mand-kw ...))
+                          (syntax->datum #'(all-kw ...))))]
       ;; let
       [(let-values ([(name ...) expr] ...) . body)
        (tc/let-values #'((name ...) ...) #'(expr ...) #'body form)]
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/kw-types.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/kw-types.rkt
index 9daa8804..9b59c242 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/kw-types.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/kw-types.rkt
@@ -2,7 +2,8 @@
 
 (require "abbrev.rkt" "../rep/type-rep.rkt"
          "../utils/tc-utils.rkt"
-         racket/list racket/set racket/dict racket/match)
+         racket/list racket/set racket/dict racket/match
+         syntax/parse)
 
 ;; convert : [Listof Keyword] [Listof Type] [Listof Type] [Option Type]
 ;;           [Option Type] [Option (Pair Type symbol)] boolean -> Type
@@ -130,6 +131,113 @@
       [(PolyDots-names: names f)
        (make-PolyDots names (kw-convert f #:split split?))]))
 
+;; kw-unconvert : Type (Listof Syntax) (Listof Keyword) (Listof Keyword) -> Type
+;; Given a type for a core keyword function, unconvert it to a
+;; normal function type.
+;;
+;; precondition: only call this for functions with no type annotations,
+;;               which means they will never have polymorphic types.
+(define (kw-unconvert ft formalss mand-keywords keywords)
+  (define (lengthish formals)
+    (define lst (syntax->list formals))
+    (if lst (length lst) +inf.0))
+  ;; only need longest formals and smallest formals to determine
+  ;; which arguments are optional non-kw arguments
+  (define max-formals (argmax lengthish formalss))
+  (define min-formals (argmin lengthish formalss))
+  (define-values (raw-non-kw-argc rest?)
+    (syntax-parse max-formals
+      [(_ _ non-kw:id ...)
+       (values (length (syntax->list #'(non-kw ...))) #f)]
+      [(_ _ non-kw:id ... . rst:id)
+       (values (length (syntax->list #'(non-kw ...))) #t)]))
+  (define opt-non-kw-argc
+    (syntax-parse min-formals
+      [(_ _ non-kw:id ...)
+       (- raw-non-kw-argc (length (syntax->list #'(non-kw ...))))]
+      ;; if min and max both have rest args, then there cannot
+      ;; have been any optional arguments
+      [(_ _ non-kw:id ... . rst:id) 0]))
+  ;; counted twice since optionals expand to two arguments
+  (define non-kw-argc (+ raw-non-kw-argc opt-non-kw-argc))
+  (define mand-non-kw-argc (- non-kw-argc (* 2 opt-non-kw-argc)))
+  (match ft
+    [(Function: arrs)
+     (cond [(= (length arrs) 1) ; no optional args (either kw or not)
+            (match-define (arr: doms rng _ _ _) (car arrs))
+            (define kw-length
+              (- (length doms) (+ non-kw-argc (if rest? 1 0))))
+            (define-values (kw-args other-args) (split-at doms kw-length))
+            (define actual-kws
+              (for/list ([kw (in-list keywords)]
+                         [kw-type (in-list kw-args)])
+                (make-Keyword kw kw-type #t)))
+            (define rest-type
+              (and rest?
+                   (if (equal? (last other-args) Univ)
+                       Univ
+                       -Bottom)))
+            (make-Function
+             (list (make-arr* (take other-args non-kw-argc)
+                              rng
+                              #:kws actual-kws
+                              #:rest rest-type)))]
+           [(and (even? (length arrs)) ; had optional args
+                 (>= (length arrs) 2))
+            ;; assumption: only one arr is needed, since the types for
+            ;; the actual domain are the same (the difference is in the
+            ;; second type for the optional keyword protocol)
+            (match-define (arr: doms rng _ _ _) (car arrs))
+            (define kw-length
+              (- (length doms) (+ non-kw-argc (if rest? 1 0))))
+            (define kw-args (take doms kw-length))
+            (define actual-kws (compute-kws mand-keywords keywords kw-args))
+            (define other-args (drop doms kw-length))
+            (define-values (mand-args opt-and-rest-args)
+              (split-at other-args mand-non-kw-argc))
+            (define rest-type
+              (and rest?
+                   (if (equal? (last opt-and-rest-args) Univ)
+                       Univ
+                       -Bottom)))
+            (define opt-types
+              (let loop ([opt-args opt-and-rest-args]
+                         [opt-types '()])
+                (if (or (null? opt-args)
+                        (null? (cdr opt-args)))
+                    (reverse opt-types)
+                    (loop (cddr opt-args) (cons (car opt-args) opt-types)))))
+            (make-Function
+             (for/list ([to-take (in-range (add1 (length opt-types)))])
+               (make-arr* (append mand-args (take opt-types to-take))
+                          rng
+                          #:kws actual-kws
+                          #:rest rest-type)))]
+           [else (int-err "unsupported arrs in keyword function type")])]
+    [_ (int-err "unsupported keyword function type")]))
+
+;; compute-kws : (Listof Keyword) (Listof Keyword) (Listof Type)
+;;               -> (Listof make-Keyword)
+;; Computes the keyword types for an arr in kw-unconvert
+;;
+;; assumptions: (1) in kw-args, there are two types per optional kw
+;;                  and the first type is the argument type (which is
+;;                  the same in every `arr` in the function type)
+;;              (2) kw-args and keywords are sorted by keyword<? order
+(define (compute-kws mand-keywords keywords kw-args)
+  (let loop ([kw-args kw-args]
+             [keywords keywords]
+             [kw-types '()])
+    (cond [(empty? kw-args) (reverse kw-types)]
+          [(memq (car keywords) mand-keywords)
+           (loop (cdr kw-args) (cdr keywords)
+                 (cons (make-Keyword (car keywords) (car kw-args) #t)
+                       kw-types))]
+          [else ; optional, so there are two arg types
+           (loop (cddr kw-args) (cdr keywords)
+                 (cons (make-Keyword (car keywords) (car kw-args) #f)
+                       kw-types))])))
+
 (define ((opt-convert-arr required-pos optional-pos) arr)
   (match arr
     [(arr: args result #f #f '())
@@ -167,4 +275,4 @@
          (make-PolyDots names (loop f))]
         [t t]))))
 
-(provide kw-convert opt-convert)
+(provide kw-convert kw-unconvert opt-convert)
diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt
index 6fe278b5..fc72932a 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt
@@ -165,6 +165,8 @@
   ;; Needed for bindings of types and TR primitives in expressions
   (except-in (base-env extra-procs prims base-types base-types-extra)
     define lambda λ)
+  ;; For tests that rely on kw/opt properties
+  (prefix-in tr: (only-in (base-env prims) define lambda λ))
   ;; Needed for constructing TR types in expected values
   (for-syntax
     (rep type-rep filter-rep object-rep)
@@ -1956,6 +1958,33 @@
              #:ret (ret (t:-> (t:Un (-Param -Symbol -Symbol) -Symbol) -Symbol))
              #:expected (ret (t:-> (t:Un (-Param -Symbol -Symbol) -Symbol) -Symbol))]
 
+       ;; test kw function without type annotation
+       [tc-e (let () (tr:define (f x #:y y) y) (f 'a #:y 'b)) Univ]
+       [tc-e (let () (tr:define (f x [a "a"] #:y y) y) (f 'a #:y 'b)) Univ]
+       [tc-e (let () (tr:define (f x #:y y . args) y) (f 'a 'b #:y 'c)) Univ]
+       [tc-e (let () (tr:define (f x [a "a"] #:y y . args) y) (f 'a 'b #:y 'c)) Univ]
+       [tc-e (let () (tr:define (f x #:y y #:z z) y) (f 'a #:y 'c #:z 'd)) Univ]
+       [tc-e (let () (tr:define (f x #:y [y "y"] #:z z) y)
+                     (f 'a #:y 'y #:z 'd) (f 'a #:z 'd)) Univ]
+       [tc-e (let () (tr:define (f x #:y [y "y"] #:z [z "z"]) y)
+                     (f 'a) (f 'a #:z 'd) (f 'a #:y 'y #:z 'd)) Univ]
+       [tc-e (let () (tr:define (f x #:y y #:z z) y) (f 'a #:y 'c #:z 'd)) Univ]
+       [tc-e (let () (tr:define (f x [a "a"] #:y y #:z z) y) (f 'a #:y 'c #:z 'd)) Univ]
+       [tc-e (let () (tr:define (f x #:y [y 'y]) y) (f "a" #:y "b")) Univ]
+       [tc-e (let () (tr:define (f x [a "a"] #:y [y 'y]) y) (f "a" #:y "b")) Univ]
+       [tc-e (let () (tr:define (f x #:y [y 'y] . args) y) (f "a" "b" #:y "b")) Univ]
+       [tc-e (let () (tr:define (f x [a "a"] #:y [y 'y] . args) y) (f "a" "b" #:y "b")) Univ]
+       ;; FIXME: these tests work in the REPL correctly, but not in the test harness
+       ;;        probably due to the reader type annotations
+       #|
+       [tc-e (let () (tr:define (f #{x : Symbol} #:y y) x) (f 'a #:y 'b)) -Symbol]
+       [tc-err (let () (tr:define (f #{x : Symbol} #:y y) y) (f "a" #:y 'b))
+               #:msg #rx"expected: Symbol.*given: String"]
+       |#
+       [tc-err (let () (tr:define (f x #:y y) (string-append x "foo")) (void))
+               #:msg #rx"expected: String.*given: Any"]
+       [tc-err (let () (tr:define (f x #:y y) y) (f "a"))
+               #:msg #rx"Required keyword not supplied"]
         )
   (test-suite
    "tc-literal tests"