From caeda2ff0dc5f370a8a7203817384c8ff10a1bd5 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Fri, 15 Aug 2014 16:18:17 -0400 Subject: [PATCH] sysf: move apply-forall to typecheck.rkt --- sysf.rkt | 15 --------------- 1 file changed, 15 deletions(-) diff --git a/sysf.rkt b/sysf.rkt index 4d221e4..a68067c 100644 --- 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)