Mercurial > meta

comparison variant.urs @ 27:ca1c07d49b5e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
comparison
equal deleted inserted replaced
26:c1da0e3749b3 27:ca1c07d49b5e
41 -> r ::: {K} -> folder r -> variant (map f r) -> $(map fr r) -> t 41 -> r ::: {K} -> folder r -> variant (map f r) -> $(map fr r) -> t
42 42
43 val destr2R : K --> f1 :: (K -> Type) -> f2 :: (K -> Type) -> fr :: (K -> Type) -> t ::: Type 43 val destr2R : K --> f1 :: (K -> Type) -> f2 :: (K -> Type) -> fr :: (K -> Type) -> t ::: Type
44 -> (p :: K -> f1 p -> f2 p -> fr p -> t) 44 -> (p :: K -> f1 p -> f2 p -> fr p -> t)
45 -> r ::: {K} -> folder r -> variant (map f1 r) -> variant (map f2 r) -> $(map fr r) -> option t 45 -> r ::: {K} -> folder r -> variant (map f1 r) -> variant (map f2 r) -> $(map fr r) -> option t
46
47 (* Metaprogrammed type-directed case-match.
48
49 This uses a combination of type classes and metaprogramming to make
50 it easy to write case-matches on very large variants with many
51 similar elements. Here's how you use it:
52
53 1. For every type in the variant, write a local typeclass function
54 which reduces it to t, and register as such using the 'declareCase'
55 function in the module you created.
56
57 let val empty = declareCase (fn _ (_ : int) => True)
58
59 These functions also take an initial argument, which has
60 type [a -> variant ts]; e.g. you can use this to create
61 a new copy of the variant with different values!
62 Make sure you specify type signatures on the argument [t]
63 so that we can identify who this typeclass is for. (If you
64 use type classes to construct the return value, you may
65 also need to declare the return type explicitly.)
66
67 2. Do the match using 'typeCase':
68
69 typeCase t
70
71 If you need to override specific constructors, use this idiom:
72
73 @typeCase t (_ ++ {
74 YourConstr = declareCase (fn _ _ => ...)
75 }) _
76
77 How does it work? Very simple: it uses local typeclasses + Ur/Web's
78 support for automatically instantiating records of typeclasses.
79 *)
80
81 class type_case :: {Type} -> Type -> Type -> Type
82 val declareCase : ts ::: {Type} -> t ::: Type -> a ::: Type -> ((a -> variant ts) -> a -> t) -> type_case ts t a
83 val typeCase : ts ::: {Type} -> t ::: Type -> variant ts -> $(map (type_case ts t) ts) -> folder ts -> t