From cb36097f8d7cb9bd86f2d371a7acd71ebf06d2e0 Mon Sep 17 00:00:00 2001
From: Stephen Chang <stchang@ccs.neu.edu>
Date: Wed, 5 Oct 2016 10:33:18 -0400
Subject: [PATCH] mlish define-type to more closely resemble paper

---
 turnstile/examples/mlish.rkt | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

diff --git a/turnstile/examples/mlish.rkt b/turnstile/examples/mlish.rkt
index b7430e5..59b372d 100644
--- a/turnstile/examples/mlish.rkt
+++ b/turnstile/examples/mlish.rkt
@@ -458,23 +458,24 @@
              #`(app 
                 #,(assign-type #'Cons? #'(?∀ (X ...) (ext-stlc:→ (Name X ...) Bool))) 
                 . rst)])) ...
+         ;; TODO: remove default provides to use define-typed-syntax here
          (define-syntax (Cons stx)
            (syntax-parse/typed-syntax stx
              ; no args and not polymorphic
              [C:id ≫
               #:when (and (stx-null? #'(X ...)) (stx-null? #'(τ ...)))
               --------
-              [_ ≻ (C)]]
+              [≻ (C)]]
              ; no args but polymorphic, check expected type
-             [C:id ⇐ : (NameExpander τ-expected-arg (... ...)) ≫
+             [:id ⇐ (NameExpander τ-expected-arg (... ...)) ≫
               #:when (stx-null? #'(τ ...))
               --------
-              [⊢ [_ ≫ (StructName) ⇐ : _]]]
+              [⊢ (StructName)]]
              ; id with multiple expected args, HO fn
-             [C:id ≫
+             [:id ≫
               #:when (not (stx-null? #'(τ ...)))
               --------
-              [⊢ [_ ≫ StructName ⇒ : (?∀ (X ...) (ext-stlc:→ τ ... (Name X ...)))]]]
+              [⊢ StructName ⇒ (?∀ (X ...) (ext-stlc:→ τ ... (Name X ...)))]]
              [(C τs e_arg ...) ≫
               #:when (brace? #'τs) ; commit to this clause
               #:with [X* (... ...)] #'[X ...]
@@ -482,10 +483,11 @@
               #:with {~! τ_X:type (... ...)} #'τs
               #:with (τ_in:type (... ...)) ; instantiated types
               (inst-types/cs #'(X ...) #'([X* τ_X.norm] (... ...)) #'(τ ...))
-              [⊢ [e_arg* ≫ e_arg*- ⇐ : τ_in.norm] (... ...)]
+              ;; e_arg* helps align ellipses
+              [⊢ e_arg* ≫ e_arg*- ⇐ τ_in.norm] (... ...)
               #:with [e_arg- ...] #'[e_arg*- (... ...)]
               --------
-              [⊢ [_ ≫ (StructName e_arg- ...) ⇒ : (Name τ_X.norm (... ...))]]]
+              [⊢ (StructName e_arg- ...) ⇒ (Name τ_X.norm (... ...))]]
              [(C . args) ≫ ; no type annotations, must infer instantiation
               #:with StructName/ty 
               (set-stx-prop/preserved
@@ -493,7 +495,7 @@
                'orig
                (list #'C))
               --------
-              [_ ≻ (mlish:#%app StructName/ty . args)]]))
+              [≻ (mlish:#%app StructName/ty . args)]]))
          ...)]))
 
 ;; match --------------------------------------------------