add stlc+(iso)recursive types

tapl/README.md

@@ -9,6 +9,7 @@ A file extends its immediate parent file.
          - stlc+var.rkt
            - stlc+cons.rkt
              - stlc+box.rkt
+           - stlc+rec-iso.rkt
      - stlc+sub.rkt
        - stlc+rec+sub.rkt (also pull in tup from stlc+var.rkt)
      - sysf.rkt

tapl/ext-stlc.rkt

@@ -1,5 +1,8 @@
 #lang racket/base
 (require "typecheck.rkt")
+;; prefix-in an identifier if:
+;; - it will be extended, eg #%datum
+;; - want to use racket's version in this file, eg #%app
 (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/notes.txt

@@ -1,6 +1,15 @@
+2015-06-30
+when extending a typed language, use prefix-in for identifiers:
+- that are extended, eg #%datum in ext-stlc.rkt
+  - rename-out the extended implementation of the form
+- or when you want to use racket's version, eg #%app in ext-stlc.rkt
+  - rename-out the prefixed form
+- must except-out the prefixed forms, eg stlc:#%app and stlc:#%datum in ext-stlc
+
 2015-06-26
 Random thought: Can kinds be "erased"?
 - first thought is no, since they appear to be needed for type equality?
+- Solution: add them to body of lambda (eg which represents a forall)
 
 2015-06-26
 syntax marks problem: 

tapl/tests/rackunit-typechecking.rkt

@@ -11,7 +11,7 @@
      (format
       "Expression ~a [loc ~a:~a] has type ~a, expected ~a"
       (syntax->datum #'e) (syntax-line #'e) (syntax-column #'e)
-      (syntax->datum #'τ) (syntax->datum #'τ-expected))
+      (syntax->datum (get-orig #'τ)) (syntax->datum (get-orig #'τ-expected)))
      #'(void)]))
 
 (define-syntax (check-not-type stx)

tapl/tests/run-all-tests.rkt

@@ -7,6 +7,8 @@
 (require "stlc+cons-tests.rkt")
 (require "stlc+box-tests.rkt")
 
+(require "stlc+rec-iso-tests.rkt")
+
 (require "stlc+sub-tests.rkt")
 (require "stlc+rec+sub-tests.rkt")
 

tapl/typecheck.rkt

@@ -120,7 +120,8 @@
     (pattern stx
              #:when (stx-pair? #'stx)
              #:when (brace? #'stx)
-             #:with (τ) #'stx)))
+             #:with (τ:type) #'stx
+             #:with norm #'τ.norm)))
 
 (begin-for-syntax
   ;; ⊢ : Syntax Type -> Syntax
@@ -178,7 +179,6 @@
   
   (define current-type-eval (make-parameter #f))
 
-  (require inspect-syntax)
   ;; term expansion
   ;; expand/df : Syntax -> Syntax
   ;; Local expands the given syntax object. 
@@ -225,10 +225,11 @@
 (define-for-syntax (subst τ x e)
   (syntax-parse e
     [y:id #:when (bound-identifier=? e x) τ]
-    [y:id #'y]
     [(esub ...)
      #:with (esub_subst ...) (stx-map (λ (e1) (subst τ x e1)) #'(esub ...))
-     (syntax-track-origin #'(esub_subst ...) e x)]))
+     (syntax-track-origin #'(esub_subst ...) e x)]
+    [_ e]))
+
 
 (define-for-syntax (substs τs xs e)
   (stx-fold subst e τs xs))