Mercurial > meta
diff variant.urs @ 27:ca1c07d49b5e
Type-directed case matching for variants.
author | Edward Z. Yang <ezyang@mit.edu> |
---|---|
date | Thu, 26 Jul 2012 16:39:02 -0400 |
parents | e7d64ea0f922 |
children |
line wrap: on
line diff
--- 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