summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-06-06 14:09:30 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-06-06 14:09:30 -0400
commit4d4d6e4aea6565fa167296d16f94f4b768d5414e (patch)
tree1d3da14055d91262a0e36315573406b564790fdc /lib
parenta144d74a7fb416108f643daaa3a734e416683737 (diff)
List library additions; fix another substructure unification bug
Diffstat (limited to 'lib')
-rw-r--r--lib/ur/list.ur28
-rw-r--r--lib/ur/list.urs4
2 files changed, 32 insertions, 0 deletions
diff --git a/lib/ur/list.ur b/lib/ur/list.ur
index 0776ff30..0aae9010 100644
--- a/lib/ur/list.ur
+++ b/lib/ur/list.ur
@@ -122,3 +122,31 @@ fun foldlMap [a] [b] [c] f =
in
fold []
end
+
+fun assoc [a] [b] (_ : eq a) (x : a) =
+ let
+ fun assoc' ls =
+ case ls of
+ [] => None
+ | (y, z) :: ls =>
+ if x = y then
+ Some z
+ else
+ assoc' ls
+ in
+ assoc'
+ end
+
+fun search [a] [b] f =
+ let
+ fun search' ls =
+ case ls of
+ [] => None
+ | x :: ls =>
+ case f x of
+ None => search' ls
+ | v => v
+ in
+ search'
+ end
+
diff --git a/lib/ur/list.urs b/lib/ur/list.urs
index 92589508..1b80a9d3 100644
--- a/lib/ur/list.urs
+++ b/lib/ur/list.urs
@@ -26,3 +26,7 @@ val exists : a ::: Type -> (a -> bool) -> t a -> bool
val foldlMap : a ::: Type -> b ::: Type -> c ::: Type
-> (a -> b -> c * b) -> b -> t a -> t c * b
+
+val assoc : a ::: Type -> b ::: Type -> eq a -> a -> t (a * b) -> option b
+
+val search : a ::: Type -> b ::: Type -> (a -> option b) -> t a -> option b