Improves error message for premise typos

This commit is contained in:
Casey Klein 2011-08-10 12:23:31 -05:00
parent a2dc2d9540
commit 4d1651645a
2 changed files with 16 additions and 7 deletions

View File

@ -1938,17 +1938,18 @@
(for/fold ([acc (foldl pat-pos acc-init conc-in)])
([prem (drop-ellipses #'prems)])
(syntax-case prem ()
[(form-name . _)
(judgment-form-id? #'form-name)
(let-values ([(prem-in prem-out) (split-body prem)])
(check-judgment-arity prem)
(for ([pos prem-in]) (tmpl-pos pos acc))
(foldl pat-pos acc prem-out))]
[(-where pat tmpl)
(where-keyword? #'-where)
(begin
(tmpl-pos #'tmpl acc)
(pat-pos #'pat acc))]
[(form-name . _)
(if (judgment-form-id? #'form-name)
(let-values ([(prem-in prem-out) (split-body prem)])
(check-judgment-arity prem)
(for ([pos prem-in]) (tmpl-pos pos acc))
(foldl pat-pos acc prem-out))
(raise-syntax-error syn-err-name "expected judgment form name" #'form-name))]
[_ (raise-syntax-error syn-err-name "malformed premise" prem)])))
(for ([pos conc-out]) (tmpl-pos pos acc-out))
acc-out)]))

View File

@ -59,13 +59,21 @@
#:contract (J n))])
bad-def)
(#rx"malformed premise"
([bad-prem (q)])
([bad-prem q])
(let ()
(define-judgment-form syn-err-lang
#:mode (J I)
[(J number)
bad-prem])
(void)))
(#rx"expected judgment form name"
([bad-judgment-form q])
(let ()
(define-judgment-form syn-err-lang
#:mode (J I)
[(J number)
(bad-judgment-form)])
(void)))
(#rx"different numbers of positions"
([bad-def (define-judgment-form syn-err-lang
#:mode (J I)