From 7b10648eb9fa9a7bf5d89b00bba2a8798a7c3e6d Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Sat, 9 Jan 2016 00:20:37 -0500 Subject: [PATCH] Added optional arg to type-infer/syn for local env Added undocumented feature to type-infer/syn. An optional argument can be used to locally extend gamma attempting to infer the type. --- curnel/redex-lang.rkt | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/curnel/redex-lang.rkt b/curnel/redex-lang.rkt index e782062..2999c26 100644 --- a/curnel/redex-lang.rkt +++ b/curnel/redex-lang.rkt @@ -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)))