code cleanup

tapl/ext-stlc.rkt

@@ -1,7 +1,5 @@
 #lang racket/base
-(require
-  #;(for-syntax racket/base syntax/parse syntax/stx racket/string "stx-utils.rkt")
-  "typecheck.rkt")
+(require "typecheck.rkt")
 (require (prefix-in stlc: (only-in "stlc+lit.rkt" #%app #%datum))
          (except-in "stlc+lit.rkt" #%app #%datum))
 (provide (rename-out [datum/tc #%datum]

tapl/stlc+box.rkt

@@ -1,9 +1,5 @@
 #lang racket/base
-(require
-  #;(for-syntax racket/base syntax/parse syntax/stx racket/syntax racket/string
-              "stx-utils.rkt" "typecheck.rkt")
-  #;(for-meta 2 racket/base syntax/parse racket/syntax)
-  "typecheck.rkt")
+(require "typecheck.rkt")
 (require (prefix-in stlc: (only-in "stlc+cons.rkt" #%app λ))
          (except-in "stlc+cons.rkt" #%app λ))
 (provide (rename-out [stlc:#%app #%app] [stlc:λ λ]))

tapl/stlc+cons.rkt

@@ -1,9 +1,5 @@
 #lang racket/base
-(require
-  #;(for-syntax racket/base syntax/parse syntax/stx racket/syntax racket/string
-              "stx-utils.rkt" "typecheck.rkt")
-  #;(for-meta 2 racket/base syntax/parse racket/syntax)
-  "typecheck.rkt")
+(require "typecheck.rkt")
 (require (prefix-in stlc: (only-in "stlc+var.rkt" #%app λ let begin))
          (except-in "stlc+var.rkt" #%app λ let begin))
 (provide (rename-out [stlc:#%app #%app] [stlc:λ λ] [stlc:let let] [stlc:begin begin]

tapl/stlc+lit.rkt

@@ -1,7 +1,5 @@
 #lang racket/base
-(require
-  #;(for-syntax racket/base syntax/parse)
-  "typecheck.rkt")
+(require "typecheck.rkt")
 (require "stlc.rkt")
 (provide (all-from-out "stlc.rkt"))
 (provide (rename-out [datum/tc #%datum]))

tapl/stlc+rec+sub.rkt

@@ -1,8 +1,6 @@
 #lang racket/base
-(require
-  #;(for-syntax racket/base syntax/parse racket/string syntax/stx racket/set "stx-utils.rkt")
-  "typecheck.rkt")
-;; want to use type=? from stlc+var.rkt
+(require "typecheck.rkt")
+;; want to use type=? from stlc+var.rkt, not stlc+sub.rkt
 (require (except-in "stlc+sub.rkt" #%app #%datum sub? type=?)
          (prefix-in stlc: (only-in "stlc+sub.rkt" #%app #%datum sub?))
          (except-in "stlc+var.rkt" #%app #%datum +)

tapl/stlc+sub.rkt

@@ -1,7 +1,5 @@
 #lang racket/base
-(require
-  #;(for-syntax racket/base syntax/parse racket/string "stx-utils.rkt")
-  "typecheck.rkt")
+(require "typecheck.rkt")
 (require (except-in "stlc+lit.rkt" #%datum + #%app)
          (prefix-in stlc: (only-in "stlc+lit.rkt" #%app #%datum)))
 (provide (rename-out #;[app/tc #%app] [stlc:#%app #%app] [datum/tc #%datum]))
@@ -41,10 +39,8 @@
 (begin-for-syntax
   (define (sub? τ1 τ2)
     (or ((current-type=?) τ1 τ2)
-        #;(and (identifier? τ2) (free-identifier=? τ2 #'Top))
         (syntax-parse (list τ1 τ2) #:literals (→ Nat Int Num Top)
           [(_ Top) #t]
-          #;[(t1:id t2:id) (free-identifier=? #'t1 #'t2)]
           [(Nat τ) ((current-sub?) #'Int #'τ)]
           [(Int τ) ((current-sub?) #'Num #'τ)]
           [(τ Num) ((current-sub?) #'τ #'Int)]
@@ -54,37 +50,5 @@
                 ((current-sub?) #'s2 #'t2))]
           [_ #f])))
   (define current-sub? (make-parameter sub?))
-  (current-typecheck-relation (current-sub?))
+  (current-typecheck-relation sub?)
   (define (subs? τs1 τs2) (stx-andmap (current-sub?) τs1 τs2)))
-
-#;(define-syntax (app/tc stx)
-  (syntax-parse stx
-    [(_ x ...)
-     #:with res
-     (parameterize ([current-type=? (current-sub?)])
-       (local-expand #'(stlc:#%app x ...) 'expression null))
-     #'res]))
-
-#;(define-syntax (app/tc stx)
-  (syntax-parse stx #:literals (→)
-    [(_ e_fn e_arg ...)
-     #:with (e_fn- τ_fn) (infer+erase #'e_fn)
-     #:fail-unless (→? #'τ_fn)
-                   (format "Type error: Attempting to apply a non-function ~a with type ~a\n"
-                           (syntax->datum #'e_fn) (syntax->datum #'τ_fn))
-     #:with (→ τ ... τ_res) #'τ_fn
-     #:with ((e_arg- τ_arg) ...) (infers+erase #'(e_arg ...))
-;     #:fail-unless (types=? #'(τ ...) #'(τ_arg ...))
-     #:fail-unless (subs? #'(τ_arg ...) #'(τ ...))
-                   (string-append
-                    (format
-                     "Wrong number of args given to function ~a, or args have wrong type:\ngiven: "
-                     (syntax->datum #'e_fn))
-                    (string-join
-                     (map (λ (e+τ) (format "~a : ~a" (car e+τ) (cadr e+τ))) (syntax->datum #'([e_arg τ_arg] ...)))
-                     ", ")
-                    "\nexpected arguments with type: "
-                    (string-join
-                     (map (λ (x) (format "~a" x)) (syntax->datum #'(τ ...)))
-                     ", "))
-     (⊢ #'(#%app e_fn- e_arg- ...) #'τ_res)]))

tapl/stlc+tup.rkt

@@ -1,7 +1,5 @@
 #lang racket/base
-(require
-  #;(for-syntax racket/base syntax/parse syntax/stx racket/string "stx-utils.rkt")
-  "typecheck.rkt")
+(require "typecheck.rkt")
 (require (prefix-in stlc: (only-in "ext-stlc.rkt" #%app))
          (except-in "ext-stlc.rkt" #%app))
 (provide (rename-out [stlc:#%app #%app])

tapl/stlc+var.rkt

@@ -1,9 +1,5 @@
 #lang racket/base
-(require
-  #;(for-syntax racket/base syntax/parse syntax/stx racket/syntax racket/string
-              "stx-utils.rkt" "typecheck.rkt")
-  #;(for-meta 2 racket/base syntax/parse racket/syntax)
-  "typecheck.rkt")
+(require "typecheck.rkt")
 (require (prefix-in stlc: (only-in "stlc+tup.rkt" #%app λ tup proj let type=?))
          (except-in "stlc+tup.rkt" #%app λ tup proj let type=?))
 (provide (rename-out [stlc:#%app #%app] [stlc:λ λ] [stlc:let let]))
@@ -31,29 +27,13 @@
 (begin-for-syntax
   ;; type=? : Type Type -> Boolean
   ;; Indicates whether two types are equal
-  ;; TODO: fix this code duplication, should call stlc:type=?
   (define (type=? τ1 τ2)
     (syntax-parse (list τ1 τ2)
       [(s1:str s2:str) (string=? (syntax-e #'s1) (syntax-e #'s2))]
-      [_ (stlc:type=? τ1 τ2)]
-      #;[(x:id y:id) (free-identifier=? τ1 τ2)]
-      #;[((τa ...) (τb ...)) (types=? #'(τa ...) #'(τb ...))]
-      #;[_ #f]))
+      [_ (stlc:type=? τ1 τ2)]))
 
   (current-type=? type=?)
-  (current-typecheck-relation (current-type=?))
-  ;; redefine these to use the new type=?
-  
-  ;; type equality = structurally recursive identifier equality
-  ;; uses the type=? in the context of τs1 instead of here
-  #;(define (types=? τs1 τs2)
-    (and (= (stx-length τs1) (stx-length τs2))
-         (stx-andmap type=? τs1 τs2)))
-  ;; uses the type=? in the context of τs instead of here
-  #;(define (same-types? τs)
-    (define τs-lst (syntax->list τs))
-    (or (null? τs-lst)
-        (andmap (λ (τ) (type=? (car τs-lst) τ)) (cdr τs-lst)))))
+  (current-typecheck-relation (current-type=?)))
 
 (provide define-type-alias)
 (define-syntax (define-type-alias stx)
@@ -108,7 +88,6 @@
      #:with (∨ (l_x τ_x) ...) #'τ_e
      #:fail-when (null? (syntax->list #'(l ...))) "no clauses"
      #:fail-unless (= (stx-length #'(l ...)) (stx-length #'(l_x ...))) "wrong number of case clauses"
-;     #:fail-unless (stx-andmap stx-str=? #'(l ...) #'(l_x ...)) "case clauses not exhaustive"
      #:fail-unless (typechecks? #'(l ...) #'(l_x ...)) "case clauses not exhaustive"
      #:with (((x-) e_l- τ_el) ...)
             (stx-map (λ (bs e) (infer/type-ctxt+erase bs e)) #'(([x : τ_x]) ...) #'(e_l ...))

tapl/stlc.rkt

@@ -1,7 +1,5 @@
 #lang racket/base
-(require
-  #;(for-syntax racket/base syntax/parse syntax/stx racket/string "stx-utils.rkt")
-  "typecheck.rkt")
+(require "typecheck.rkt")
 (provide (rename-out [λ/tc λ] [app/tc #%app]))
 (provide (for-syntax type=? types=? same-types? current-type=?))
 (provide #%module-begin #%top-interaction #%top require) ; from racket
@@ -21,8 +19,6 @@
   ;; Indicates whether two types are equal
   ;; structurally checks for free-identifier=?
   (define (type=? τ1 τ2)
-    ;(printf "~a\n" (syntax->datum τ1))
-    ;(printf "~a\n" (syntax-property τ1 'surface-type))
     (syntax-parse (list τ1 τ2)
       [(x:id y:id) (free-identifier=? τ1 τ2)]
       [((τa ...) (τb ...)) (types=? #'(τa ...) #'(τb ...))]
@@ -57,7 +53,6 @@
                            (syntax->datum #'e_fn) (syntax->datum #'τ_fn))
      #:with (→ τ ... τ_res) #'τ_fn
      #:with ((e_arg- τ_arg) ...) (infers+erase #'(e_arg ...))
-;     #:fail-unless ((eval-syntax (datum->syntax #'e_fn 'types=?)) #'(τ ...) #'(τ_arg ...))
      #:fail-unless (typechecks? #'(τ_arg ...) #'(τ ...))
                    (string-append
                     (format

tapl/sysf.rkt

@@ -1,10 +1,8 @@
 #lang racket/base
-(require
-  #;(for-syntax racket/base syntax/parse "stx-utils.rkt")
-  "typecheck.rkt")
-(require (except-in "stlc+lit.rkt" #%app type=?)
-         (prefix-in stlc: (only-in "stlc+lit.rkt" #%app type=?)))
-(provide (rename-out [stlc:#%app #%app]))
+(require "typecheck.rkt")
+(require (except-in "stlc+lit.rkt" #%app type=? λ)
+         (prefix-in stlc: (only-in "stlc+lit.rkt" #%app type=? λ)))
+(provide (rename-out [stlc:#%app #%app] [stlc:λ λ]))
 (provide (except-out (all-from-out "stlc+lit.rkt") stlc:#%app (for-syntax stlc:type=?)))
 (provide Λ inst)
 (provide (for-syntax type=?))
@@ -25,35 +23,17 @@
 (begin-for-syntax
   ;; type=? : Type Type -> Boolean
   ;; Indicates whether two types are equal
+  ;; Extend to handle ∀
   (define (type=? τ1 τ2)
-    ;(printf "t1 = ~a\n" (syntax->datum τ1))
-    ;(printf "t2 = ~a\n" (syntax->datum τ2))
     (syntax-parse (list τ1 τ2) #:literals (∀)
       [((∀ (x ...) t1) (∀ (y ...) t2))
        #:when (= (stx-length #'(x ...)) (stx-length #'(y ...)))
        #:with (z ...) (generate-temporaries #'(x ...))
-       (type=? (substs #'(z ...) #'(x ...) #'t1)
-               (substs #'(z ...) #'(y ...) #'t2))]
+       ((current-type=?) (substs #'(z ...) #'(x ...) #'t1)
+                         (substs #'(z ...) #'(y ...) #'t2))]
       [_ (stlc:type=? τ1 τ2)]))
   (current-type=? type=?)
-  (current-typecheck-relation (current-type=?))
-;      [(s1:str s2:str) (string=? (syntax-e #'s1) (syntax-e #'s2))]
-;      [(x:id y:id) (free-identifier=? τ1 τ2)]
-;      [((τa ...) (τb ...)) (types=? #'(τa ...) #'(τb ...))]
-;      [_ #f]))
-
-  ;; redefine these to use the new type=?
-  
-  ;; type equality = structurally recursive identifier equality
-  ;; uses the type=? in the context of τs1 instead of here
-  #;(define (types=? τs1 τs2)
-    (and (= (stx-length τs1) (stx-length τs2))
-         (stx-andmap type=? τs1 τs2)))
-  ;; uses the type=? in the context of τs instead of here
-  #;(define (same-types? τs)
-    (define τs-lst (syntax->list τs))
-    (or (null? τs-lst)
-        (andmap (λ (τ) (type=? (car τs-lst) τ)) (cdr τs-lst)))))
+  (current-typecheck-relation type=?))
 
 (define-syntax (Λ stx)
   (syntax-parse stx

tapl/typecheck.rkt

@@ -1,7 +1,6 @@
 #lang racket/base
 (require
-  (for-syntax racket syntax/parse racket/syntax syntax/stx "stx-utils.rkt")
-  #;(for-meta 2 racket/base syntax/parse racket/list syntax/stx "stx-utils.rkt"))
+  (for-syntax racket syntax/parse racket/syntax syntax/stx "stx-utils.rkt"))
 (provide 
  (for-syntax (all-defined-out))
  (all-defined-out)
@@ -50,7 +49,7 @@
     (pattern τ:expr))
   (define-syntax-class typed-binding #:datum-literals (:)
     (pattern [x:id : τ:type])
-    (pattern (~not [x:id : τ:type])
+    (pattern (~and any (~not [x:id : τ:type]))
      #:with x #f
      #:with τ #f
      #:fail-when #t
@@ -88,8 +87,9 @@
        #:with (e ...) es
        #:with
        ((~literal #%plain-lambda) xs+
-         (lr-stxs+vs1 stxs1 vs1 (lr-stxs+vs2 stxs2 vs2
-          ((~literal #%expression) e+) ...)))
+         ((~literal letrec-syntaxes+values) stxs1 ()
+           ((~literal letrec-syntaxes+values) stxs2 ()
+             ((~literal #%expression) e+) ...)))
        (expand/df
         #'(λ (x ...)
             (let-syntax ([x (make-rename-transformer (⊢ #'x #'τ))] ...)
@@ -113,32 +113,6 @@
   (define (typecheck? t1 t2) ((current-typecheck-relation) t1 t2))
   (define (typechecks? τs1 τs2)
     (stx-andmap (current-typecheck-relation) τs1 τs2))
- ; (define current-type=? (make-parameter #f))
- ; (define current-sub? (make-parameter #f))
-  
-;  ;; type equality = structurally recursive identifier equality
-;  (define (types=? τs1 τs2)
-;    (and (= (stx-length τs1) (stx-length τs2))
-;         (stx-andmap type=? τs1 τs2)))
-;  (define (same-types? τs)
-;    (define τs-lst (syntax->list τs))
-;    (or (null? τs-lst)
-;        (andmap (λ (τ) (type=? (car τs-lst) τ)) (cdr τs-lst))))
-;
-;  ;; type=? : Type Type -> Boolean
-;  ;; Indicates whether two types are equal
-;  (define (type=? τ1 τ2)
-;    (syntax-parse #`(#,τ1 #,τ2) #:datum-literals (∀)
-;      ;; TODO: should not have any datum literals
-;      [(x:id y:id) (free-identifier=? τ1 τ2)]
-;      [(s1:str s2:str) (string=? (syntax-e #'s1) (syntax-e #'s2))]
-;      [((∀ (x ...) t1) (∀ (y ...) t2))
-;       #:when (= (stx-length #'(x ...)) (stx-length #'(y ...)))
-;       #:with (z ...) (generate-temporaries #'(x ...))
-;       (type=? (substs #'(z ...) #'(x ...) #'t1)
-;               (substs #'(z ...) #'(y ...) #'t2))]
-;      [((τ1 ...) (τ2 ...)) (types=? #'(τ1 ...) #'(τ2 ...))]
-;      [_ #f]))
 
   ;; type expansion
   (define (eval-τ τ [tvs #'()])