Mercurial > urweb

annotate lib/ur/list.urs @ 1242:4ed556678214

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
At loop heads, havoc relations that might be changed by the loop
author Adam Chlipala <adamc@hcoop.net>
date Sat, 17 Apr 2010 14:26:52 -0400
parents 61c3139eab12
children 4c367c8f5b2d
rev   line source
adamc@794 1 datatype t = datatype Basis.list
adamc@794 2
adamc@846 3 val show : a ::: Type -> show a -> show (t a)
adamc@846 4 val eq : a ::: Type -> eq a -> eq (t a)
adamc@794 5
adamc@845 6 val foldl : a ::: Type -> b ::: Type -> (a -> b -> b) -> b -> t a -> b
adamc@850 7 val foldlAbort : a ::: Type -> b ::: Type -> (a -> b -> option b) -> b -> t a -> option b
adamc@850 8 val foldlMapAbort : a ::: Type -> b ::: Type -> c ::: Type
adamc@850 9 -> (a -> b -> option (c * b)) -> b -> t a -> option (t c * b)
adamc@845 10
adamc@1057 11 val foldr : a ::: Type -> b ::: Type -> (a -> b -> b) -> b -> t a -> b
adamc@1057 12
adamc@916 13 val length : a ::: Type -> t a -> int
adamc@916 14
adamc@794 15 val rev : a ::: Type -> t a -> t a
adamc@794 16
adamc@821 17 val revAppend : a ::: Type -> t a -> t a -> t a
adamc@821 18
adamc@821 19 val append : a ::: Type -> t a -> t a -> t a
adamc@821 20
adamc@794 21 val mp : a ::: Type -> b ::: Type -> (a -> b) -> t a -> t b
adamc@794 22
adamc@821 23 val mapPartial : a ::: Type -> b ::: Type -> (a -> option b) -> t a -> t b
adamc@821 24
adamc@796 25 val mapX : a ::: Type -> ctx ::: {Unit} -> (a -> xml ctx [] []) -> t a -> xml ctx [] []
adamc@800 26
adamc@800 27 val mapM : m ::: (Type -> Type) -> monad m -> a ::: Type -> b ::: Type
adamc@830 28 -> (a -> m b) -> t a -> m (t b)
adamc@830 29
adamc@1107 30 val mapPartialM : m ::: (Type -> Type) -> monad m -> a ::: Type -> b ::: Type -> (a -> m (option b)) -> t a -> m (t b)
adamc@1107 31
adamc@830 32 val mapXM : m ::: (Type -> Type) -> monad m -> a ::: Type -> ctx ::: {Unit}
adamc@830 33 -> (a -> m (xml ctx [] [])) -> t a -> m (xml ctx [] [])
adamc@821 34
adamc@821 35 val filter : a ::: Type -> (a -> bool) -> t a -> t a
adamc@822 36
adamc@822 37 val exists : a ::: Type -> (a -> bool) -> t a -> bool
adamc@822 38
adamc@840 39 val foldlM : m ::: (Type -> Type) -> monad m -> a ::: Type -> b ::: Type
adamc@840 40 -> (a -> b -> m b) -> b -> t a -> m b
adamc@840 41
adamc@822 42 val foldlMap : a ::: Type -> b ::: Type -> c ::: Type
adamc@822 43 -> (a -> b -> c * b) -> b -> t a -> t c * b
adamc@839 44
adamc@839 45 val search : a ::: Type -> b ::: Type -> (a -> option b) -> t a -> option b
adamc@843 46
adamc@843 47 val all : a ::: Type -> (a -> bool) -> t a -> bool
adamc@844 48
adamc@844 49 val app : m ::: (Type -> Type) -> monad m -> a ::: Type
adamc@844 50 -> (a -> m unit) -> t a -> m unit
adamc@845 51
adamc@908 52 val mapQuery : tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type
adamc@908 53 -> [tables ~ exps] =>
adamc@1191 54 sql_query [] tables exps
adamc@908 55 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables) -> t)
adamc@908 56 -> transaction (list t)
adamc@845 57
adamc@1107 58 val mapQueryM : tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type
adamc@1107 59 -> [tables ~ exps] =>
adamc@1191 60 sql_query [] tables exps
adamc@1107 61 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction t)
adamc@1107 62 -> transaction (list t)
adamc@1107 63
adamc@1107 64 val mapQueryPartialM : tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type
adamc@1107 65 -> [tables ~ exps] =>
adamc@1191 66 sql_query [] tables exps
adamc@1107 67 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction (option t))
adamc@1107 68 -> transaction (list t)
adamc@1107 69
adamc@845 70 (** Association lists *)
adamc@845 71
adamc@845 72 val assoc : a ::: Type -> b ::: Type -> eq a -> a -> t (a * b) -> option b
adamc@845 73
adamc@845 74 val assocAdd : a ::: Type -> b ::: Type -> eq a -> a -> b -> t (a * b) -> t (a * b)