commit caeda2ff0dc5f370a8a7203817384c8ff10a1bd5 parent ea5d41deb0bfdbd2379d1d2872d284a7dbaf0bf0 Author: Stephen Chang <stchang@ccs.neu.edu> Date: Fri, 15 Aug 2014 16:18:17 -0400 sysf: move apply-forall to typecheck.rkt Diffstat:
| M | sysf.rkt | | | 15 | --------------- |
1 file changed, 0 insertions(+), 15 deletions(-)
diff --git a/sysf.rkt b/sysf.rkt @@ -56,21 +56,6 @@ (⊢ (syntax/loc stx (lam xs e++ ... e_result++)) #'(∀ τs (→ τ ... τ_body)))] [(_ any ...) #'(stlc:λ any ...)])) -(define-for-syntax (apply-forall ∀τ τs) - (define ctx (syntax-local-make-definition-context)) - (define id (generate-temporary)) - (syntax-local-bind-syntaxes - (list id) - (syntax-parse ∀τ #:datum-literals (∀) - [(∀ (X ...) τbody) - #'(λ (stx) - (syntax-parse stx - [(_ (τ (... ...))) - #:with (X ...) #'(τ (... ...)) - #'τbody]))]) - ctx) - (local-expand #`(#,id #,τs) 'expression (list #'#%app) ctx)) - ; #%app ----------------------------------------------------------------------- (define-syntax (app/tc stx) (syntax-parse stx #:literals (→ void)