From 3ad9fa2fb1939dab0a17eaac31f21b7ae5077860 Mon Sep 17 00:00:00 2001
From: AlexKnauth <alexander@knauth.org>
Date: Wed, 22 Jun 2016 11:00:13 -0400
Subject: [PATCH] =?UTF-8?q?allow=20nested=20=E2=87=92=20arrows=20in=20the?=
 =?UTF-8?q?=20conclusion?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 tapl/typed-lang-builder/stlc+effect.rkt       | 35 +++----------------
 .../typed-lang-builder/typed-lang-builder.rkt | 27 +++++++++++---
 2 files changed, 26 insertions(+), 36 deletions(-)

diff --git a/tapl/typed-lang-builder/stlc+effect.rkt b/tapl/typed-lang-builder/stlc+effect.rkt
index 5bb2ba0..8b2485b 100644
--- a/tapl/typed-lang-builder/stlc+effect.rkt
+++ b/tapl/typed-lang-builder/stlc+effect.rkt
@@ -1,8 +1,6 @@
 #lang macrotypes/tapl/typed-lang-builder
 (extends "stlc+box.rkt" #:except ref deref := #%app λ)
 
-(provide (for-syntax get-new-effects))
-
 ;; Simply-Typed Lambda Calculus, plus mutable references
 ;; Types:
 ;; - types from stlc+cons.rkt
@@ -23,31 +21,6 @@
                 (~parse ((~literal quote) (loc ...))
                         (stx-or #'tmp #'(quote ()))))])))
 
-  (define (add-news e locs) (assign-type e #:tag 'ν locs))
-  (define (add-assigns e locs) (assign-type e #:tag ':= locs))
-  (define (add-derefs e locs) (assign-type e #:tag '! locs))
-  (define (add-effects e new-locs assign-locs deref-locs)
-    (add-derefs
-     (add-assigns
-      (add-news e new-locs)
-      assign-locs)
-     deref-locs))
-     
-  (define (get-effects e tag)
-    (syntax-property e tag))
-  (define (get-new-effects e) (get-effects e 'ν))
-  (define (get-assign-effects e) (get-effects e ':=))
-  (define (get-deref-effects e) (get-effects e '!))
-  
-  (define (print-effects e)
-    (printf "expr ~a\n" (syntax->datum e))
-    (define e+ (local-expand e 'expression null))
-    (printf "new locs: ~a\n" (syntax-property e+ 'ν))
-    (printf "deref locs: ~a\n" (syntax-property e+ '!))
-    (printf "assign locs: ~a\n" (syntax-property e+ ':=)))
-
-  (define (stx-cons a b)
-    (datum->syntax #f (cons a b)))
   (define (stx-truth? a)
     (and a (not (and (syntax? a) (false? (syntax-e a))))))
   (define (stx-or a b)
@@ -90,10 +63,10 @@
         (⇒ ! (~locs ds ...))]]
    --------
    [⊢ [[_ ≫ (λ- (x- ...) e-)]
-       (⇒ : #,(add-effects #'(→ bvs.type ... τ_res)
-                           #'(locs ns ...)
-                           #'(locs as ...)
-                           #'(locs ds ...)))]]])
+       (⇒ : (→ bvs.type ... τ_res)
+          (⇒ ν (locs ns ...))
+          (⇒ := (locs as ...))
+          (⇒ ! (locs ds ...)))]]])
 
 (define-type-constructor Ref)
 
diff --git a/tapl/typed-lang-builder/typed-lang-builder.rkt b/tapl/typed-lang-builder/typed-lang-builder.rkt
index 6a525a1..e062cc4 100644
--- a/tapl/typed-lang-builder/typed-lang-builder.rkt
+++ b/tapl/typed-lang-builder/typed-lang-builder.rkt
@@ -45,6 +45,16 @@
                      (~parse
                       (~and tag-prop.e-pat ... tag-pat)
                       (typeof #'e-tmp #:tag 'tag)))])
+  (define-splicing-syntax-class ⇒-prop/conclusion
+    #:datum-literals (⇒)
+    #:attributes (tag tag-expr)
+    [pattern (~seq ⇒ tag:id tag-stx (tag-prop:⇒-prop/conclusion) ...)
+             #:with tag-expr
+             (for/fold ([tag-expr #'#`tag-stx])
+                       ([k (in-list (syntax->list #'[tag-prop.tag ...]))]
+                        [v (in-list (syntax->list #'[tag-prop.tag-expr ...]))])
+               (with-syntax ([tag-expr tag-expr] [k k] [v v])
+                 #'(assign-type tag-expr #:tag 'k v)))])
   (define-splicing-syntax-class ⇐-prop
     #:datum-literals (⇐ :)
     [pattern (~seq ⇐ : τ-stx)
@@ -72,6 +82,12 @@
     [pattern (~seq (p:⇐-prop) (p2:⇒-prop) ...)
              #:with τ-stx #'p.τ-stx
              #:with e-pat #'(~and p.e-pat p2.e-pat ...)])
+  (define-splicing-syntax-class ⇒-props/conclusion
+    #:attributes ([tag 1] [tag-expr 1])
+    [pattern (~seq p:⇒-prop/conclusion)
+             #:with [tag ...] #'[p.tag]
+             #:with [tag-expr ...] #'[p.tag-expr]]
+    [pattern (~seq (:⇒-prop/conclusion) ...)])
   (define-splicing-syntax-class id+props+≫
     #:datum-literals (≫)
     #:attributes ([x- 1] [ctx 1])
@@ -165,13 +181,14 @@
     #:attributes ([pat 0] [stuff 1] [body 0])
     [pattern [⊢ [[pat* ≫ e-stx] ⇒ k v]]
              #:with :last-clause #'[⊢ [[pat* ≫ e-stx] (⇒ k v)]]]
-    [pattern [⊢ [[pat ≫ e-stx] (⇒ k:id v) ...]]
+    [pattern [⊢ [[pat ≫ e-stx] props:⇒-props/conclusion]]
              #:with [stuff ...] #'[]
              #:with body:expr
-             #'(for/fold ([result (quasisyntax/loc this-syntax e-stx)])
-                         ([tag (in-list (list 'k ...))]
-                          [τ (in-list (list #`v ...))])
-                 (assign-type result τ #:tag tag))]
+             (for/fold ([body #'(quasisyntax/loc this-syntax e-stx)])
+                       ([k (in-list (syntax->list #'[props.tag ...]))]
+                        [v (in-list (syntax->list #'[props.tag-expr ...]))])
+               (with-syntax ([body body] [k k] [v v])
+                 #'(assign-type body #:tag 'k v)))]
     [pattern [⊢ [[pat* ≫ e-stx] ⇐ : τ-pat]]
              #:with stx (generate-temporary 'stx)
              #:with τ (generate-temporary #'τ-pat)