Ur/Web Metaprogramming Library

view variant.urs @ 28:f55f66c6fdee

Migrate ap method to Record module.
author Edward Z. Yang <ezyang@mit.edu>
date Thu Jul 26 16:48:37 2012 -0400 (21 months ago)
parents e7d64ea0f922
children
line source
1 (** Derived functions dealing with polymorphic variants *)
3 val read : r ::: {Unit} -> t ::: Type -> folder r -> $(mapU t r) -> variant (mapU {} r) -> t
4 val write : r ::: {Unit} -> t ::: Type -> folder r -> $(mapU t r) -> variant (mapU {} r) -> t -> $(mapU t r)
6 val search : r ::: {Unit} -> t ::: Type -> (variant (mapU {} r) -> option t) -> folder r -> option t
7 val find : r ::: {Unit} -> (variant (mapU {} r) -> bool) -> folder r -> option (variant (mapU {} r))
9 val test : nm :: Name -> t ::: Type -> ts ::: {Type} -> [[nm] ~ ts] => folder ([nm = t] ++ ts)
10 -> variant ([nm = t] ++ ts) -> option t
11 val testLess : nm :: Name -> t ::: Type -> ts ::: {Type} -> [[nm] ~ ts] => folder ts -> variant ([nm = t] ++ ts) -> option t
13 val weaken : r1 ::: {Type} -> r2 ::: {Type} -> [r1 ~ r2] => folder r1
14 -> variant r1 -> variant (r1 ++ r2)
16 val testEq : K --> f :: (K -> Type) -> nm :: Name -> t ::: K -> ts ::: {K} -> r ::: {K} -> [[nm] ~ ts] =>
17 Eq.eq r ([nm = t] ++ ts)
18 -> folder r
19 -> variant (map f r) -> option (f t)
21 val eq : r ::: {Unit} -> folder r -> variant (mapU {} r) -> variant (mapU {} r) -> bool
23 val makeEq : K --> f :: (K -> Type) -> nm :: Name -> t ::: K -> ts ::: {K} -> r ::: {K} -> [[nm] ~ ts] =>
24 Eq.eq r ([nm = t] ++ ts)
25 -> f t
26 -> variant (map f r)
28 val mp : r ::: {Unit} -> t ::: Type -> folder r -> (variant (mapU {} r) -> t) -> $(mapU t r)
30 val fold : r ::: {Unit} -> t ::: Type -> folder r -> (variant (mapU {} r) -> t -> t) -> t -> t
32 val foldR : tr ::: Type -> r ::: {Unit} -> t ::: Type -> folder r -> (variant (mapU {} r) -> tr -> t -> t) -> $(mapU tr r) -> t -> t
34 val appR : m ::: (Type -> Type) -> monad m
35 -> tr ::: Type -> r ::: {Unit} -> folder r -> (variant (mapU {} r) -> tr -> m {}) -> $(mapU tr r) -> m {}
37 val mapR : tr ::: Type -> t ::: Type -> r ::: {Unit} -> folder r -> (variant (mapU {} r) -> tr -> t) -> $(mapU tr r) -> $(mapU t r)
39 val destrR : K --> f :: (K -> Type) -> fr :: (K -> Type) -> t ::: Type
40 -> (p :: K -> f p -> fr p -> t)
41 -> r ::: {K} -> folder r -> variant (map f r) -> $(map fr r) -> t
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)
45 -> r ::: {K} -> folder r -> variant (map f1 r) -> variant (map f2 r) -> $(map fr r) -> option t
47 (* Metaprogrammed type-directed case-match.
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:
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.
57 let val empty = declareCase (fn _ (_ : int) => True)
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.)
67 2. Do the match using 'typeCase':
69 typeCase t
71 If you need to override specific constructors, use this idiom:
73 @typeCase t (_ ++ {
74 YourConstr = declareCase (fn _ _ => ...)
75 }) _
77 How does it work? Very simple: it uses local typeclasses + Ur/Web's
78 support for automatically instantiating records of typeclasses.
79 *)
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