annotate variant.urs @ 18:6cd839818393

Adjust to name change for [Top.id]
author Adam Chlipala <adam@chlipala.net>
date Thu, 29 Dec 2011 14:15:02 -0500
parents 799f43bce62b
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