diff lib/ur/list.ur @ 821:395a5d450cc0

Chars and more string operations
author Adam Chlipala <adamc@hcoop.net>
date Tue, 26 May 2009 12:25:06 -0400
parents 066493f7f008
children d4e811beb8eb
line wrap: on
line diff
--- a/lib/ur/list.ur	Sat May 23 10:14:51 2009 -0400
+++ b/lib/ur/list.ur	Tue May 26 12:25:06 2009 -0400
@@ -20,6 +20,18 @@
         rev' []
     end
 
+val revAppend (a ::: Type) =
+    let
+        fun ra (ls : list a) acc =
+            case ls of
+                [] => acc
+              | x :: ls => ra ls (x :: acc)
+    in
+        ra
+    end
+
+fun append (a ::: Type) (ls1 : t a) (ls2 : t a) = revAppend (rev ls1) ls2                
+
 fun mp (a ::: Type) (b ::: Type) f =
     let
         fun mp' acc ls =
@@ -30,6 +42,18 @@
         mp' []
     end
 
+fun mapPartial (a ::: Type) (b ::: Type) f =
+    let
+        fun mp' acc ls =
+            case ls of
+                [] => rev acc
+              | x :: ls => mp' (case f x of
+                                    None => acc
+                                  | Some y => y :: acc) ls
+    in
+        mp' []
+    end
+
 fun mapX (a ::: Type) (ctx ::: {Unit}) f =
     let
         fun mapX' ls =
@@ -49,3 +73,13 @@
     in
         mapM' []
     end
+
+fun filter (a ::: Type) f =
+    let
+        fun fil acc ls =
+            case ls of
+                [] => rev acc
+              | x :: ls => fil (if f x then x :: acc else acc) ls
+    in
+        fil []
+    end