From 4c8297c1f381599333e998da585f4ef5ac24383b Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Tue, 9 Jun 2009 11:12:34 -0400
Subject: Mark current as effectful; add List functions

---
 lib/ur/list.ur | 43 +++++++++++++++++++++++++++++--------------
 1 file changed, 29 insertions(+), 14 deletions(-)

(limited to 'lib/ur/list.ur')

diff --git a/lib/ur/list.ur b/lib/ur/list.ur
index 60cd7316..2e62facb 100644
--- a/lib/ur/list.ur
+++ b/lib/ur/list.ur
@@ -10,6 +10,16 @@ val show = fn [a] (_ : show a) =>
                   mkShow show'
               end
 
+fun foldl [a] [b] f =
+    let
+        fun foldl' acc ls =
+            case ls of
+                [] => acc
+              | x :: ls => foldl' (f x acc) ls
+    in
+        foldl'
+    end
+
 val rev = fn [a] =>
              let
                  fun rev' acc (ls : list a) =
@@ -123,20 +133,6 @@ fun foldlMap [a] [b] [c] f =
         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 =
@@ -183,3 +179,22 @@ fun app [m] (_ : monad m) [a] f =
     in
         app'
     end
+
+fun assoc [a] [b] (_ : eq a) (x : a) =
+    let
+        fun assoc' (ls : list (a * b)) =
+            case ls of
+                [] => None
+              | (y, z) :: ls =>
+                if x = y then
+                    Some z
+                else
+                    assoc' ls
+    in
+        assoc'
+    end
+
+fun assocAdd [a] [b] (_ : eq a) (x : a) (y : b) (ls : t (a * b)) =
+    case assoc x ls of
+        None => (x, y) :: ls
+      | Some _ => ls
-- 
cgit v1.2.3