revise extra-info to handle mutually recursive datatypes

- define extra-info as a separate macro whose input is the types in the tycon - extra-info in main tycon is just the name of the extra-info macro - extra-info macro is expanded only when extra-info is requested - naturally handles additional tyvar substs in the types - breaks the recursion to avoid inf loops for recursive and mutually recursive datatypes - enables simplification of direct recursive datatypes - no longer need subst-special - performance is much improved (okasaki: ~1min, was ~4min)
2016-04-13 14:00:20 -04:00 · 2016-04-13 14:00:20 -04:00 · 8a36c7962b
commit 8a36c7962b
parent 5c3d0edb5e
12 changed files with 245 additions and 152 deletions
--- a/tapl/mlish.rkt
+++ b/tapl/mlish.rkt
@ -11,7 +11,6 @@
 (require (only-in "sysf.rkt" ~∀ ∀ ∀? Λ))
 (reuse × tup proj define-type-alias #:from "stlc+rec-iso.rkt")
 (require (only-in "stlc+rec-iso.rkt" ~× ×?))
-(provide → define-type)
 (provide (rename-out [ext-stlc:and and] [ext-stlc:#%datum #%datum]))
 (reuse member length reverse list-ref cons nil isnil head tail list #:from "stlc+cons.rkt")
 (require (prefix-in stlc+cons: (only-in "stlc+cons.rkt" list cons nil)))
@ -25,13 +24,15 @@
 (require (prefix-in stlc+cons: (only-in "stlc+cons.rkt" list)))
 (require (prefix-in stlc+tup: (only-in "stlc+tup.rkt" tup)))

+(provide → →/test match2 define-type)
+
 ;; ML-like language
 ;; - top level recursive functions
 ;; - user-definable algebraic datatypes
 ;; - pattern matching
 ;; - (local) type inference

-;; type inference constraint solving
+  ;; type inference constraint solving
 (begin-for-syntax 
  (define (compute-constraint τ1-τ2)
    (syntax-parse τ1-τ2
@ -193,11 +194,9 @@
         (⊢ g : ty_fn_expected #;(∀ Ys (ext-stlc:→ τ+orig ...)))))
      (define g
        (Λ Ys (ext-stlc:λ ([x : τ] ...) (ext-stlc:begin e_body ... e_ann)))))])
-;
-;; internal form used to expand many types at once under the same context
-(define-type-constructor Tmp #:arity >= 0 #:bvs >= 0) ; need a >= 0 arity

-;; define-type --------------------------------------------------
+;; define-type -----------------------------------------------
+;; TODO: should validate τ as part of define-type definition (before it's ever used)
 (define-syntax (define-type stx)
  (syntax-parse stx
    [(_ Name:id . rst)
@ -217,6 +216,10 @@
                         (~parse (fld ...) (generate-temporaries #'(τ ...)))))) ...)
     #:with RecName (generate-temporary #'Name)
     #:with NameExpander (format-id #'Name "~~~a" #'Name)
+     #:with NameExtraInfo (format-id #'Name "~a-extra-info" #'Name)
+     #:with NameDelayed (format-id #'Name "~a-delayed" #'Name)
+     #:with NameForced (format-id #'NameDelayed "~a-force" #'NameDelayed)
+     #:with NameForcedExpander (format-id #'NameForced "~~~a" #'NameForced)
     #:with (StructName ...) (generate-temporaries #'(Cons ...))
     #:with ((e_arg ...) ...) (stx-map generate-temporaries #'((τ ...) ...))
     #:with ((e_arg- ...) ...) (stx-map generate-temporaries #'((τ ...) ...))
@ -224,11 +227,25 @@
     #:with ((acc ...) ...) (stx-map (λ (S fs) (stx-map (λ (f) (format-id S "~a-~a" S f)) fs))
                                     #'(StructName ...) #'((fld ...) ...))
     #:with (Cons? ...) (stx-map mk-? #'(StructName ...))
+     #:with (Y ...) (generate-temporaries #'(X ...))
     ;; types, but using RecName instead of Name
     #:with ((τ/rec ...) ...) (subst #'RecName #'Name #'((τ ...) ...))
-     #:with (Y ...) (generate-temporaries #'(X ...))
     #`(begin
+;         (define NameDelayed (lambda () (error "types not allowed at runtime")))
+         ; TODO: use define-type-constructor for delayed form as well,
+         ;; to get proper pattern expanders, etc
+         ;; (define-syntax (Name stx) 
+         ;;   (syntax-parse stx
+         ;;     [(_ Y ...) (add-orig (mk-type #'(delay NameDelayed Y ...)) stx)]))
+         (define-syntax (NameExtraInfo stx)
+           (syntax-parse stx
+             [(_ X ...) #'(('Cons 'StructName Cons? [acc τ] ...) ...)]))
         (define-type-constructor Name
+           #:arity = #,(stx-length #'(X ...))
+           #:extra-info 'NameExtraInfo
+;           #:extra-info (X ...) (('Cons 'StructName Cons? [acc τ] ...) ...)
+           #:no-provide)
+         #;(define-type-constructor Name
           #:arity = #,(stx-length #'(X ...))
           #:extra-info (X ...) 
             (λ (RecName) 
@ -263,6 +280,7 @@
              #:with τ-expected (syntax-property #'C 'expected-type)
              #:fail-unless (syntax-e #'τ-expected)
                            (type-error #:src stx #:msg "cannot infer type of ~a; add annotations" #'C)
+;              #:with (_ (~datum delay) (_ () _ τ-expected-arg (... ...))) ((current-type-eval) #'τ-expected)
              #:with (NameExpander τ-expected-arg (... ...)) ((current-type-eval) #'τ-expected)
              #'(C {τ-expected-arg (... ...)})]
             [_:id 
@ -316,12 +334,12 @@
        [{(~datum _)} #'()]
        [{(~literal stlc+cons:nil)}  #'()]
        [{A:id} ; disambiguate 0-arity constructors (that don't need parens)
-         #:with ((~literal #%plain-lambda) (RecName) 
-                 ((~literal let-values) ()
-                  ((~literal let-values) ()
-                   . info-body)))
-                 (get-extra-info #'ty)
-                #'()]
+         ;; #:with ((~literal #%plain-lambda) (RecName) 
+         ;;         ((~literal let-values) ()
+         ;;          ((~literal let-values) ()
+         ;;           . info-body)))
+         #:when (get-extra-info #'ty)
+         #'()]
        ;; comma tup syntax always has parens
 ;        [{(~and ps (p1 ((~literal unquote) p2) ((~literal unquote) p) ...))}
        [{(~and ps (p1 (unq p) ...))}
@ -333,10 +351,11 @@
      [((~datum _) ty) #'()]
      [((~or (~literal stlc+cons:nil)) ty) #'()]
      [(A:id ty) ; disambiguate 0-arity constructors (that don't need parens)
-       #:with ((~literal #%plain-lambda) (RecName) 
-               ((~literal let-values) ()
-                ((~literal let-values) ()
-                 . (((~literal #%plain-app) ((~literal quote) C) . rst) ...))))
+       #:with (_ (_ ((~literal quote) C) . _) ...)
+       ;; ((~literal #%plain-lambda) (RecName) 
+       ;;         ((~literal let-values) ()
+       ;;          ((~literal let-values) ()
+       ;;           . (((~literal #%plain-app) ((~literal quote) C) . rst) ...))))
              (get-extra-info #'ty)
       #:when (member (syntax->datum #'A) (syntax->datum #'(C ...)))
       #'()]
@ -360,19 +379,19 @@
       #:with (~List t) #'ty
       (unifys #'([p t] [ps ty]))]
      [((Name p ...) ty)
-        #:with ((~literal #%plain-lambda) (RecName) 
-                ((~literal let-values) ()
-                 ((~literal let-values) ()
-                  . info-body)))
-               (get-extra-info #'ty)
-        #:with ((_ ((~literal quote) ConsAll) . _) ...) #'info-body
-        #:with info-unfolded (subst-special #'τ_e #'RecName #'info-body)
+        ;; #:with ((~literal #%plain-lambda) (RecName) 
+        ;;         ((~literal let-values) ()
+        ;;          ((~literal let-values) ()
+        ;;           . info-body)))
+       ;; (get-extra-info #'ty)
+;        #:with (_ (_ ((~literal quote) ConsAll) . _) ...) (get-extra-info #'ty)
+;        #:with info-unfolded (subst-special #'τ_e #'RecName #'info-body)
        #:with (_ ((~literal quote) Cons) ((~literal quote) StructName) Cons? [_ acc τ] ...)
               (stx-findf
-                   (syntax-parser
-                     [((~literal #%plain-app) 'C . rst)
-                      (equal? (syntax->datum #'Name) (syntax->datum #'C))])
-                 #'info-unfolded)
+                 (syntax-parser
+                  [(_ 'C . rst) 
+                   (equal? (syntax->datum #'Name) (syntax->datum #'C))])
+                 (stx-cdr (get-extra-info #'ty)))
        (unifys #'([p τ] ...))]
      [p+t #:fail-when #t (format "could not unify ~a" (syntax->datum #'p+t)) #'()]))
  (define (unifys p+tys) (stx-appendmap unify-pat+ty p+tys))
@ -384,12 +403,12 @@
        [{(~datum _)} #'_]
        [{(~literal stlc+cons:nil)}  (syntax/loc p (list))]
        [{A:id} ; disambiguate 0-arity constructors (that don't need parens)
-         #:with ((~literal #%plain-lambda) (RecName) 
-                 ((~literal let-values) ()
-                  ((~literal let-values) ()
-                   . info-body)))
-                 (get-extra-info ty)
-                (compile-pat #'(A) ty)]
+         ;; #:with ((~literal #%plain-lambda) (RecName) 
+         ;;         ((~literal let-values) ()
+         ;;          ((~literal let-values) ()
+         ;;           . info-body)))
+         #:when (get-extra-info ty)
+         (compile-pat #'(A) ty)]
        ;; comma tup stx always has parens
        ;; comma tup syntax always has parens
 ;        [{(~and ps (p1 ((~literal unquote) p2) ((~literal unquote) p) ...))}
@ -402,11 +421,11 @@
     [(~literal stlc+cons:nil) ; nil
      #'(list)]
     [A:id ; disambiguate 0-arity constructors (that don't need parens)
-      #:with ((~literal #%plain-lambda) (RecName) 
-              ((~literal let-values) ()
-               ((~literal let-values) ()
-                . (((~literal #%plain-app) ((~literal quote) C) . rst) ...))))
-              (get-extra-info ty)
+      ;; #:with ((~literal #%plain-lambda) (RecName) 
+      ;;         ((~literal let-values) ()
+      ;;          ((~literal let-values) ()
+      ;;           . (((~literal #%plain-app) ((~literal quote) C) . rst) ...))))
+       #:with (_ (_ ((~literal quote) C) . _) ...) (get-extra-info ty)
       #:when (member (syntax->datum #'A) (syntax->datum #'(C ...)))
      (compile-pat #'(A) ty)]
     [x:id p]
@ -435,19 +454,19 @@
      #:with ps- (compile-pat #'ps ty)
      #'(cons p- ps-)]
     [(Name . pats)
-      #:with ((~literal #%plain-lambda) (RecName) 
-              ((~literal let-values) ()
-               ((~literal let-values) ()
-                . info-body)))
-             (get-extra-info ty)
-      #:with ((_ ((~literal quote) ConsAll) . _) ...) #'info-body
-      #:with info-unfolded (subst-special #'τ_e #'RecName #'info-body)
+      ;; #:with ((~literal #%plain-lambda) (RecName) 
+      ;;         ((~literal let-values) ()
+      ;;          ((~literal let-values) ()
+      ;;           . info-body)))
+      ;;        (get-extra-info ty)
+      ;; #:with ((_ ((~literal quote) ConsAll) . _) ...) #'info-body
+      ;; #:with info-unfolded (subst-special #'τ_e #'RecName #'info-body)
      #:with (_ ((~literal quote) Cons) ((~literal quote) StructName) Cons? [_ acc τ] ...)
             (stx-findf
-                 (syntax-parser
-                   [((~literal #%plain-app) 'C . rst)
-                    (equal? (syntax->datum #'Name) (syntax->datum #'C))])
-               #'info-unfolded)
+               (syntax-parser
+                [(_ 'C . rst) 
+                 (equal? (syntax->datum #'Name) (syntax->datum #'C))])
+               (stx-cdr (get-extra-info ty)))
      #:with (p- ...) (stx-map compile-pat #'pats #'(τ ...))
      (syntax/loc p (StructName p- ...))]))

@ -494,13 +513,14 @@
                   (syntax->list #'((p ...) ...)))])])]
     [else ; algebraic datatypes
      (syntax-parse (get-extra-info ty)
-        [((~literal #%plain-lambda) (RecName) 
+        [#;((~literal #%plain-lambda) (RecName) 
           ((~literal let-values) ()
             ((~literal let-values) ()
              . (((~literal #%plain-app)  
                  ((~literal quote) C) 
                  ((~literal quote) Cstruct)
                  . rst) ...))))
+         (_ (_ ((~literal quote) C) ((~literal quote) Cstruct) . rst) ...)
         (syntax-parse pats
           [((Cpat _ ...) ...)
            (define Cs (syntax->datum #'(C ...)))
@ -522,7 +542,6 @@
    (stx-map (lambda (p) (list (get-ctx p ty) (compile-pat p ty))) pats))
  )

-(provide match2)
 (define-syntax (match2 stx)
 (syntax-parse stx #:datum-literals (with)
   [(_ e with . clauses)
@ -530,11 +549,16 @@
    #:with [e- τ_e] (infer+erase #'e)
    (syntax-parse #'clauses #:datum-literals (->)
     [([(~seq p ...) -> e_body] ...)
-      #:with (pat ...) (stx-map (lambda (ps) (syntax-parse ps [(pp ...) (syntax/loc stx {pp ...})]))
-                            #'((p ...) ...)) ; use brace to indicate root pattern
+      #:with (pat ...) (stx-map ; use brace to indicate root pattern
+                         (lambda (ps) (syntax-parse ps [(pp ...) (syntax/loc stx {pp ...})]))
+                         #'((p ...) ...)) 
      #:with ([(~and ctx ([x ty] ...)) pat-] ...) (compile-pats #'(pat ...) #'τ_e)
      ;; #:with ((~and ctx ([x ty] ...)) ...) (stx-map (lambda (p) (get-ctx p #'τ_e)) #'(pat ...))
-      #:with ([(x- ...) e_body- ty_body] ...) (stx-map infer/ctx+erase #'(ctx ...) #'(e_body ...))
+      #:with ty-expected (get-expected-type stx)
+      #:with ([(x- ...) e_body- ty_body] ...) 
+             (stx-map 
+               infer/ctx+erase 
+               #'(ctx ...) #'((add-expected e_body ty-expected) ...))
      ;; #:with (pat- ...) (stx-map (lambda (p) (compile-pat p #'τ_e)) #'(pat ...))
      #:fail-unless (same-types? #'(ty_body ...))
                    (string-append "branches have different types, given: "
@ -602,13 +626,15 @@
             (~optional (~seq #:when e_guard) #:defaults ([e_guard #'(ext-stlc:#%datum . #t)]))
             -> e_c_un] ...) ; un = unannotated with expected ty
        ;; len #'clauses maybe > len #'info, due to guards
-        #:with ((~literal #%plain-lambda) (RecName) 
-                ((~literal let-values) ()
-                 ((~literal let-values) ()
-                  . info-body)))
-               (get-extra-info #'τ_e)
-        #:with info-unfolded (subst-special #'τ_e #'RecName #'info-body)
-        #:with ((_ ((~literal quote) ConsAll) . _) ...) #'info-body
+        ;; #:with ((~literal #%plain-lambda) (RecName) 
+        ;;         ((~literal let-values) ()
+        ;;          ((~literal let-values) ()
+        ;;           . info-body)))
+        ;;        (get-extra-info #'τ_e)
+        ;; #:with info-unfolded (subst-special #'τ_e #'RecName #'info-body)
+        #:with info-body (get-extra-info #'τ_e)
+        #:with info-unfolded #'info-body
+        #:with (_ (_ ((~literal quote) ConsAll) . _) ...) #'info-body
        #:fail-unless (set=? (syntax->datum #'(Clause ...))
                             (syntax->datum #'(ConsAll ...)))
                      (type-error #:src stx
@ -627,7 +653,7 @@
                      (syntax-parser
                        [((~literal #%plain-app) 'C . rst)
                         (equal? Cl (syntax->datum #'C))])
-                    #'info-unfolded))
+                    (stx-cdr #'info-unfolded))) ; drop leading #%app
                (syntax->datum #'(Clause ...)))
        ;; this commented block experiments with expanding to unsafe ops
        ;; #:with ((acc ...) ...) (stx-map 
@ -660,7 +686,6 @@
    [(_ . rst) (syntax-property #'(∀ () (ext-stlc:→ . rst)) 'orig (list #'(→ . rst)))]))
 ; special arrow that computes free vars; for use with tests
 ; (because we can't write explicit forall
-(provide →/test)
 (define-syntax →/test 
  (syntax-parser
    [(_ (~and Xs (X:id ...)) . rst)
@ -730,8 +755,7 @@
        #'(ext-stlc:#%app e_fn/ty (add-expected e_arg τ_inX) ...)])]
    [else
     ;; ) solve for type variables Xs
-     (define/with-syntax ((e_arg1- ...) tys-solved) 
-       (solve #'Xs #'tyX_args stx))
+     (define/with-syntax ((e_arg1- ...) tys-solved) (solve #'Xs #'tyX_args stx))
     ;; ) instantiate polymorphic function type
     (syntax-parse (inst-types #'tys-solved #'Xs #'tyX_args)
      [(τ_in ... τ_out) ; concrete types
--- a/tapl/stx-utils.rkt
+++ b/tapl/stx-utils.rkt
@ -68,6 +68,11 @@
 (define (stx-drop stx n)
  (drop (syntax->list stx) n))

+(define (generate-temporariess stx)
+  (stx-map generate-temporaries stx))
+(define (generate-temporariesss stx)
+  (stx-map generate-temporariess stx))
+
 ;; based on make-variable-like-transformer from syntax/transformer,
 ;; but using (#%app id ...) instead of ((#%expression id) ...)
 (define (make-variable-like-transformer ref-stx)
--- a/tapl/tests/mlish/bg/monad.mlish
+++ b/tapl/tests/mlish/bg/monad.mlish
@ -114,9 +114,9 @@
 ;; check match2 nested datatype bug
 (check-type
    (match bq-tails-result with
-     [None -> (None {Int})]
+     [None -> None]
     [Some bq -> (bq-head bq)]) : (Option Int) -> (Some 4))
 (check-type
    (match2 bq-tails-result with
-     [None -> (None {Int})]
+     [None -> None]
     [Some bq -> (bq-head bq)]) : (Option Int) -> (Some 4))
--- a/tapl/tests/mlish/loop.mlish
+++ b/tapl/tests/mlish/loop.mlish
@ -0,0 +1,108 @@
+#lang s-exp "../../mlish.rkt"
+(require "../rackunit-typechecking.rkt")
+
+;; datatype with no self-reference
+(define-type (Test X)
+  (A X) 
+  (B X X))
+
+(check-type (A 1) : (Test Int))
+(check-type (B 1 2) : (Test Int))
+
+(check-type
+    (match (A 1) with
+     [A x -> x]
+     [B x y -> (+ x y)]) : Int -> 1)
+
+(check-type
+    (match (B 1 2) with
+     [A x -> x]
+     [B x y -> (+ x y)]) : Int -> 3)
+
+;; datatype with self-reference
+(define-type (Rec X)
+  N
+  (C X (Rec X)))
+
+(check-type N : (Rec Int) -> N)
+(check-type (N {Int}) : (Rec Int) -> (N {Int}))
+(check-type (C 1 N) : (Rec Int) -> (C 1 N))
+
+(check-type
+    (match (N {Int}) with
+     [N -> 0]
+     [C x xs -> x]) : Int -> 0)
+
+(check-type
+    (match (C 1 N) with
+     [N -> 0]
+     [C x xs -> x]) : Int -> 1)
+
+;; mutually referential datatypes
+(define-type (Loop1 X)
+  (L1 (Loop2 X)))
+(define-type (Loop2 X)
+  (L2 (Loop1 X)))
+
+(define (looping-f [x : (Loop1 Y)] -> (Loop1 Y)) x)
+
+(define-type (ListA X)
+  NA
+  (CA X (ListB X)))
+(define-type (ListB X)
+  NB
+  (CB X (ListA X)))
+
+;; TODO: error should occur here
+(define-type (ListC X)
+  NC
+  (CC X (ListA X X))) ; misapplication of ListA type constructor
+
+(check-type NC : (ListC Int))
+(typecheck-fail (CC 1 NA)) ; and not here
+
+;; (define (g [x : (ListA Int Int)] -> Int) 0)
+
+(typecheck-fail (CA 1 NA))
+(check-type (CA 1 NB) : (ListA Int))
+(check-type (CA 1 (CB 2 NA)) : (ListA Int))
+(typecheck-fail (CA 1 (CB 2 NB)))
+(typecheck-fail (CB 1 NB))
+(check-type (CB 1 NA) : (ListB Int))
+(check-type (CB 1 (CA 2 NB)) : (ListB Int))
+(typecheck-fail (CB 1 (CA 2 NA)))
+
+(check-type
+    (match (CA 1 NB) with
+     [NA -> 0]
+     [CA x xs -> x]) : Int -> 1)
+
+(check-type
+    (match (CA 1 (CB 2 NA)) with
+     [NA -> 0]
+     [CA x xs ->
+      (match xs with
+       [NB -> 3]
+       [CB x xs -> x])]) : Int -> 2)
+
+;; "real world" mutually referential datatypes
+(define-type (BankersDeque A)
+  [BD Int (List A) Int (List A)])
+
+(define-type (ImplicitCatDeque A)
+  [Shallow (BankersDeque A)]
+  [Deep (BankersDeque A)
+        (ImplicitCatDeque (BankersDeque (CmpdElem (BankersDeque A))))
+        (BankersDeque A)
+        (ImplicitCatDeque (BankersDeque (CmpdElem (BankersDeque A))))
+        (BankersDeque A)])
+
+(define-type (CmpdElem A)
+  [Simple (BankersDeque A)]
+  [Cmpd (BankersDeque A) 
+        (ImplicitCatDeque 
+          (BankersDeque (CmpdElem (BankersDeque A)))) (BankersDeque A)])
+
+(define (id (icd : (ImplicitCatDeque Int)) → (ImplicitCatDeque Int))
+  icd)
+
--- a/tapl/tests/mlish/polyrecur.mlish
+++ b/tapl/tests/mlish/polyrecur.mlish
@ -109,7 +109,7 @@
        (BankersDeque A)])


-(typecheck-fail
+#;(typecheck-fail
  (λ ([icd : (ImplicitCatDeque A)]) icd)
  #:with-msg 
  "type constructor ImplicitCatDeque expects 1 args, given 2")
--- a/tapl/tests/run-all-mlish-tests.rkt
+++ b/tapl/tests/run-all-mlish-tests.rkt
@ -1,36 +1,24 @@
-#lang racket
+#lang racket/base
+(require racket/match racket/system racket/port)

 (match-define (list i1 o1 id1 err1 f1)
  (process "time racket run-mlish-tests1.rkt"))
-(match-define (list i1b o1b id1b err1b f1b)
-  (process "time racket run-mlish-tests1b.rkt"))
 (match-define (list i2 o2 id2 err2 f2)
  (process "time racket run-mlish-tests2.rkt"))
 (match-define (list i3 o3 id3 err3 f3)
-  (process "time racket mlish/bg/basics.mlish"))
-(match-define (list i3b o3b id3b err3b f3b)
-  (process "time racket mlish/bg/basics2.mlish"))
-(match-define (list i3c o3c id3c err3c f3c)
  (process "time racket run-mlish-tests3.rkt"))
 (match-define (list i4 o4 id4 err4 f4)
  (process "time racket run-mlish-tests4.rkt"))

-(displayln "----- General tests and queens: ---------------------------------")
+(displayln "----- General MLish tests: --------------------------------------")
 (write-string (port->string err1))
 (write-string (port->string i1))
-(displayln "----- Shootout tests: -------------------------------------------")
-(write-string (port->string err1b))
-(write-string (port->string i1b))
-(displayln "----- RW OCaml tests: -------------------------------------------")
+(displayln "----- Shootout and RW OCaml tests: ------------------------------")
 (write-string (port->string err2))
 (write-string (port->string i2))
 (displayln "----- Ben's tests: ----------------------------------------------")
 (write-string (port->string err3))
 (write-string (port->string i3))
-(write-string (port->string err3b))
-(write-string (port->string i3b))
-(write-string (port->string err3c))
-(write-string (port->string i3c))
 (displayln "----- Okasaki / polymorphic recursion tests: --------------------")
 (write-string (port->string err4))
 (write-string (port->string i4))
@ -38,51 +26,12 @@
 (close-input-port i1)
 (close-output-port o1)
 (close-input-port err1)
-(close-input-port i1b)
-(close-output-port o1b)
-(close-input-port err1b)
 (close-input-port i2)
 (close-output-port o2)
 (close-input-port err2)
 (close-input-port i3)
 (close-output-port o3)
 (close-input-port err3)
-(close-input-port i3b)
-(close-output-port o3b)
-(close-input-port err3b)
-(close-input-port i3c)
-(close-output-port o3c)
-(close-input-port err3c)
 (close-input-port i4)
 (close-output-port o4)
 (close-input-port err4)
-
-;; (require "mlish-tests.rkt")
-;; (require "mlish/queens.mlish")
-;; (require "mlish/trees.mlish")
-;; (require "mlish/chameneos.mlish")
-;; (require "mlish/ack.mlish")
-;; (require "mlish/ary.mlish")
-;; (require "mlish/fannkuch.mlish")
-;; (require "mlish/fasta.mlish")
-;; (require "mlish/fibo.mlish")
-;; (require "mlish/hash.mlish")
-;; ;(require "mlish/heapsort.mlish")
-;; (require "mlish/knuc.mlish")
-;; (require "mlish/matrix.mlish")
-;; (require "mlish/nbody.mlish")
-
-;; ;; from rw ocaml
-;; (require "mlish/term.mlish")
-;; (require "mlish/find.mlish")
-;; (require "mlish/alex.mlish")
-;; (require "mlish/inst.mlish")
-;; (require "mlish/result.mlish")
-
-;; ;; bg
-;; (require "mlish/bg/basics.mlish")
-;; (require "mlish/bg/huffman.mlish")
-;; (require "mlish/bg/lambda.rkt")
-
-;; ;; okasaki, polymorphic recursion
-;; (require "mlish/polyrecur.mlish")
--- a/tapl/tests/run-mlish-tests1.rkt
+++ b/tapl/tests/run-mlish-tests1.rkt
@ -1,8 +1,10 @@
 #lang racket/base
 (require "mlish-tests.rkt")
-(require "mlish/queens.mlish")
+;(require "mlish/queens.mlish")
 (require "mlish/listpats.mlish")
 (require "mlish/match2.mlish")
+(require "mlish/polyrecur.mlish")
+(require "mlish/loop.mlish")

 ;; (require "mlish/trees.mlish")
 ;; (require "mlish/chameneos.mlish")
--- a/tapl/tests/run-mlish-tests1b.rkt
+++ b/tapl/tests/run-mlish-tests1b.rkt
@ -1,15 +0,0 @@
-#lang racket/base
-;; (require "mlish-tests.rkt")
-;(require "mlish/queens.mlish")
-(require "mlish/trees-tests.mlish")
-(require "mlish/chameneos.mlish")
-(require "mlish/ack.mlish")
-(require "mlish/ary.mlish")
-(require "mlish/fannkuch.mlish")
-(require "mlish/fasta.mlish")
-(require "mlish/fibo.mlish")
-(require "mlish/hash.mlish")
-;(require "mlish/heapsort.mlish")
-(require "mlish/knuc.mlish")
-(require "mlish/matrix.mlish")
-(require "mlish/nbody.mlish")
--- a/tapl/tests/run-mlish-tests2.rkt
+++ b/tapl/tests/run-mlish-tests2.rkt
@ -1,4 +1,21 @@
 #lang racket/base
+
+(require "mlish/queens.mlish")
+
+;; shootout tests
+(require "mlish/trees-tests.mlish")
+(require "mlish/chameneos.mlish")
+(require "mlish/ack.mlish")
+(require "mlish/ary.mlish")
+(require "mlish/fannkuch.mlish")
+(require "mlish/fasta.mlish")
+(require "mlish/fibo.mlish")
+(require "mlish/hash.mlish")
+;(require "mlish/heapsort.mlish")
+(require "mlish/knuc.mlish")
+(require "mlish/matrix.mlish")
+(require "mlish/nbody.mlish")
+
 ;; from rw ocaml
 (require "mlish/term.mlish")
 (require "mlish/find.mlish")
--- a/tapl/tests/run-mlish-tests3.rkt
+++ b/tapl/tests/run-mlish-tests3.rkt
@ -1,5 +1,7 @@
 #lang racket/base
 ;; bg
+(require "mlish/bg/basics.mlish")
+(require "mlish/bg/basics2.mlish")
 (require "mlish/bg/huffman.mlish")
 (require "mlish/bg/lambda.mlish")
 (require "mlish/bg/monad.mlish")
--- a/tapl/tests/run-mlish-tests4.rkt
+++ b/tapl/tests/run-mlish-tests4.rkt
@ -1,5 +1,5 @@
 #lang racket/base

 ;; okasaki tests
-(require "mlish/polyrecur.mlish")
+;(require "mlish/polyrecur.mlish")
 (require "mlish/bg/okasaki.mlish")
--- a/tapl/typecheck.rkt
+++ b/tapl/typecheck.rkt
@ -6,9 +6,9 @@
              "stx-utils.rkt")
  (for-meta 2 racket/base syntax/parse racket/syntax syntax/stx "stx-utils.rkt")
  (for-meta 3 racket/base syntax/parse racket/syntax)
-  racket/bool racket/provide racket/require racket/match)
+  racket/bool racket/provide racket/require racket/match racket/promise)
 (provide
- symbol=? match
+ symbol=? match delay
 (except-out (all-from-out racket/base) #%module-begin)
 (for-syntax (all-defined-out)) (all-defined-out)
 (for-syntax
@ -431,9 +431,9 @@
    (syntax-parse t
      [((~literal #%plain-app) internal-id
        ((~literal #%plain-lambda) bvs
-         ((~literal #%expression) extra-info-to-extract) . rst))
-       #'extra-info-to-extract]
-      [_ #'void]))
+         ((~literal #%expression) ((~literal quote) extra-info-macro)) . tys))
+       (expand/df #'(extra-info-macro . tys))]
+      [_ #f]))
  (define (get-tyargs ty)
    (syntax-parse ty
      [((~literal #%plain-app) internal-id
@ -493,9 +493,10 @@
         #:defaults ([bvs-op #'=][bvs-n #'0]))
        (~optional (~seq #:arr (~and (~parse has-annotations? #'#t) tycon))
         #:defaults ([tycon #'void]))
-        (~optional (~seq #:extra-info extra-bvs extra-info)
+        #;(~optional (~seq #:extra-info extra-bvs extra-info)
                   #:defaults ([extra-bvs #'()]
                               [extra-info #'void]))
+        (~optional (~seq #:extra-info extra-info) #:defaults ([extra-info #'void]))
        (~optional (~and #:no-provide (~parse no-provide? #'#t)))
        )
     #:with #%kind (format-id #'kind "#%~a" #'kind)
@ -580,14 +581,14 @@
               #:with k_result (if #,(attribute has-annotations?)
                                   #'(tycon k_arg (... ...))
                                   #'#%kind)
-               #:with extra-info-inst
-                      (if (stx-null? #'extra-bvs)
-                          #'extra-info
-                          (substs #'τs- #'extra-bvs #'extra-info))
+               ;; #:with extra-info-inst
+               ;;        (if (stx-null? #'extra-bvs)
+               ;;            #'extra-info
+               ;;            (substs #'τs- #'extra-bvs #'extra-info))
               (add-orig
                (assign-type 
                  (syntax/loc stx 
-                    (τ-internal (λ bvs- (#%expression extra-info-inst) . τs-))) 
+                    (τ-internal (λ bvs- (#%expression extra-info) . τs-))) 
                  #'k_result)
                #'(τ . args))]
             ;; else fail with err msg