annotate variant.urs @ 30:4e673b535434

Optimizing JSON generation
author Adam Chlipala <adam@chlipala.net>
date Thu, 04 Dec 2014 19:52:51 -0500
parents ca1c07d49b5e
children
rev   line source
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