diff options
author | Adam Chlipala <adamc@hcoop.net> | 2009-05-26 12:25:06 -0400 |
---|---|---|
committer | Adam Chlipala <adamc@hcoop.net> | 2009-05-26 12:25:06 -0400 |
commit | d8801e05ef2f81f21eb27555b626ee2e52c3365f (patch) | |
tree | 53e0b285bbcb0e28d3cbbd507da21fcc41d8995e /lib/ur/list.ur | |
parent | 5232b7e45cf55208a0a3ea41395bb9f87d06dd21 (diff) |
Chars and more string operations
Diffstat (limited to 'lib/ur/list.ur')
-rw-r--r-- | lib/ur/list.ur | 34 |
1 files changed, 34 insertions, 0 deletions
diff --git a/lib/ur/list.ur b/lib/ur/list.ur index 7079f6bc..7527362d 100644 --- a/lib/ur/list.ur +++ b/lib/ur/list.ur @@ -20,6 +20,18 @@ val rev (a ::: Type) = rev' [] end +val revAppend (a ::: Type) = + let + fun ra (ls : list a) acc = + case ls of + [] => acc + | x :: ls => ra ls (x :: acc) + in + ra + end + +fun append (a ::: Type) (ls1 : t a) (ls2 : t a) = revAppend (rev ls1) ls2 + fun mp (a ::: Type) (b ::: Type) f = let fun mp' acc ls = @@ -30,6 +42,18 @@ fun mp (a ::: Type) (b ::: Type) f = mp' [] end +fun mapPartial (a ::: Type) (b ::: Type) f = + let + fun mp' acc ls = + case ls of + [] => rev acc + | x :: ls => mp' (case f x of + None => acc + | Some y => y :: acc) ls + in + mp' [] + end + fun mapX (a ::: Type) (ctx ::: {Unit}) f = let fun mapX' ls = @@ -49,3 +73,13 @@ fun mapM (m ::: (Type -> Type)) (_ : monad m) (a ::: Type) (b ::: Type) f = in mapM' [] end + +fun filter (a ::: Type) f = + let + fun fil acc ls = + case ls of + [] => rev acc + | x :: ls => fil (if f x then x :: acc else acc) ls + in + fil [] + end |