From 61e99c8a2ef55ef3e26752abcd3adea5dc8a8548 Mon Sep 17 00:00:00 2001
From: "William J. Bowman" <wjb@williamjbowman.com>
Date: Sat, 9 Jan 2016 00:24:23 -0500
Subject: [PATCH] Improvements to match; replacing uses of case

* Match now infers the result more by adding pattern variables to
  local-env while inferring types.
* Replaced uses of case* and case with match when possible
---
 oll.rkt          |  8 ++++----
 stdlib/bool.rkt  |  2 +-
 stdlib/sugar.rkt | 44 ++++++++++++++++++++++++++------------------
 3 files changed, 31 insertions(+), 23 deletions(-)

diff --git a/oll.rkt b/oll.rkt
index 70c2acb..1618cc4 100644
--- a/oll.rkt
+++ b/oll.rkt
@@ -238,10 +238,10 @@
 (data Var : Type (avar : (-> Nat Var)))
 
 (define (var-equal? (v1 : Var) (v2 : Var))
-  (case* Var Type v1 () (lambda (v : Var) Bool)
-    [(avar (n1 : Nat)) IH: ()
-     (case* Var Type v2 () (lambda (v : Var) Bool)
-       [(avar (n2 : Nat)) IH: ()
+  (match v1
+    [(avar (n1 : Nat))
+     (match v2
+       [(avar (n2 : Nat))
         (nat-equal? n1 n2)])]))
 (module+ test
   (require rackunit)
diff --git a/stdlib/bool.rkt b/stdlib/bool.rkt
index d0709a7..61cc897 100644
--- a/stdlib/bool.rkt
+++ b/stdlib/bool.rkt
@@ -7,7 +7,7 @@
   (false : Bool))
 
 (define-syntax-rule (if t s f)
-  (case t
+  (match t
     [true s]
     [false f]))
 
diff --git a/stdlib/sugar.rkt b/stdlib/sugar.rkt
index f26b709..6f8eeaa 100644
--- a/stdlib/sugar.rkt
+++ b/stdlib/sugar.rkt
@@ -113,39 +113,46 @@
      #`(elim D U P #,@(map rewrite-clause (syntax->list #'(clause* ...))) p ... e)]))
 
 (begin-for-syntax
-  (define-struct clause (args body))
+  (define-struct clause (args types decl body))
   (define ih-dict (make-hash))
   (define (clause-parse syn)
     (syntax-case syn (:)
       [((con (a : A) ...) body)
-       (make-clause #'((a : A) ...) #'body)]
+       (make-clause (syntax->list #'(a ...)) (syntax->list #'(A ...)) #'((a : A) ...) #'body)]
       [(e body)
-       (make-clause #'() #'body)]))
+       (make-clause '() '() #'() #'body)]))
 
   (define (infer-result clauses)
-    (for/or ([clause clauses])
-      (type-infer/syn (clause-body clause))))
+    (or
+     (for/or ([clause clauses])
+       (type-infer/syn
+        (clause-body clause)
+        #:local-env (for/fold ([d '()])
+                              ([arg (clause-args clause)]
+                               [type (clause-types clause)])
+                          (dict-set d arg type))))
+     (raise-syntax-error
+      'match
+      "Could not infer type of result."
+      (clause-body (car clauses)))))
 
-  (define (infer-ihs D motive args-syn)
-    (syntax-case args-syn (:)
-      [((a : A) ...)
-       (for/fold ([ih-dict (make-immutable-hash)])
-                 ([type-syn (syntax->list #'(A ...))]
-                  [arg-syn (syntax->list #'(a ...))]
-		 ;; NB: Non-hygenic
-		 #:when (cur-equal? type-syn D))
-         (dict-set ih-dict (syntax->datum arg-syn) `(,(format-id args-syn "ih-~a" arg-syn) . ,#`(#,motive #,arg-syn))))]
-      [() '()]))
+  (define (infer-ihs D motive args types)
+    (for/fold ([ih-dict (make-immutable-hash)])
+              ([type-syn types]
+               [arg-syn args]
+               ;; NB: Non-hygenic
+               #:when (cur-equal? type-syn D))
+      (dict-set ih-dict (syntax->datum arg-syn) `(,(format-id arg-syn "ih-~a" arg-syn) . ,#`(#,motive #,arg-syn)))))
 
   (define (clause->method D motive clause)
     (dict-clear! ih-dict)
-    (let* ([ihs (infer-ihs D motive (clause-args clause))]
+    (let* ([ihs (infer-ihs D motive (clause-args clause) (clause-types clause))]
            [ih-args (dict-map
                      ihs
                      (lambda (k v)
                        (dict-set! ih-dict k (car v))
                        #`(#,(car v) : #,(cdr v))))])
-      #`(lambda* #,@(clause-args clause) #,@ih-args #,(clause-body clause)))))
+      #`(lambda* #,@(clause-decl clause) #,@ih-args #,(clause-body clause)))))
 
 (define-syntax (recur syn)
   (syntax-case syn ()
@@ -165,7 +172,8 @@
     [(_ e clause* ...)
      (let* ([clauses (map clause-parse (syntax->list #'(clause* ...)))]
             [R (infer-result clauses)]
-            [D (type-infer/syn #'e)]
+            [D (or (type-infer/syn #'e)
+                   (raise-syntax-error 'match "Could not infer discrimnant's type." syn))]
 	    [motive #`(lambda (x : #,D) #,R)]
             [U (type-infer/syn R)])
        #`((elim #,D #,U)