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

Added optional arg to type-infer/syn for local env

Browse Source 
Added undocumented feature to type-infer/syn. An optional argument can
be used to locally extend gamma attempting to infer the type.
This commit is contained in:
William J. Bowman 2016-01-09 00:20:37 -05:00
parent 63bbb50752
commit 7b10648eb9
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
1 changed files with 7 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
curnel/redex-lang.rkt
View File

@ -246,9 +246,13 @@
(define (cur-equal? e1 e2)
(and (judgment-holds (equivalent ,(delta) ,(eval-cur e1) ,(eval-cur e2))) #t))
(define (type-infer/syn syn)
(let ([t (type-infer/term (eval-cur syn))])
(and t (datum->cur syn t))))
;; TODO: Document local-env
(define (type-infer/syn syn #:local-env [env '()])
(parameterize ([gamma (for/fold ([gamma (gamma)])
([(x t) (in-dict env)])
(extend-Γ/syn (thunk gamma) x t))])
(let ([t (type-infer/term (eval-cur syn))])
(and t (datum->cur syn t)))))
(define (type-check/syn? syn type)
(type-check/term? (eval-cur syn) (eval-cur type)))