code cleanup

stlc.rkt

@@ -9,7 +9,7 @@
 (provide 
  (except-out
   (all-from-out racket/base) 
-  λ #%app + #%datum let #;letrec cons null null? begin void
+  λ #%app + #%datum let cons null null? begin void
   #%module-begin if define
   ))
 
@@ -126,13 +126,6 @@
      #:when (stx-andmap assert-Unit-type #'(e+ ...))
      (⊢ (syntax/loc stx (let ([x+ e_x+] ...) e+ ... e_result+)) (typeof #'e_result+))]))
 
-#;(define-syntax (letrec/tc stx)
-  (syntax-parse stx #:datum-literals (:)
-    [(_ ([f:id : τ_f e_f] ...) body ... body_result)
-     #:with (_ ([(f+) e_f+] ...) body+ ... body_result+)
-            (expand/df #'(letrec ([f e_f] ...) body ... body_result))
-    (syntax/loc stx (letrec ([f+ e_f+] ...) body+ ... body_result+))]))
-
 ; #%app
 (define-syntax (app/tc stx)
   (syntax-parse stx #:literals (→ void) 
@@ -189,9 +182,6 @@
 (define-syntax (define/tc stx)
   (syntax-parse stx #:datum-literals (:)
     [(_ (f:id [x:id : τ] ...) : τ_result e ...)
-;     #:with τ_result (generate-temporary #'f)
-;     #:when (fvs (set-add (fvs) (syntax->datum #'τ_result)))
-;     #:when (fv=>f (fv=>f-set #'τ_result #'f))
      #:when (Γ (type-env-extend #'([f (→ τ ... τ_result)])))
      #'(define f (λ/tc ([x : τ] ...) e ...))]
     [(_ x:id e) #'(define x e)]))
@@ -265,7 +255,7 @@
                            (letrec-values ([f v] ...) e ... (void)))))
         (define #,(datum->syntax stx 'runtime-env)
           (for/hash ([x:τ '#,(map (λ (xτ) (cons (car xτ) (syntax->datum (cdr xτ))))
-                                  (hash->list (Γ)))]);(do-subst (Γ))))])
+                                  (hash->list (Γ)))])
             (values (car x:τ) (cdr x:τ))))
         ))]))
 

sysf.rkt

@@ -98,9 +98,6 @@
     ;; is copied from stlc:define
     [(_ (f:id τs [x:id : τ] ...) : τ_result e ...)
      #:when (curly-parens? #'τs)
-;     #:with τ_result (generate-temporary #'f)
-;     #:when (fvs (set-add (fvs) (syntax->datum #'τ_result)))
-;     #:when (fv=>f (fv=>f-set #'τ_result #'f))
      #:when (Γ (type-env-extend #'([f (∀ τs (→ τ ... τ_result))])))
      #'(define f (λ/tc τs ([x : τ] ...) e ...))]
     [(_ any ...) #'(stlc:define any ...)]))

typecheck.rkt

@@ -17,22 +17,6 @@
 (define-for-syntax (type=? τ1 τ2)
 ;  (printf "type= ~a ~a\n" (syntax->datum τ1) (syntax->datum τ2))
   (syntax-parse #`(#,τ1 #,τ2)
-;    [(x:id τ)
-;     #:when (and (set-member? (fvs) (syntax->datum #'x))
-;                 (hash-has-key? (fvs-subst) (syntax->datum #'x)))
-;     (type=? (hash-ref (fvs-subst) (syntax->datum #'x)) #'τ)]
-;    [(x:id τ)
-;     #:when (set-member? (fvs) (syntax->datum #'x))
-;     #:when (fvs-subst (fvs-subst-set #'x #'τ))
-;     #t]
-;    [(τ x:id)
-;     #:when (and (set-member? (fvs) (syntax->datum #'x))
-;                 (hash-has-key? (fvs-subst) (syntax->datum #'x)))
-;     (type=? (hash-ref (fvs-subst) (syntax->datum #'x)) #'τ)]
-;    [(τ x:id)
-;     #:when (set-member? (fvs) (syntax->datum #'x))
-;     #:when (fvs-subst (fvs-subst-set #'x #'τ))
-;     #t]
     [(x:id y:id) (free-identifier=? τ1 τ2)]
     [((tycon1 τ1 ...) (tycon2 τ2 ...)) 
      (and (free-identifier=? #'tycon1 #'tycon2)
@@ -79,28 +63,7 @@
   (define-syntax (with-extended-type-env stx)
     (syntax-parse stx
       [(_ x-τs e)
-       #'(parameterize ([Γ (type-env-extend x-τs)]) e)]))
-
-  ;; generated type vars
-;  (define fvs (make-parameter (set)))
-;  (define fv=>f (make-parameter (hash)))
-;  (define (fv=>f-set fv f) (hash-set (fv=>f) (syntax->datum fv) f))
-;  (define fvs-subst (make-parameter (hash)))
-;  (define (fvs-subst-set x τ)
-;    (hash-set (fvs-subst) (syntax->datum x) τ))
-;  (define (do-subst/τ τ)
-;    (syntax-parse τ
-;      [x:id
-;       #:when (set-member? (fvs) (syntax->datum #'x))
-;       (hash-ref (fvs-subst) (syntax->datum #'x) #'???)]
-;      [τ:id #'τ]
-;      [(tycon τ ...)
-;       #:with (τ-subst ...) (stx-map do-subst/τ #'(τ ...))
-;       #'(tycon τ-subst ...)]))
-;  (define (do-subst h)
-;    (for/hash ([(x τ) (in-hash h)])
-;      (values x (do-subst/τ τ)))))
-)
+       #'(parameterize ([Γ (type-env-extend x-τs)]) e)])))
 
 ;; apply-forall ---------------------------------------------------------------
 (define-for-syntax (apply-forall ∀τ τs)
@@ -118,7 +81,6 @@
    ctx)
   (local-expand #`(#,id #,τs) 'expression (list #'#%app) ctx))
 
-
 ;; expand/df ------------------------------------------------------------------
 ;; depth-first expand
 (define-for-syntax (expand/df e [ctx #f])