From c72d4a7f4009a9677a78883a546349169cd0bb6c Mon Sep 17 00:00:00 2001
From: AlexKnauth <alexander@knauth.org>
Date: Tue, 21 Jun 2016 21:58:21 -0400
Subject: [PATCH] more work on exist and mlish-core

---
 tapl/typed-lang-builder/exist.rkt      |  4 +-
 tapl/typed-lang-builder/mlish-core.rkt | 60 +++++++++++---------------
 2 files changed, 27 insertions(+), 37 deletions(-)

diff --git a/tapl/typed-lang-builder/exist.rkt b/tapl/typed-lang-builder/exist.rkt
index b4ec669..30292b5 100644
--- a/tapl/typed-lang-builder/exist.rkt
+++ b/tapl/typed-lang-builder/exist.rkt
@@ -17,8 +17,8 @@
 (define-typed-syntax pack
   [(pack (τ:type e) as ∃τ:type) ▶
    [#:with (~∃* (τ_abstract) τ_body) #'∃τ.norm]
-   [⊢ [[e ≫ e-] ⇒ : τ_e]]
-   [#:when (typecheck? #'τ_e  (subst #'τ.norm #'τ_abstract #'τ_body))]
+   [#:with τ_e (subst #'τ.norm #'τ_abstract #'τ_body)]
+   [⊢ [[e ≫ e-] ⇐ : τ_e]]
    --------
    [⊢ [[_ ≫ e-] ⇒ : ∃τ.norm]]])
 
diff --git a/tapl/typed-lang-builder/mlish-core.rkt b/tapl/typed-lang-builder/mlish-core.rkt
index 26b6b35..abbf7d2 100644
--- a/tapl/typed-lang-builder/mlish-core.rkt
+++ b/tapl/typed-lang-builder/mlish-core.rkt
@@ -676,25 +676,23 @@
     (stx-map (lambda (p) (list (get-ctx p ty) (compile-pat p ty))) pats))
   )
 
-(define-syntax (match2 stx)
- (syntax-parse stx #:datum-literals (with)
-   [(match2 e with . clauses)
-    #:fail-when (null? (syntax->list #'clauses)) "no clauses"
-    #:with [e- τ_e] (infer+erase #'e)
-    (syntax-parse #'clauses #:datum-literals (->)
-     [([(~seq p ...) -> e_body] ...)
-      #: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 ty-expected (get-expected-type stx)
-      #:with ([(x- ...) e_body- ty_body] ...) 
-             (stx-map 
-               infer/ctx+erase 
-               #'(ctx ...) #'((add-expected e_body ty-expected) ...))
-      #:when (check-exhaust #'(pat- ...) #'τ_e)
-      (⊢ (match- e- [pat- (let- ([x- x] ...) e_body-)] ...) : (⊔ ty_body ...))
-      ])]))
+(define-typed-syntax match2 #:datum-literals (with ->)
+  [(match2 e with . clauses) ▶
+   [#:fail-unless (not (null? (syntax->list #'clauses))) "no clauses"]
+   [⊢ [[e ≫ e-] ⇒ : τ_e]]
+   [#:with ([(~seq p ...) -> e_body] ...) #'clauses]
+   [#: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 ty-expected (get-expected-type stx)]
+   [() ([x : ty ≫ x-] ...)
+    ⊢ [[(add-expected e_body ty-expected) ≫ e_body-] ⇒ : ty_body]]
+   ...
+   [#:when (check-exhaust #'(pat- ...) #'τ_e)]
+   --------
+   [⊢ [[_ ≫ (match- e- [pat- (let- ([x- x] ...) e_body-)] ...)]
+       ⇒ : (⊔ ty_body ...)]]])
 
 (define-typed-syntax match #:datum-literals (with -> ::)
   ;; e is a tuple
@@ -707,8 +705,8 @@
    [#:with (~× ty ...) #'τ_e]
    [#:fail-unless (stx-length=? #'(ty ...) #'(x ...))
                   "match clause pattern not compatible with given tuple"]
-   [#:with [(x- ...) e_body- ty_body] (infer/ctx+erase #'([x ty] ...) 
-                                                       #'(add-expected e_body t_expect))]
+   [() ([x : ty ≫ x-] ...)
+    ⊢ [[(add-expected e_body t_expect) ≫ e_body-] ⇒ : ty_body]]
    [#:with (acc ...) (for/list ([(a i) (in-indexed (syntax->list #'(x ...)))])
                        #`(lambda (s) (list-ref s #,(datum->syntax #'here i))))]
    [#:with z (generate-temporary)]
@@ -734,9 +732,9 @@
                             (= 1 (stx-length #'(xs ...)))))
     "match: missing non-empty list case"]
    [#:with (~List ty) #'τ_e]
-   [#:with ([(x- ... rst-) e_body- ty_body] ...)
-    (stx-map (lambda (ctx e) (infer/ctx+erase ctx e)) 
-             #'(([x ty] ... [rst (List ty)]) ...) #'((add-expected e_body t_expect) ...))]
+   [() ([x : ty ≫ x-] ... [rst : (List ty) ≫ rst-])
+    ⊢ [[(add-expected e_body t_expect) ≫ e_body-] ⇒ : ty_body]]
+   ...
    [#:with (len ...) (stx-map (lambda (p) #`#,(stx-length p)) #'((x ...) ...))]
    [#:with (lenop ...) (stx-map (lambda (p) (if (brack? p) #'=- #'>=-)) #'(xs ...))]
    [#:with (pred? ...) (stx-map
@@ -792,17 +790,9 @@
    ;;                             #`(lambda (s) (unsafe-struct*-ref s #,(datum->syntax #'here i)))))
    ;;                          #'((acc-fn ...) ...))]
    [#:with (e_c ...+) (stx-map (lambda (ec) (add-expected-ty ec #'t_expect)) #'(e_c_un ...))]
-   ;TODO: get this working
-   ;[() ([x : τ ≫ x-] ...)
-   ; ⊢ [[e_guard ≫ e_guard-] ⇐ : Bool] [[e_c ≫ e_c-] ⇒ : τ_ec]]
-   ;...
-   [#:with (((x- ...) (e_guard- e_c-) (τ_guard τ_ec)) ...)
-    (stx-map 
-     (λ (bs eg+ec) (infers/ctx+erase bs eg+ec)) 
-     #'(([x : τ] ...) ...) #'((e_guard e_c) ...))]
-   [#:fail-unless (and (same-types? #'(τ_guard ...))
-                       (Bool? (stx-car #'(τ_guard ...))))
-    "guard expression(s) must have type bool"]
+   [() ([x : τ ≫ x-] ...)
+    ⊢ [[e_guard ≫ e_guard-] ⇐ : Bool] [[e_c ≫ e_c-] ⇒ : τ_ec]]
+   ...
    [#:with z (generate-temporary)] ; dont duplicate eval of test expr
    --------
    [⊢ [[_ ≫ (let- ([z e-])