suzanne.soy/macrotypes
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

factor out fail messages

Browse Source
This commit is contained in:
AlexKnauth 2016-06-22 09:55:11 -04:00
parent 11fb481f00
commit 961f32e6a2
7 changed files with 47 additions and 24 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
tapl/tests/tlb-mlish-tests.rkt
View File

@ -12,7 +12,7 @@
;; top-level defines
(define (f [x : Int] → Int) x)
(typecheck-fail (f 1 2) #:with-msg "Wrong number of arguments")
(typecheck-fail (f 1 2) #:with-msg "f: wrong number of arguments: expected 1, given 2")
(check-type f : (→ Int Int))
(check-type (f 1) : Int ⇒ 1)
(typecheck-fail (f (λ ([x : Int]) x)))
@ -32,7 +32,7 @@
(Cons X (List X)))
;; arity err
(typecheck-fail (Cons 1) #:with-msg "Cons: Wrong number of arguments")
(typecheck-fail (Cons 1) #:with-msg "Cons: wrong number of arguments: expected 2, given 1")
;; type err
(typecheck-fail (Cons 1 1)

37
tapl/typecheck.rkt
View File

@ -399,6 +399,41 @@
(define (expand/df e)
(local-expand e 'expression null))
;; typecheck-fail-msg/1 : Type Type Stx -> String
(define (typecheck-fail-msg/1 τ_expected τ_given expression)
(format "type mismatch: expected ~a, given ~a\n expression: ~s"
(type->str τ_expected)
(type->str τ_given)
(syntax->datum (get-orig expression))))
;; typecheck-fail-msg/1/no-expr : Type Type Stx -> String
(define (typecheck-fail-msg/1/no-expr τ_expected τ_given)
(format "type mismatch: expected ~a, given ~a"
(type->str τ_expected)
(type->str τ_given)))
;; typecheck-fail-msg/multi/no-exprs : (Stx-Listof Type) (Stx-Listof Type) -> String
(define (typecheck-fail-msg/multi/no-exprs τs_expected τs_given)
(format (string-append "type mismatch\n"
" expected: ~a\n"
" given: ~a")
(string-join (stx-map type->str τs_expected) ", ")
(string-join (stx-map type->str τs_given) ", ")))
;; no-expected-type-fail-msg : -> String
(define (no-expected-type-fail-msg)
"no expected type, add annotations")
;; num-args-fail-msg : Stx (Stx-Listof Type) (Stx-Listof Stx) -> String
(define (num-args-fail-msg fn τs_expected arguments)
(format (string-append "~s: wrong number of arguments: expected ~a, given ~a\n"
" expected: ~a\n"
" arguments: ~a")
(syntax->datum (get-orig fn))
(stx-length τs_expected) (stx-length arguments)
(string-join (stx-map type->str τs_expected) ", ")
(string-join (map ~s (map syntax->datum (stx-map get-orig arguments))) ", ")))
(struct exn:fail:type:check exn:fail:user ())
(struct exn:fail:type:infer exn:fail:user ())
@ -434,7 +469,7 @@
[(stx-pair? τ) (string-join (stx-map type->str τ)
#:before-first "("
#:after-last ")")]
[else (format "~a" (syntax->datum τ))])))
[else (format "~s" (syntax->datum τ))])))
(begin-for-syntax
(define (mk-? id) (format-id id "~a?" id))

3
tapl/typed-lang-builder/fomega.rkt
View File

@ -110,8 +110,7 @@
[(tyapp τ_fn τ_arg ...) ▶
[⊢ [[τ_fn ≫ τ_fn-] ⇒ : (~⇒ k_in ... k_out)]]
[#:fail-unless (stx-length=? #'[k_in ...] #'[τ_arg ...])
(format "wrong number of arguments: expected ~a, given ~a"
(stx-length #'[k_in ...]) (stx-length #'[τ_arg ...]))]
(num-args-fail-msg #'τ_fn #'[k_in ...] #'[τ_arg ...])]
[⊢ [[τ_arg ≫ τ_arg-] ⇐ : k_in] ...]
--------
[⊢ [[_ ≫ (#%app- τ_fn- τ_arg- ...)] ⇒ : k_out]]])

2
tapl/typed-lang-builder/mlish-core.rkt
View File

@ -865,7 +865,7 @@
[#:with (unsolved-X ...) (find-free-Xs #'Xs* #'τ_out)]
;; arity check
[#:fail-unless (stx-length=? #'(τ_in ...) #'e_args)
(format "~s: Wrong number of arguments." (syntax->datum (get-orig #'e_fn)))]
(num-args-fail-msg #'e_fn #'[τ_in ...] #'e_args)]
;; compute argument types
[#:with (τ_arg ...) (stx-map typeof #'(e_arg- ...))]
;; typecheck args

3
tapl/typed-lang-builder/stlc+effect.rkt
View File

@ -66,8 +66,7 @@
(⇒ := (~locs fas ...))
(⇒ ! (~locs fds ...))]]
[#:fail-unless (stx-length=? #'[e ...] #'[τ_in ...])
(format "wrong number of arguments: expected ~a, given ~a"
(stx-length #'[τ_in ...] #'[e ...]))]
(num-args-fail-msg #'efn #'[τ_in ...] #'[e ...])]
[⊢ [[e ≫ e_arg-]
(⇐ : τ_in)
(⇒ ν (~locs ns ...))

3
tapl/typed-lang-builder/stlc.rkt
View File

@ -41,8 +41,7 @@
[(_ e_fn e_arg ...) ▶
[⊢ [[e_fn ≫ e_fn-] ⇒ : (~→ τ_in ... τ_out)]]
[#:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])
(format "wrong number of arguments: expected ~a, given ~a"
(stx-length #'[τ_in ...]) (stx-length #'[e_arg ...]))]
(num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])]
[⊢ [[e_arg ≫ e_arg-] ⇐ : τ_in] ...]
--------
[⊢ [[_ ≫ (#%app- e_fn- e_arg- ...)] ⇒ : τ_out]]])

19
tapl/typed-lang-builder/typed-lang-builder.rkt
View File

@ -59,10 +59,7 @@
(~post
(~fail #:when (and (not (typecheck? #'τ-tmp #'τ-exp))
(get-orig #'e-tmp))
(format "type mismatch: expected ~a, given ~a\n expression: ~s"
(type->str #'τ-exp)
(type->str #'τ-tmp)
(syntax->datum (get-orig #'e-tmp)))))
(typecheck-fail-msg/1 #'τ-exp #'τ-tmp #'e-tmp)))
(get-orig #'e-tmp)))])
(define-splicing-syntax-class ⇒-props
#:attributes (e-pat)
@ -147,18 +144,12 @@
#:with [pat ...]
#'[(~post
(~fail #:unless (typecheck? #'a #'b)
(format "type mismatch: expected ~a, given ~a"
(type->str #'b)
(type->str #'a))))]]
(typecheck-fail-msg/1/no-expr #'b #'a)))]]
[pattern (~seq [a τ⊑ b] ooo:elipsis)
#:with [pat ...]
#'[(~post
(~fail #:unless (typechecks? #'[a ooo] #'[b ooo])
(format (string-append "type mismatch\n"
" expected: ~a\n"
" given: ~a")
(string-join (stx-map type->str #'[b ooo]) ", ")
(string-join (stx-map type->str #'[a ooo]) ", "))))]]
(typecheck-fail-msg/multi/no-exprs #'[b ooo] #'[a ooo])))]]
[pattern [#:when condition:expr]
#:with [pat ...]
#'[(~fail #:unless condition)]]
@ -189,7 +180,7 @@
pat*
(~parse τ (get-expected-type #'stx))
(~post (~post (~fail #:unless (syntax-e #'τ)
"no expected type, add annotations")))
(no-expected-type-fail-msg))))
(~parse τ-pat #'τ))
#:with [stuff ...] #'[]
#:with body:expr
@ -216,7 +207,7 @@
pat*
(~parse τ (get-expected-type #'stx))
(~post (~post (~fail #:unless (syntax-e #'τ)
"no expected type, add annotations")))
(no-expected-type-fail-msg))))
(~parse τ-pat #'τ))
#:attr transform-body
(lambda (body)