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

Fix inner-expand bug, changed type error output

Browse Source 
* Fix inner-expand? issue which could prevent type-checking terms
  properly.
* No longer print out gamma and sigma when type checking fails
This commit is contained in:
William J. Bowman 2015-10-03 03:31:27 -04:00
parent ca9e36a973
commit 4cae9688fb
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
1 changed files with 4 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
curnel/redex-lang.rkt
View File

@ -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)