aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/ur
diff options
context:
space:
mode:
Diffstat (limited to 'lib/ur')
-rw-r--r--lib/ur/list.ur21
-rw-r--r--lib/ur/list.urs4
-rw-r--r--lib/ur/listPair.ur8
-rw-r--r--lib/ur/listPair.urs4
4 files changed, 26 insertions, 11 deletions
diff --git a/lib/ur/list.ur b/lib/ur/list.ur
index b99ef515..d774cc54 100644
--- a/lib/ur/list.ur
+++ b/lib/ur/list.ur
@@ -31,17 +31,17 @@ fun foldl [a] [b] f =
foldl'
end
-fun foldlPartial [a] [b] f =
+fun foldlAbort [a] [b] f =
let
- fun foldlPartial' acc ls =
+ fun foldlAbort' acc ls =
case ls of
[] => Some acc
| x :: ls =>
case f x acc of
None => None
- | Some acc' => foldlPartial' acc' ls
+ | Some acc' => foldlAbort' acc' ls
in
- foldlPartial'
+ foldlAbort'
end
val rev = fn [a] =>
@@ -54,6 +54,19 @@ val rev = fn [a] =>
rev' []
end
+fun foldlMapAbort [a] [b] [c] f =
+ let
+ fun foldlMapAbort' ls' acc ls =
+ case ls of
+ [] => Some (rev ls', acc)
+ | x :: ls =>
+ case f x acc of
+ None => None
+ | Some (x', acc') => foldlMapAbort' (x' :: ls') acc' ls
+ in
+ foldlMapAbort' []
+ end
+
val revAppend = fn [a] =>
let
fun ra (ls : list a) acc =
diff --git a/lib/ur/list.urs b/lib/ur/list.urs
index f5495d41..1b0fced9 100644
--- a/lib/ur/list.urs
+++ b/lib/ur/list.urs
@@ -4,7 +4,9 @@ val show : a ::: Type -> show a -> show (t a)
val eq : a ::: Type -> eq a -> eq (t a)
val foldl : a ::: Type -> b ::: Type -> (a -> b -> b) -> b -> t a -> b
-val foldlPartial : a ::: Type -> b ::: Type -> (a -> b -> option b) -> b -> t a -> option b
+val foldlAbort : a ::: Type -> b ::: Type -> (a -> b -> option b) -> b -> t a -> option b
+val foldlMapAbort : a ::: Type -> b ::: Type -> c ::: Type
+ -> (a -> b -> option (c * b)) -> b -> t a -> option (t c * b)
val rev : a ::: Type -> t a -> t a
diff --git a/lib/ur/listPair.ur b/lib/ur/listPair.ur
index 745e436c..0182af19 100644
--- a/lib/ur/listPair.ur
+++ b/lib/ur/listPair.ur
@@ -1,15 +1,15 @@
-fun foldlPartial [a] [b] [c] f =
+fun foldlAbort [a] [b] [c] f =
let
- fun foldlPartial' acc ls1 ls2 =
+ fun foldlAbort' acc ls1 ls2 =
case (ls1, ls2) of
([], []) => Some acc
| (x1 :: ls1, x2 :: ls2) =>
(case f x1 x2 acc of
None => None
- | Some acc' => foldlPartial' acc' ls1 ls2)
+ | Some acc' => foldlAbort' acc' ls1 ls2)
| _ => None
in
- foldlPartial'
+ foldlAbort'
end
fun mapX [a] [b] [ctx ::: {Unit}] f =
diff --git a/lib/ur/listPair.urs b/lib/ur/listPair.urs
index 310a1a4e..f2287c13 100644
--- a/lib/ur/listPair.urs
+++ b/lib/ur/listPair.urs
@@ -1,5 +1,5 @@
-val foldlPartial : a ::: Type -> b ::: Type -> c ::: Type
- -> (a -> b -> c -> option c) -> c -> list a -> list b -> option c
+val foldlAbort : a ::: Type -> b ::: Type -> c ::: Type
+ -> (a -> b -> c -> option c) -> c -> list a -> list b -> option c
val mapX : a ::: Type -> b ::: Type -> ctx ::: {Unit}
-> (a -> b -> xml ctx [] []) -> list a -> list b -> xml ctx [] []