code cleanup

tapl/fomega.rkt

@@ -26,13 +26,13 @@
 
 (begin-for-syntax
   ;; extend type-eval to handle tyapp
+  ;; - requires manually handling all other forms
   (define (type-eval τ)
-    (printf "eval: ~a\n" (syntax->datum τ))
+;    (printf "eval: ~a\n" (syntax->datum τ))
     (syntax-parse τ
       [((~literal #%plain-app) τ_fn τ_arg ...)
        #:with ((~literal #%plain-lambda) (tv ...) τ_body) ((current-type-eval) #'τ_fn)
        #:with (τ_arg+ ...) (stx-map (current-type-eval) #'(τ_arg ...))
-       #:when (printf "match\n")
        (substs #'(τ_arg+ ...) #'(tv ...) #'τ_body)]
       [((~literal ∀) _ ...) ((current-type-eval) (sysf:type-eval τ))]
       [((~literal →) _ ...) ((current-type-eval) (sysf:type-eval τ))]
@@ -47,23 +47,7 @@
        (syntax-track-origin #'(#%plain-app arg+ ...) τ #'#%plain-app)]
       [(τ ...) (stx-map (current-type-eval) #'(τ ...))]
       [_ (sysf:type-eval τ)]))
-  (current-type-eval type-eval)
-
-  ;; extend to handle tyapp
-;  (define (type=? τ1 τ2)
-;    (printf "(τ=) t1 = ~a\n" #;τ1 (syntax->datum τ1))
-;    (printf "(τ=) t2 = ~a\n" #;τ2 (syntax->datum τ2))
-;    (syntax-parse (list τ1 τ2)
-;      [(((~literal #%plain-app) ((~literal #%plain-lambda) (tv ...) τ_body) τ_arg ...) _)
-;       #:when (printf "match1\n")
-;       ((current-type=?) (substs  #'(τ_arg ...) #'(tv ...) #'τ_body) τ2)]
-;      [(_ ((~literal #%plain-app) ((~literal #%plain-lambda) (tv ...) τ_body) τ_arg ...))
-;       #:when (printf "match2\n")
-;       ((current-type=?) τ1 (substs  #'(τ_arg ...) #'(tv ...) #'τ_body))]
-;      [_ (sysf:type=? τ1 τ2)]))
-;  (current-type=? type=?)
-;  (current-typecheck-relation type=?))
-)
+  (current-type-eval type-eval))
 
 (define-base-type ★)
 (define-type-constructor ⇒)
@@ -110,13 +94,6 @@
      (⊢ #'e- (substs #'(τ.norm ...) #'(tv ...) #'τ_body))]))
 
 ;; TODO: merge with regular λ and app?
-#;(define-syntax (tyλ stx)
-  (syntax-parse stx
-    ; b = [tv : k]
-    [(_ (b:typed-binding ...) τ)
-     #:with ((tv- ...) τ- k) (infer/type-ctxt+erase #'(b ...) #'τ)
-     ; TODO: Racket lambda?
-     (⊢ #'(λ (tv- ...) τ-) #'(⇒ b.τ ... k))]))
 (define-syntax (tyλ stx)
   (syntax-parse stx 
     [(_ (b:typed-binding ...) τ)
@@ -124,10 +101,6 @@
      ;; b.τ's here are actually kinds
      (⊢ #'(λ tvs- τ-) #'(⇒ b.τ ... k))]))
 
-#;(define-syntax (tyapply stx)
-  (syntax-parse stx
-    [(_ ((~literal #%plain-lambda) (tv ...) τ_body) τ_arg ...)
-     (substs  #'(τ_arg ...) #'(tv ...) #'τ_body)]))
 (define-syntax (tyapp stx)
   (syntax-parse stx
     [(_ τ_fn τ_arg ...)
@@ -154,13 +127,6 @@
       ;; cant do type-subst here bc τ_fn might be a (forall) tyvar
       ;#:with τ_res ((current-type-eval) #'(tyapply τ_fn- τ_arg- ...))
      (⊢ #'(#%app τ_fn- τ_arg- ...) #'k_res)]))
-#;(define-syntax (tyapp stx)
-  (syntax-parse stx
-    [(_ τ_fn τ_arg ...)
-     #:with [τ_fn- ((~literal ⇒) k ... k_res)] (infer+erase #'τ_fn)
-     #:with ([τ_arg- k_arg] ...) (infers+erase #'(τ_arg ...))
-     #:when (typechecks? #'(k_arg ...) #'(k ...))
-     (⊢ #'(#%app τ_fn- τ_arg- ...) #'k_res)]))
 
 ;; must override #%app and λ and primops to use new →
 ;; TODO: parameterize →?

tapl/notes.txt

@@ -7,12 +7,12 @@ syntax marks problem:
 - in the type created by \Lambda, eg \x.(-> x x), the binding x and body x's
   were free-id= but not bound-id= because the body x's had extra marks
 - this is because (the syntax representing) types are marked going "into" an 
-  expansion, but do not receive the cancelling mark coming out of the
+  expansion, but do not receive the cancelling mark coming *out of* the
   expansion since they are attached as a syntax-property
 - thus, when this lam goes through another expansion (via \vdash), the binding x
   and body x's become neither free-id nor bound-id=?
 Solution: 
-- undo the mark (using syntax-local-introduce) before attaching a type 
+- undo the mark (using syntax-local-introduce) when retrieving the a type 
   as a syntax property (ie in \vdash)
 - need one more syntax-local-introduce in infer/tvs+erase
 - i guess the rule is I need as many syntax-local-introduce's as extra

tapl/stlc+sub.rkt

@@ -22,7 +22,7 @@
 (define-base-type Top)
 (define-base-type Num)
 (define-base-type Nat)
-;; TODO: implement define-subtype
+;; TODO: implement define-subtype, for now hardcode relations
 ;(define-subtype Int <: Num)
 ;(define-subtype Nat <: Int)
 

tapl/stlc+var.rkt

@@ -24,17 +24,8 @@
 ;; - sums (var)
 
 (begin-for-syntax
-  ;; type expansion
-  ;; extend to handle strings
-  #;(define (eval-τ τ . rst)
-    (syntax-parse τ
-      [s:str τ] ; record field
-      [_ (apply stlc:eval-τ τ rst)]))
-  #;(current-τ-eval eval-τ)
-  
   ; extend to:
-  ; 1) first eval types, to accomodate aliases
-  ; 2) accept strings (ie, record labels)
+  ; 1) accept strings (ie, record labels)
   (define (type=? τ1 τ2)
     (syntax-parse (list τ1 τ2)
       [(s1:str s2:str) (string=? (syntax-e #'s1) (syntax-e #'s2))]

tapl/stlc.rkt

@@ -13,38 +13,20 @@
 ;; - multi-arg app
 
 (begin-for-syntax
-  ;; type expansion
-  ;; - must structurally recur to check nested identifiers
-  ;; - rst allows adding extra args later
+  ;; type eval
+  ;; - for now, type-eval = full expansion
+  ;; - must expand because:
+  ;;   - checks for unbound identifiers (ie, undefined types)
   (define (type-eval τ) (expand/df τ))
-;  #;(define (eval-τ τ . rst)
-;    ; app is #%app in τ's ctxt, not here (which is racket's #%app)
-;    (define app (datum->syntax τ '#%app))
-;    ;; stop right before expanding:
-;    ;; - #%app, this should mean tycon via define-type-constructor
-;    ;; - app, other compound types, like variants
-;    ;;   - ow, the type checking in #%app will fail
-;    ;;   (could leave this case out until adding variants but it's general
-;    ;;    enough, so leave it here)
-;    ;; could match specific type constructors like → before expanding
-;    ;; but this is more general and wont require subsequent extensions for
-;    ;; every defined type constructor
-;    (syntax-parse (local-expand τ 'expression (list app #'#%app))
-;      ; full expansion checks for undefined types
-;      [x:id (local-expand #'x 'expression null)]
-;      [((~literal #%app) tcon t ...)
-;       #`(tcon #,@(stx-map (λ (ty) (apply (current-τ-eval) ty rst)) #'(t ...)))]
-;      ; else just structurually eval
-;      [(t ...) (stx-map (λ (ty) (apply (current-τ-eval) ty rst)) #'(t ...))]))
   (current-type-eval type-eval))
 
 (begin-for-syntax
   ;; type=? : Type Type -> Boolean
   ;; Indicates whether two types are equal
-  ;; type equality = structurally free-identifier=?
+  ;; type equality == structurally free-identifier=?
   (define (type=? τ1 τ2)
-    (printf "(τ=) t1 = ~a\n" #;τ1 (syntax->datum τ1))
-    (printf "(τ=) t2 = ~a\n" #;τ2 (syntax->datum τ2))
+;    (printf "(τ=) t1 = ~a\n" #;τ1 (syntax->datum τ1))
+;    (printf "(τ=) t2 = ~a\n" #;τ2 (syntax->datum τ2))
     (syntax-parse (list τ1 τ2)
       [(x:id y:id) (free-identifier=? τ1 τ2)]
       [((τa ...) (τb ...)) (types=? #'(τa ...) #'(τb ...))]
@@ -67,10 +49,6 @@
   (syntax-parse stx 
     [(_ (b:typed-binding ...) e)
      #:with (xs- e- τ_res) (infer/type-ctxt+erase #'(b ...) #'e)
-;     #:with (a as ...) #'(b.τ ...)
-;     #:when (printf "lam: ~a\n" (free-identifier=? #'a #'τ_res))
-;     #:with (lam (aa) resres) (local-expand #'(λ (a) τ_res) 'expression null)
-;     #:when (printf "lam2: ~a\n" (free-identifier=? #'aa #'resres))
      (⊢ #'(λ xs- e-) #'(→ b.τ ... τ_res))]))
 
 (define-syntax (app/tc stx)

tapl/sysf.rkt

@@ -28,16 +28,6 @@
      (syntax/loc stx (#%plain-lambda (x ...) body))]))
 
 (begin-for-syntax
-  ;; Extend to handle ∀, skip typevars
-;  #;(define (type-eval τ [tvs #'()] . rst)
-;    (syntax-parse τ
-;      [x:id #:when (stx-member τ tvs) τ]
-;      [((~literal ∀) ts t-body)
-;       #`(∀ ts #,(apply (current-τ-eval) #'t-body (stx-append tvs #'ts) rst))]
-;      ;; need to duplicate stlc:eval-τ here to pass extra params
-;      [_ (apply stlc:eval-τ τ tvs rst)]))
-;  #;(current-type-eval type-eval)
-
   ;; extend to handle ∀
   (define (type=? τ1 τ2)
     (syntax-parse (list τ1 τ2)
@@ -45,13 +35,6 @@
         ((~literal #%plain-lambda) (y:id ...) k2 ... t2))
        #:when (= (stx-length #'(x ...)) (stx-length #'(y ...)))
        #:with (z ...) (generate-temporaries #'(x ...))
-       ;#:when (typechecks? #'(k1 ...) #'(k2 ...))
-;       #:when (printf "t1 = ~a\n" (syntax->datum #'t1))
-;       #:when (printf "t2 = ~a\n" (syntax->datum #'t2))
-;       #:when (printf "~a\n"
-;                      (map syntax->datum
- ;                          (list (substs #'(z ...) #'(x ...) #'t1)
-;                            (substs #'(z ...) #'(y ...) #'t2))))
        ((current-type=?) (substs #'(z ...) #'(x ...) #'t1)
                          (substs #'(z ...) #'(y ...) #'t2))]
       [_ (stlc:type=? τ1 τ2)]))

tapl/tests/run-all-tests.rkt

@@ -10,5 +10,5 @@
 (require "stlc+sub-tests.rkt")
 (require "stlc+rec+sub-tests.rkt")
 
-;(require "sysf-tests.rkt")
-;(require "fomega-tests.rkt")
+(require "sysf-tests.rkt")
+(require "fomega-tests.rkt")

tapl/tests/stlc-tests.rkt

@@ -1,4 +1,4 @@
 #lang s-exp "../stlc.rkt"
 (require "rackunit-typechecking.rkt")
 
-;; cannot have tests without base types
+;; cannot write any terms without base types

tapl/typecheck.rkt

@@ -18,7 +18,7 @@
 ;; - A base type is just a Racket identifier, so type equality, even with
 ;;   aliasing, is just free-identifier=?
 
-;; Types are represented as (fully expanded, but not the same as racket fully expanded) syntax
+;; Types are represented as fully expanded syntax
 ;; - base types are identifiers
 ;; - type constructors are prefix
 
@@ -98,7 +98,6 @@
     (pattern stx:expr
      #:with norm ((current-type-eval) #'stx)
      #:with τ #'norm)) ; backwards compat
-;     #:with τ #'stx)) ; backwards compat
   (define-syntax-class typed-binding #:datum-literals (:)
     (pattern [x:id : stx:type] #:with τ #'stx.τ)
     (pattern (~and any (~not [x:id : τ:type]))
@@ -186,7 +185,7 @@
 
   (struct exn:fail:type:check exn:fail:user ())
 
-;; type-error #:src Syntax #:msg String Syntax ...
+  ;; type-error #:src Syntax #:msg String Syntax ...
   ;; usage:
   ;; type-error #:src src-stx
   ;;            #:msg msg-string msg-args ...
@@ -198,7 +197,6 @@
               (syntax->datum args) ...)
       (current-continuation-marks)))))
 
-
 (define-syntax (define-primop stx)
     (syntax-parse stx #:datum-literals (:)
       [(_ op:id : τ)
@@ -216,13 +214,10 @@
 (define-for-syntax (mk-pred x) (format-id x "~a?" x))
 (define-for-syntax (mk-acc base field) (format-id base "~a-~a" base field))
 
+; subst τ for y in e, if (bound-id=? x y)
 (define-for-syntax (subst τ x e)
   (syntax-parse e
-    [y:id
-;     #:when (printf "~a = ~a? = ~a\n" #'y x (free-identifier=? e x))
-;     #:when (printf "~a = ~a? = ~a\n" #'y x (bound-identifier=? e x))
-     #:when (bound-identifier=? e x)
-     τ]
+    [y:id #:when (bound-identifier=? e x) τ]
     [y:id #'y]
     [(esub ...)
      #:with (esub_subst ...) (stx-map (λ (e1) (subst τ x e1)) #'(esub ...))