commit d880b9d66810978854b050ba3c28415132f1658f
parent 893d457bad69f85ece8f4d30211dce65c7c13ec4
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Fri, 26 Feb 2016 16:54:12 -0500
clean up app err msgs; need to fix tests
Diffstat:
4 files changed, 56 insertions(+), 65 deletions(-)
diff --git a/tapl/mlish.rkt b/tapl/mlish.rkt
@@ -63,7 +63,6 @@
(define-syntax f (make-rename-transformer (⊢ g : (∀ (X ...) (ext-stlc:→ τ ... τ_out)))))
(define g (Λ (X ...) (ext-stlc:λ ([x : τ] ...) e_ann))))]
[(_ (f:id [x:id (~datum :) τ] ... (~datum →) τ_out) e)
- #:when (displayln #'f)
#:with Ys
(let L ([Xs #'()]) ; compute unbound ids; treat as tyvars
(with-handlers
@@ -75,12 +74,14 @@
(L (cons Y Xs)))])
((current-type-eval) #`(∀ #,Xs (ext-stlc:→ τ ... τ_out)))
Xs))
- #:when (displayln #'Ys)
- #:with g (generate-temporary #'f)
+ #:with g (add-orig (generate-temporary #'f) #'f)
#:with e_ann #'(add-expected e τ_out)
+ #:with (τ+orig ...) (stx-map (λ (t) (add-orig t t)) #'(τ ... τ_out))
#`(begin
(define-syntax f
- (make-rename-transformer (⊢ g : (∀ Ys (ext-stlc:→ τ ... τ_out)))))
+ (make-rename-transformer
+ ;(⊢ g : (∀ Ys (ext-stlc:→ τ ... τ_out)))))
+ (⊢ g : (∀ Ys (ext-stlc:→ τ+orig ...)))))
(define g
(Λ Ys (ext-stlc:λ ([x : τ] ...) e_ann))))])
;
@@ -92,7 +93,7 @@
[(_ Name:id . rst)
#:with Name2 (generate-temporary #'Name)
#`(begin
- (define-type (Name2) . #,(subst #'(Name2) #'Name #'rst))
+ (define-type (Name2) . #,(subst (add-orig #'(Name2) #'Name) #'Name #'rst))
(define-type-alias Name (Name2)))]
[(_ (Name:id X:id ...)
;; constructors must have the form (Cons τ ...)
@@ -153,19 +154,9 @@
#'(e_arg ...) #'(τ_in.norm (... ...)))
#:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in.norm (... ...)))
;; need to duplicate #%app err msg here, to attach additional props
- (string-append
- (format "~a (~a:~a) Arguments to constructor ~a have wrong type(s), "
- (syntax-source stx) (syntax-line stx) (syntax-column stx)
- 'Cons)
- "or wrong number of arguments:\nGiven:\n"
- (string-join
- (map (λ (e t) (format " ~a : ~a" e t)) ; indent each line
- (syntax->datum #'(e_arg ...))
- (stx-map type->str #'(τ_arg ...)))
- "\n" #:after-last "\n")
- (format "Expected: ~a arguments with type(s): "
- (stx-length #'(τ_in (... ...))))
- (string-join (stx-map type->str #'(τ_in (... ...))) ", "))
+ (mk-app-err-msg stx
+ #:expected #'(τ_in.norm (... ...)) #:given #'(τ_arg ...)
+ #:name (format "constructor ~a" 'Cons))
#:with τ_out (syntax-property
(syntax-property #'(Name τ_X (... ...)) 'constructor #'Cons)
'accessors
@@ -270,37 +261,15 @@
(syntax->datum #'e_fn) (type->str #'τ_fn))
#:with (~∀ (X ...) (~ext-stlc:→ τ_inX ... τ_outX)) #'τ_fn
#:fail-unless (stx-length=? #'(τ_inX ...) #'(e_arg ...)) ; check arity
- (string-append
- (format "~a (~a:~a) Wrong number of arguments given to function ~a.\n"
- (syntax-source stx) (syntax-line stx) (syntax-column stx)
- (syntax->datum #'e_fn))
- (format "Expected: ~a arguments with types: "
- (stx-length #'(τ_inX ...)))
- (string-join (stx-map type->str #'(τ_inX ...)) ", " #:after-last "\n")
- "Given:\n"
- (string-join
- (map (λ (e t) (format " ~a : ~a" e t)) ; indent each line
- (syntax->datum #'(e_arg ...))
- (stx-map type->str #'(τ_arg ...)))
- "\n"))
+ (mk-app-err-msg stx #:expected #'(τ_inX ...) #:given #'(τ_arg ...)
+ #:note "Wrong number of arguments.")
#:with cs (compute-constraints #'((τ_inX τ_arg) ...))
#:with (τ_solved ...) (filter (λ (x) x) (stx-map (λ (y) (lookup y #'cs)) #'(X ...)))
#:fail-unless (stx-length=? #'(X ...) #'(τ_solved ...))
- (format "could not instantiate polymorphic fn ~a" (syntax->datum #'e_fn))
+ (mk-app-err-msg stx #:expected #'(τ_inX ...) #:given #'(τ_arg ...)
+ #:note "Could not infer instantiation of polymorphic function.")
#:with (τ_in ... τ_out) (stx-map (λ (t) (substs #'(τ_solved ...) #'(X ...) t)) #'(τ_inX ... τ_outX))
; some code duplication
#:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
- (string-append
- (format "~a (~a:~a) Arguments to function ~a have wrong type(s).\n"
- (syntax-source stx) (syntax-line stx) (syntax-column stx)
- (syntax->datum #'e_fn))
- "Given:\n"
- (string-join
- (map (λ (e t) (format " ~a : ~a" e t)) ; indent each line
- (syntax->datum #'(e_arg ...))
- (stx-map type->str #'(τ_arg ...)))
- "\n" #:after-last "\n")
- (format "Expected: ~a arguments with type(s): "
- (stx-length #'(τ_in ...)))
- (string-join (stx-map type->str #'(τ_in ...)) ", "))
+ (mk-app-err-msg stx #:given #'(τ_arg ...) #:expected #'(τ_in ...))
(⊢ (#%app e_fn- e_arg- ...) : τ_out)])
diff --git a/tapl/stlc.rkt b/tapl/stlc.rkt
@@ -1,5 +1,6 @@
#lang s-exp "typecheck.rkt"
(provide (for-syntax current-type=? types=?))
+(provide (for-syntax mk-app-err-msg))
;; Simply-Typed Lambda Calculus
;; - no base types; can't write any terms
@@ -72,22 +73,34 @@
#:with (xs- e- τ_res) (infer/ctx+erase #'bvs #'e)
(⊢ (λ xs- e-) : (→ bvs.type ... τ_res))])
+(define-for-syntax (mk-app-err-msg stx #:expected [expected-τs #'()]
+ #:given [given-τs #'()]
+ #:note [note ""]
+ #:name [name #f])
+ (syntax-parse stx
+ [(_ e_fn e_arg ...)
+ (define fn-name
+ (if name name
+ (format "function ~a"
+ (syntax->datum (or (get-orig #'e_fn) #'e_fn)))))
+ (string-append
+ (format "~a (~a:~a):\nType error applying "
+ (syntax-source stx) (syntax-line stx) (syntax-column stx))
+ fn-name ". " note "\n"
+ (format " Expected: ~a argument(s) with type(s): " (stx-length expected-τs))
+ (string-join (stx-map type->str expected-τs) ", " #:after-last "\n")
+ " Given:\n"
+ (string-join
+ (map (λ (e t) (format " ~a : ~a" e t)) ; indent each line
+ (syntax->datum #'(e_arg ...))
+ (stx-map type->str given-τs))
+ "\n")
+ "\n")]))
+
(define-typed-syntax #%app
[(_ e_fn e_arg ...)
#:with [e_fn- (τ_in ... τ_out)] (⇑ e_fn as →)
#:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...))
#:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
- (string-append
- (format "~a (~a:~a) Arguments to function ~a have wrong type(s), "
- (syntax-source stx) (syntax-line stx) (syntax-column stx)
- (syntax->datum #'e_fn-))
- "or wrong number of arguments:\nGiven:\n"
- (string-join
- (map (λ (e t) (format " ~a : ~a" e t)) ; indent each line
- (syntax->datum #'(e_arg ...))
- (stx-map type->str #'(τ_arg ...)))
- "\n" #:after-last "\n")
- (format "Expected: ~a arguments with type(s): "
- (stx-length #'(τ_in ...)))
- (string-join (stx-map type->str #'(τ_in ...)) ", "))
+ (mk-app-err-msg stx #:expected #'(τ_in ...) #:given #'(τ_arg ...))
(⊢ (#%app e_fn- e_arg- ...) : τ_out)])
diff --git a/tapl/tests/mlish-tests.rkt b/tapl/tests/mlish-tests.rkt
@@ -6,6 +6,7 @@
;; tests more or less copied from infer-tests.rkt ------------------------------
;; top-level defines
(define (f [x : Int] → Int) x)
+(typecheck-fail (f 1 2) #:with-msg "Wrong number of arguments")
(check-type f : (→ Int Int))
(check-type (f 1) : Int ⇒ 1)
(typecheck-fail (f (λ ([x : Int]) x)))
@@ -26,7 +27,12 @@
(define (g2 [lst : (List X)] → (List X)) lst)
(check-type g2 : (→ (List X) (List X)))
-(typecheck-fail (g2 1) #:with-msg "Expected.+arguments with type.+(List X)")
+(typecheck-fail (g2 1)
+ #:with-msg
+ (string-append
+ "Could not infer instantiation of polymorphic function.*"
+ "Expected.+argument\\(s\\) with type\\(s\\).+\\(List X\\)"))
+
;(check-type (g2 (Nil {Int})) : (List Int) ⇒ (Nil {Int}))
;(check-type (g2 (Nil {Bool})) : (List Bool) ⇒ (Nil {Bool}))
;(check-type (g2 (Nil {(List Int)})) : (List (List Int)) ⇒ (Nil {(List Int)}))
@@ -75,6 +81,9 @@
[ConsI x xs -> 2]) : Int ⇒ 2)
(typecheck-fail (match 1 with [INil -> 1]))
+(typecheck-fail (ConsI #f INil)
+ #:with-msg "Type error applying constructor ConsI.*Expected.*Int, IntList")
+
;; annotated
(check-type (Nil {Int}) : (List Int))
(check-type (Cons {Int} 1 (Nil {Int})) : (List Int))
@@ -97,11 +106,11 @@
(typecheck-fail Nil #:with-msg "add annotations")
(typecheck-fail (Cons 1 (Nil {Bool}))
- #:with-msg "wrong type\\(s\\)")
+ #:with-msg "Type error applying constructor Cons.*Expected.*argument.*with type.*Int, \\(List Int\\)")
(typecheck-fail (Cons {Bool} 1 (Nil {Int}))
- #:with-msg "wrong type\\(s\\)")
+ #:with-msg "Type error applying constructor Cons.*Expected.*argument.*with type.*Bool, \\(List Bool\\)")
(typecheck-fail (Cons {Bool} 1 Nil)
- #:with-msg "wrong type\\(s\\)")
+ #:with-msg "Type error applying constructor Cons.*Expected.*argument.*with type.*Bool, \\(List Bool\\)")
(typecheck-fail (match Nil with [Cons x xs -> 2] [Nil -> 1])
#:with-msg "add annotations")
@@ -146,11 +155,11 @@
(typecheck-fail
((λ ([x : Unit]) x) 2)
#:with-msg
- "Arguments to function.+have wrong type.+Given:.+Int.+Expected:.+Unit")
+ "Type error applying function.*Expected.*argument.*with type.* Unit.*Given.*Int")
(typecheck-fail
((λ ([x : Unit]) x) void)
#:with-msg
- "Arguments to function.+have wrong type.+Given:.+(→ Unit).+Expected:.+Unit")
+ "Type error applying function.*Expected.*argument.*with type.* Unit.*Given.*\\(→ Unit\\)")
(check-type ((λ ([x : Unit]) x) (void)) : Unit)
diff --git a/tapl/tests/rackunit-typechecking.rkt b/tapl/tests/rackunit-typechecking.rkt
@@ -29,7 +29,7 @@
(define-syntax (typecheck-fail stx)
(syntax-parse stx #:datum-literals (:)
- [(_ e (~optional (~seq #:with-msg msg-pat:str) #:defaults ([msg-pat ""])))
+ [(_ e (~optional (~seq #:with-msg msg-pat) #:defaults ([msg-pat ""])))
#:when (check-exn
(λ (ex) (or (exn:fail? ex) (exn:test:check? ex)))
(λ ()
