# HG changeset patch
# User Edward Z. Yang <ezyang@mit.edu>
# Date 1343335142 14400
# Node ID ca1c07d49b5e6746036edcc6ff9c62b7d335abd9
# Parent  c1da0e3749b351fc75dba5c699dc075ecebf3ae7
Type-directed case matching for variants.

diff -r c1da0e3749b3 -r ca1c07d49b5e variant.ur
--- a/variant.ur	Sun May 13 14:13:18 2012 -0400
+++ b/variant.ur	Thu Jul 26 16:39:02 2012 -0400
@@ -127,3 +127,19 @@
 fun makeEq [K] [f :: K -> Type] [nm :: Name] [t ::: K] [ts ::: {K}] [r ::: {K}] [[nm] ~ ts]
     (pf : Eq.eq r ([nm = t] ++ ts)) (x : f t) : variant (map f r) =
   Eq.cast (Eq.sym pf) [fn r => variant (map f r)] (make [nm] x)
+
+con variantMake ts' ts = $(map (fn t => t -> variant ts') ts)
+con mkLabelsAccum r = s :: {Type} -> [r ~ s] => variantMake (r ++ s) r
+fun mkLabels [ts ::: {Type}] (fl : folder ts) : variantMake ts ts
+  = @Top.fold [mkLabelsAccum]
+          (fn [nm::_] [v::_] [r::_] [[nm] ~ r]
+              (k : mkLabelsAccum r)
+              [s::_] [[nm = v] ++ r ~ s] => k [[nm = v] ++ s] ++ {nm = make [nm]})
+          (fn [s::_] [[] ~ s] => {}) fl [[]] !
+
+class type_case = fn ts t a => (a -> variant ts) -> a -> t
+
+fun declareCase [ts] [t] [a] (f : (a -> variant ts) -> a -> t) : type_case ts t a = f
+fun typeCase [ts] [t] (v : variant ts) (dstrs : $(map (type_case ts t) ts)) (fl : folder ts) : t
+(* Ur/Web not clever enough to calculate these folders, it seems *)
+  = match v (@ap [fn a => a -> variant ts] [fn a => a -> t] fl dstrs (@mkLabels fl))
diff -r c1da0e3749b3 -r ca1c07d49b5e variant.urs
--- a/variant.urs	Sun May 13 14:13:18 2012 -0400
+++ b/variant.urs	Thu Jul 26 16:39:02 2012 -0400
@@ -43,3 +43,41 @@
 val destr2R : K --> f1 :: (K -> Type) -> f2 :: (K -> Type) -> fr :: (K -> Type) -> t ::: Type
              -> (p :: K -> f1 p -> f2 p -> fr p -> t)
              -> r ::: {K} -> folder r -> variant (map f1 r) -> variant (map f2 r) -> $(map fr r) -> option t
+
+(* Metaprogrammed type-directed case-match.
+
+This uses a combination of type classes and metaprogramming to make
+it easy to write case-matches on very large variants with many
+similar elements.  Here's how you use it:
+
+    1. For every type in the variant, write a local typeclass function
+       which reduces it to t, and register as such using the 'declareCase'
+       function in the module you created.
+
+            let val empty = declareCase (fn _ (_ : int) => True)
+
+       These functions also take an initial argument, which has
+       type [a -> variant ts]; e.g. you can use this to create
+       a new copy of the variant with different values!
+       Make sure you specify type signatures on the argument [t]
+       so that we can identify who this typeclass is for.  (If you
+       use type classes to construct the return value, you may
+       also need to declare the return type explicitly.)
+
+    2. Do the match using 'typeCase':
+
+            typeCase t
+
+       If you need to override specific constructors, use this idiom:
+
+            @typeCase t (_ ++ {
+                YourConstr = declareCase (fn _ _ => ...)
+            }) _
+
+How does it work?  Very simple: it uses local typeclasses + Ur/Web's
+support for automatically instantiating records of typeclasses.
+*)
+
+class type_case :: {Type} -> Type -> Type -> Type
+val declareCase : ts ::: {Type} -> t ::: Type -> a ::: Type -> ((a -> variant ts) -> a -> t) -> type_case ts t a
+val typeCase : ts ::: {Type} -> t ::: Type -> variant ts -> $(map (type_case ts t) ts) -> folder ts -> t