From 4cae9688fb86a7402920b78cf56e5842b115bf42 Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Sat, 3 Oct 2015 03:31:27 -0400 Subject: [PATCH] Fix inner-expand bug, changed type error output * Fix inner-expand? issue which could prevent type-checking terms properly. * No longer print out gamma and sigma when type checking fails --- curnel/redex-lang.rkt | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/curnel/redex-lang.rkt b/curnel/redex-lang.rkt index a0a46e2..8a89aba 100644 --- a/curnel/redex-lang.rkt +++ b/curnel/redex-lang.rkt @@ -153,7 +153,7 @@ (define reified-term ;; TODO: This results in less good error messages. Add an ;; algorithm to find the smallest ill-typed term. - (parameterize ([inner-expand? #f]) + (parameterize ([inner-expand? #t]) (let cur->datum ([syn syn]) (syntax-parse (core-expand syn) #:literals (term reduce #%app subst-all) @@ -178,12 +178,9 @@ (term (elim ,t1 ,t2)))] [(#%app e1 e2) (term (,(cur->datum #'e1) ,(cur->datum #'e2)))])))) - (unless (or inner-expand? (type-infer/term reified-term)) - ;; TODO: is this really a syntax error? - (raise-syntax-error 'cur "term is ill-typed:" - (begin (printf "Sigma: ~s~nGamma: ~s~n" (sigma) (gamma)) - reified-term) - syn)) + (unless (or (inner-expand?) (type-infer/term reified-term)) + #;(printf "Sigma: ~s~nGamma: ~s~n" (sigma) (gamma)) + (raise-syntax-error 'cur "term is ill-typed:" reified-term syn)) reified-term) (define (datum->cur syn t)