diff options
author | Benjamin Barenblat <bbaren@mit.edu> | 2020-05-31 18:29:03 -0400 |
---|---|---|
committer | Benjamin Barenblat <bbaren@mit.edu> | 2020-05-31 18:29:03 -0400 |
commit | 6cc104634ef64be3be88c1fccbe98208d95d8a1a (patch) | |
tree | 9001e5333e808808125978a52669a8bff3639438 /lib/ur/list.ur | |
parent | 82fde07cef0e41b700b9a30137562eb05f2f2c6d (diff) | |
parent | c2f1e1096f602b1cbd4531352f3e1ea6d656a186 (diff) |
Merge branch 'dfsg_clean'
Diffstat (limited to 'lib/ur/list.ur')
-rw-r--r-- | lib/ur/list.ur | 117 |
1 files changed, 116 insertions, 1 deletions
diff --git a/lib/ur/list.ur b/lib/ur/list.ur index cc533676..1eb7626a 100644 --- a/lib/ur/list.ur +++ b/lib/ur/list.ur @@ -31,6 +31,16 @@ fun foldl [a] [b] (f : a -> b -> b) = foldl' end +fun foldli [a] [b] (f : int -> a -> b -> b) = + let + fun foldli' i acc ls = + case ls of + [] => acc + | x :: ls => foldli' (i + 1) (f i x acc) ls + in + foldli' 0 + end + val rev = fn [a] => let fun rev' acc (ls : list a) = @@ -101,6 +111,16 @@ fun mp [a] [b] f = mp' [] end +fun mapConcat [a] [b] f = + let + fun mapConcat' acc ls = + case ls of + [] => rev acc + | x :: ls => mapConcat' (revAppend (f x) acc) ls + in + mapConcat' [] + end + fun mapi [a] [b] f = let fun mp' n acc ls = @@ -153,6 +173,26 @@ fun mapM [m ::: (Type -> Type)] (_ : monad m) [a] [b] f = mapM' [] end +fun mapConcatM [m] (_ : monad m) [a] [b] f = + let + fun mapConcatM' acc ls = + case ls of + [] => return (rev acc) + | x :: ls' => ls <- f x; mapConcatM' (revAppend ls acc) ls' + in + mapConcatM' [] + end + +fun mapMi [m ::: (Type -> Type)] (_ : monad m) [a] [b] f = + let + fun mapM' i acc ls = + case ls of + [] => return (rev acc) + | x :: ls => x' <- f i x; mapM' (i + 1) (x' :: acc) ls + in + mapM' 0 [] + end + fun mapPartialM [m ::: (Type -> Type)] (_ : monad m) [a] [b] f = let fun mapPartialM' acc ls = @@ -204,6 +244,21 @@ fun exists [a] f = ex end +fun existsM [m] (_ : monad m) [a] f = + let + fun ex ls = + case ls of + [] => return False + | x :: ls => + b <- f x; + if b then + return True + else + ex ls + in + ex + end + fun foldlMap [a] [b] [c] f = let fun fold ls' st ls = @@ -240,6 +295,21 @@ fun find [a] f = find' end +fun findM [m] (_ : monad m) [a] f = + let + fun find' ls = + case ls of + [] => return None + | x :: ls => + b <- f x; + if b then + return (Some x) + else + find' ls + in + find' + end + fun search [a] [b] f = let fun search' ls = @@ -253,6 +323,20 @@ fun search [a] [b] f = search' end +fun searchM [m] (_ : monad m) [a] [b] f = + let + fun search' ls = + case ls of + [] => return None + | x :: ls => + o <- f x; + case o of + None => search' ls + | v => return v + in + search' + end + fun foldlM [m] (_ : monad m) [a] [b] f = let fun foldlM' acc ls = @@ -289,7 +373,7 @@ fun filterM [m] (_ : monad m) [a] (p : a -> m bool) = filterM' [] end -fun all [m] f = +fun all [a] f = let fun all' ls = case ls of @@ -299,6 +383,21 @@ fun all [m] f = all' end +fun allM [m] (_ : monad m) [a] f = + let + fun all' ls = + case ls of + [] => return True + | x :: ls => + b <- f x; + if b then + all' ls + else + return False + in + all' + end + fun app [m] (_ : monad m) [a] f = let fun app' ls = @@ -424,6 +523,22 @@ fun assocAdd [a] [b] (_ : eq a) (x : a) (y : b) (ls : t (a * b)) = None => (x, y) :: ls | Some _ => ls +fun assocAddSorted [a] [b] (_ : eq a) (_ : ord a) (x : a) (y : b) (ls : t (a * b)) = + let + fun aas (ls : t (a * b)) (acc : t (a * b)) = + case ls of + [] => rev ((x, y) :: acc) + | (x', y') :: ls' => + if x' = x then + revAppend ((x, y) :: acc) ls' + else if x < x' then + revAppend ((x, y) :: acc) ls + else + aas ls' ((x', y') :: acc) + in + aas ls [] + end + fun recToList [a ::: Type] [r ::: {Unit}] (fl : folder r) = @foldUR [a] [fn _ => list a] (fn [nm ::_] [rest ::_] [[nm] ~ rest] x xs => x :: xs) [] fl |