diff lib/ur/list.ur @ 846:0d30e6338c65

Some standard library reorgs and additions; handle mutual datatypes better in Specialize
author Adam Chlipala <adamc@hcoop.net>
date Tue, 09 Jun 2009 18:11:59 -0400
parents 6725d73c3c31
children 1c2f335297b7
line wrap: on
line diff
--- a/lib/ur/list.ur	Tue Jun 09 11:12:34 2009 -0400
+++ b/lib/ur/list.ur	Tue Jun 09 18:11:59 2009 -0400
@@ -10,6 +10,17 @@
                   mkShow show'
               end
 
+val eq = fn [a] (_ : eq a) =>
+            let
+                fun eq' (ls1 : list a) ls2 =
+                    case (ls1, ls2) of
+                        ([], []) => True
+                      | (x1 :: ls1, x2 :: ls2) => x1 = x2 && eq' ls1 ls2
+                      | _ => False
+            in
+                mkEq eq'
+            end
+
 fun foldl [a] [b] f =
     let
         fun foldl' acc ls =
@@ -20,6 +31,19 @@
         foldl'
     end
 
+fun foldlPartial [a] [b] f =
+    let
+        fun foldlPartial' acc ls =
+            case ls of
+                [] => Some acc
+              | x :: ls =>
+                case f x acc of
+                    None => None
+                  | Some acc' => foldlPartial' acc' ls
+    in
+        foldlPartial'
+    end
+
 val rev = fn [a] =>
              let
                  fun rev' acc (ls : list a) =