|
adam@6
|
1 (** Derived functions dealing with polymorphic variants *)
|
|
adam@6
|
2
|
|
adam@6
|
3 val read : r ::: {Unit} -> t ::: Type -> folder r -> $(mapU t r) -> variant (mapU {} r) -> t
|
|
adam@6
|
4 val write : r ::: {Unit} -> t ::: Type -> folder r -> $(mapU t r) -> variant (mapU {} r) -> t -> $(mapU t r)
|
|
adam@6
|
5
|
|
adam@6
|
6 val search : r ::: {Unit} -> t ::: Type -> (variant (mapU {} r) -> option t) -> folder r -> option t
|
|
adam@6
|
7 val find : r ::: {Unit} -> (variant (mapU {} r) -> bool) -> folder r -> option (variant (mapU {} r))
|
|
adam@6
|
8
|
|
adam@6
|
9 val test : nm :: Name -> t ::: Type -> ts ::: {Type} -> [[nm] ~ ts] => folder ([nm = t] ++ ts)
|
|
adam@6
|
10 -> variant ([nm = t] ++ ts) -> option t
|
|
adam@6
|
11 val testLess : nm :: Name -> t ::: Type -> ts ::: {Type} -> [[nm] ~ ts] => folder ts -> variant ([nm = t] ++ ts) -> option t
|
|
adam@6
|
12
|
|
adam@21
|
13 val weaken : r1 ::: {Type} -> r2 ::: {Type} -> [r1 ~ r2] => folder r1
|
|
adam@21
|
14 -> variant r1 -> variant (r1 ++ r2)
|
|
adam@21
|
15
|
|
adam@6
|
16 val testEq : K --> f :: (K -> Type) -> nm :: Name -> t ::: K -> ts ::: {K} -> r ::: {K} -> [[nm] ~ ts] =>
|
|
adam@6
|
17 Eq.eq r ([nm = t] ++ ts)
|
|
adam@6
|
18 -> folder r
|
|
adam@6
|
19 -> variant (map f r) -> option (f t)
|
|
adam@6
|
20
|
|
adam@6
|
21 val eq : r ::: {Unit} -> folder r -> variant (mapU {} r) -> variant (mapU {} r) -> bool
|
|
adam@6
|
22
|
|
adam@6
|
23 val makeEq : K --> f :: (K -> Type) -> nm :: Name -> t ::: K -> ts ::: {K} -> r ::: {K} -> [[nm] ~ ts] =>
|
|
adam@6
|
24 Eq.eq r ([nm = t] ++ ts)
|
|
adam@6
|
25 -> f t
|
|
adam@6
|
26 -> variant (map f r)
|
|
adam@6
|
27
|
|
adam@21
|
28 val mp : r ::: {Unit} -> t ::: Type -> folder r -> (variant (mapU {} r) -> t) -> $(mapU t r)
|
|
adam@21
|
29
|
|
adam@6
|
30 val fold : r ::: {Unit} -> t ::: Type -> folder r -> (variant (mapU {} r) -> t -> t) -> t -> t
|
|
adam@6
|
31
|
|
adam@20
|
32 val foldR : tr ::: Type -> r ::: {Unit} -> t ::: Type -> folder r -> (variant (mapU {} r) -> tr -> t -> t) -> $(mapU tr r) -> t -> t
|
|
adam@20
|
33
|
|
adam@20
|
34 val appR : m ::: (Type -> Type) -> monad m
|
|
adam@20
|
35 -> tr ::: Type -> r ::: {Unit} -> folder r -> (variant (mapU {} r) -> tr -> m {}) -> $(mapU tr r) -> m {}
|
|
adam@20
|
36
|
|
adam@21
|
37 val mapR : tr ::: Type -> t ::: Type -> r ::: {Unit} -> folder r -> (variant (mapU {} r) -> tr -> t) -> $(mapU tr r) -> $(mapU t r)
|
|
adam@21
|
38
|
|
adam@6
|
39 val destrR : K --> f :: (K -> Type) -> fr :: (K -> Type) -> t ::: Type
|
|
adam@6
|
40 -> (p :: K -> f p -> fr p -> t)
|
|
adam@6
|
41 -> r ::: {K} -> folder r -> variant (map f r) -> $(map fr r) -> t
|
|
adam@6
|
42
|
|
adam@6
|
43 val destr2R : K --> f1 :: (K -> Type) -> f2 :: (K -> Type) -> fr :: (K -> Type) -> t ::: Type
|
|
adam@6
|
44 -> (p :: K -> f1 p -> f2 p -> fr p -> t)
|
|
adam@6
|
45 -> r ::: {K} -> folder r -> variant (map f1 r) -> variant (map f2 r) -> $(map fr r) -> option t
|
|
ezyang@27
|
46
|
|
ezyang@27
|
47 (* Metaprogrammed type-directed case-match.
|
|
ezyang@27
|
48
|
|
ezyang@27
|
49 This uses a combination of type classes and metaprogramming to make
|
|
ezyang@27
|
50 it easy to write case-matches on very large variants with many
|
|
ezyang@27
|
51 similar elements. Here's how you use it:
|
|
ezyang@27
|
52
|
|
ezyang@27
|
53 1. For every type in the variant, write a local typeclass function
|
|
ezyang@27
|
54 which reduces it to t, and register as such using the 'declareCase'
|
|
ezyang@27
|
55 function in the module you created.
|
|
ezyang@27
|
56
|
|
ezyang@27
|
57 let val empty = declareCase (fn _ (_ : int) => True)
|
|
ezyang@27
|
58
|
|
ezyang@27
|
59 These functions also take an initial argument, which has
|
|
ezyang@27
|
60 type [a -> variant ts]; e.g. you can use this to create
|
|
ezyang@27
|
61 a new copy of the variant with different values!
|
|
ezyang@27
|
62 Make sure you specify type signatures on the argument [t]
|
|
ezyang@27
|
63 so that we can identify who this typeclass is for. (If you
|
|
ezyang@27
|
64 use type classes to construct the return value, you may
|
|
ezyang@27
|
65 also need to declare the return type explicitly.)
|
|
ezyang@27
|
66
|
|
ezyang@27
|
67 2. Do the match using 'typeCase':
|
|
ezyang@27
|
68
|
|
ezyang@27
|
69 typeCase t
|
|
ezyang@27
|
70
|
|
ezyang@27
|
71 If you need to override specific constructors, use this idiom:
|
|
ezyang@27
|
72
|
|
ezyang@27
|
73 @typeCase t (_ ++ {
|
|
ezyang@27
|
74 YourConstr = declareCase (fn _ _ => ...)
|
|
ezyang@27
|
75 }) _
|
|
ezyang@27
|
76
|
|
ezyang@27
|
77 How does it work? Very simple: it uses local typeclasses + Ur/Web's
|
|
ezyang@27
|
78 support for automatically instantiating records of typeclasses.
|
|
ezyang@27
|
79 *)
|
|
ezyang@27
|
80
|
|
ezyang@27
|
81 class type_case :: {Type} -> Type -> Type -> Type
|
|
ezyang@27
|
82 val declareCase : ts ::: {Type} -> t ::: Type -> a ::: Type -> ((a -> variant ts) -> a -> t) -> type_case ts t a
|
|
ezyang@27
|
83 val typeCase : ts ::: {Type} -> t ::: Type -> variant ts -> $(map (type_case ts t) ts) -> folder ts -> t
|
