annotate variant.urs @ 6:799f43bce62b
Import some code from iwl
| author |
Adam Chlipala <adam@chlipala.net> |
| date |
Tue, 14 Dec 2010 10:33:24 -0500 |
| parents |
|
| children |
296807a9fd50 |
| 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@6
|
13 val testEq : K --> f :: (K -> Type) -> nm :: Name -> t ::: K -> ts ::: {K} -> r ::: {K} -> [[nm] ~ ts] =>
|
|
adam@6
|
14 Eq.eq r ([nm = t] ++ ts)
|
|
adam@6
|
15 -> folder r
|
|
adam@6
|
16 -> variant (map f r) -> option (f t)
|
|
adam@6
|
17
|
|
adam@6
|
18 val eq : r ::: {Unit} -> folder r -> variant (mapU {} r) -> variant (mapU {} r) -> bool
|
|
adam@6
|
19
|
|
adam@6
|
20 val makeEq : K --> f :: (K -> Type) -> nm :: Name -> t ::: K -> ts ::: {K} -> r ::: {K} -> [[nm] ~ ts] =>
|
|
adam@6
|
21 Eq.eq r ([nm = t] ++ ts)
|
|
adam@6
|
22 -> f t
|
|
adam@6
|
23 -> variant (map f r)
|
|
adam@6
|
24
|
|
adam@6
|
25 val fold : r ::: {Unit} -> t ::: Type -> folder r -> (variant (mapU {} r) -> t -> t) -> t -> t
|
|
adam@6
|
26
|
|
adam@6
|
27 val destrR : K --> f :: (K -> Type) -> fr :: (K -> Type) -> t ::: Type
|
|
adam@6
|
28 -> (p :: K -> f p -> fr p -> t)
|
|
adam@6
|
29 -> r ::: {K} -> folder r -> variant (map f r) -> $(map fr r) -> t
|
|
adam@6
|
30
|
|
adam@6
|
31 val destr2R : K --> f1 :: (K -> Type) -> f2 :: (K -> Type) -> fr :: (K -> Type) -> t ::: Type
|
|
adam@6
|
32 -> (p :: K -> f1 p -> f2 p -> fr p -> t)
|
|
adam@6
|
33 -> r ::: {K} -> folder r -> variant (map f1 r) -> variant (map f2 r) -> $(map fr r) -> option t
|
