fix mlish match

- properly propagate expected-type
- need cond that checks all cases at runtime
 - need to compute accessors and predicate
- add tests

tapl/mlish.rkt

@@ -113,11 +113,11 @@
      #`(begin
          (define-type-constructor Name
            #:arity = #,(stx-length #'(X ...))
-           #:other-prop variants #'(X ...) #'((Cons τ ...) ...))
+           #:other-prop variants #'(X ...) #'((Cons StructName [fld : τ] ...) ...))
          (struct StructName (fld ...) #:reflection-name 'Cons #:transparent) ...
          (define-syntax (Cons stx)
            (syntax-parse stx
-             ; no args and not poly morphic
+             ; no args and not polymorphic
              [C:id #:when (and (stx-null? #'(X ...)) (stx-null? #'(τ ...))) #'(C)]
              ; no args but polymorphic, check inferred type
              [C:id
@@ -191,18 +191,27 @@
   (syntax-parse stx #:datum-literals (with ->)
     [(_ e with . clauses)
      #:fail-when (null? (syntax->list #'clauses)) "no clauses"
-     #:with ([Clause:id x ... -> e_c] ...) (stx-sort #'clauses symbol<?)
+     #:with ([Clause:id x ... -> e_c_un] ...) (stx-sort #'clauses symbol<?) ; un = unannotated with expected ty
      #:with [e- τ_e] (infer+erase #'e)
-     #:with ((Cons τ ...) ...) (stx-sort (syntax-property #'τ_e 'variants) symbol<?)
+     #:with ((Cons Cons2 [fld (~datum :) τ] ...) ...) (stx-sort (syntax-property #'τ_e 'variants) symbol<?)
      #:fail-unless (= (stx-length #'(Clause ...)) (stx-length #'(Cons ...))) "wrong number of case clauses"
      #:fail-unless (typechecks? #'(Clause ...) #'(Cons ...)) "case clauses not exhaustive"
+     #:with ((acc ...) ...) (stx-map 
+                             (lambda (C fs) 
+                               (stx-map (lambda (f) (format-id C "~a-~a" C f)) fs)) 
+                             #'(Cons2 ...) 
+                             #'((fld ...) ...))
+     #:with (Cons? ...) (stx-map (lambda (C) (format-id C "~a?" C)) #'(Cons2 ...))
+     #:with t_expect (syntax-property stx 'expected-type) ; propagate inferred type
+     #:with (e_c ...) (stx-map (lambda (ec) (add-expected-ty ec #'t_expect)) #'(e_c_un ...))
      #:with (((x- ...) e_c- τ_ec) ...)
             (stx-map (λ (bs e) (infer/ctx+erase bs e)) #'(([x : τ] ...) ...) #'(e_c ...))
      #:fail-unless (same-types? #'(τ_ec ...)) "branches have different types"
-     #:with C (syntax-property #'τ_e 'constructor)
-     #:with (_ (x_out ...) e_out τ_out) (stx-assoc #'C #'((Clause (x- ...) e_c- τ_ec) ...))
-     #:with (acc ...) (syntax-property #'τ_e 'accessors)
-     (⊢ (let ([x_out (acc e-)] ...) e_out) : τ_out)]))
+     ;; #:with C (syntax-property #'τ_e 'constructor) ; check if variant is known statically
+     ;; #:with (acc ...) (syntax-property #'τ_e 'accessors)
+     ;; #:with (_ (x_out ...) e_out τ_out) (stx-assoc #'C #'((Clause (x- ...) e_c- τ_ec) ...))
+     #:with τ_out (stx-car #'(τ_ec ...))
+     (⊢ (cond [(Cons? e-) (let ([x- (acc e-)] ...) e_c-)] ...) : τ_out)]))
 
 #;(define-syntax lifted→ ; wrap → with ∀
   (syntax-parser

tapl/tests/mlish-tests.rkt

@@ -1,8 +1,6 @@
 #lang s-exp "../mlish.rkt"
 (require "rackunit-typechecking.rkt")
 
-(define (recf [x : Int] → Int) (recf x))
-
 ;; tests more or less copied from infer-tests.rkt ------------------------------
 ;; top-level defines
 (define (f [x : Int] → Int) x)
@@ -32,12 +30,13 @@
   (expected "(List X)" #:given "Int"
    #:note  "Could not infer instantiation of polymorphic function"))
 
-;(check-type (g2 (Nil {Int})) : (List Int) ⇒ (Nil {Int}))
-;(check-type (g2 (Nil {Bool})) : (List Bool) ⇒ (Nil {Bool}))
-;(check-type (g2 (Nil {(List Int)})) : (List (List Int)) ⇒ (Nil {(List Int)}))
-;(check-type (g2 (Nil {(→ Int Int)})) : (List (→ Int Int)) ⇒ (Nil {(List (→ Int Int))}))
-;(check-type (g2 (Cons 1 Nil)) : (List Int) ⇒ (Cons 1 Nil))
-;(check-type (g2 (Cons "1" Nil)) : (List String) ⇒ (Cons "1" Nil))
+;; todo? allow polymorphic nil?
+(check-type (g2 (Nil {Int})) : (List Int) ⇒ (Nil {Int}))
+(check-type (g2 (Nil {Bool})) : (List Bool) ⇒ (Nil {Bool}))
+(check-type (g2 (Nil {(List Int)})) : (List (List Int)) ⇒ (Nil {(List Int)}))
+(check-type (g2 (Nil {(→ Int Int)})) : (List (→ Int Int)) ⇒ (Nil {(List (→ Int Int))}))
+(check-type (g2 (Cons 1 Nil)) : (List Int) ⇒ (Cons 1 Nil))
+(check-type (g2 (Cons "1" Nil)) : (List String) ⇒ (Cons "1" Nil))
 
 ;(define (g3 [lst : (List X)] → X) (hd lst)) ; cant type this fn (what to put for nil case)
 ;(check-type g3 : (→ {X} (List X) X))
@@ -49,17 +48,27 @@
 ;(check-type (g3 (cons 1 nil)) : Int ⇒ 1)
 ;(check-type (g3 (cons "1" nil)) : String ⇒ "1")
 
-; recursive fn
-;(define (recf [x : Int] → Int) (recf x))
-;(check-type recf : (→ Int Int))
-;
-;(define (countdown [x : Int] → Int)
-;  (if (zero? x)
-;      0
-;      (countdown (sub1 x))))
-;(check-type (countdown 0) : Int ⇒ 0)
-;(check-type (countdown 10) : Int ⇒ 0)
-;(typecheck-fail (countdown "10") #:with-msg "Arguments.+have wrong type")
+;; recursive fn
+(define (recf [x : Int] → Int) (recf x))
+(check-type recf : (→ Int Int))
+
+(define (countdown [x : Int] → Int)
+  (if (zero? x)
+      0
+      (countdown (sub1 x))))
+(check-type (countdown 0) : Int ⇒ 0)
+(check-type (countdown 10) : Int ⇒ 0)
+(typecheck-fail (countdown "10") #:with-msg (expected "Int" #:given "String"))
+
+;; list fns ----------
+
+
+; map: tests whether match and define properly propagate 'expected-type
+(define (map [f : (→ X Y)] [lst : (List X)] → (List Y))
+  (match lst with
+   [Nil -> Nil]
+   [Cons x xs -> (Cons (f x) (map f xs))]))
+
 
 ;; end infer.rkt tests --------------------------------------------------
 
@@ -271,7 +280,7 @@
 ;; tests from stlc+lit-tests.rkt --------------------------
 ; most should pass, some failing may now pass due to added types/forms
 (check-type 1 : Int)
-;(check-not-type 1 : (Int → Int))
+(check-not-type 1 : (→ Int Int))
 ;(typecheck-fail "one") ; literal now supported
 ;(typecheck-fail #f) ; literal now supported
 (check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int))

tapl/typecheck.rkt

@@ -124,6 +124,9 @@
 ;     #:when (printf "adding expected type ~a to expression ~a\n"
 ;                    (syntax->datum #'τ) (syntax->datum #'e))
      (syntax-property #'e 'expected-type #'τ)]))
+(define-for-syntax (add-expected-ty e ty)
+  (or (and (syntax-e ty) (syntax-property e 'expected-type ((current-type-eval) ty)))
+      e))
 
 ;; type assignment
 (begin-for-syntax