From b7de8e9ac590f9d06df72d22489375b33a6efef9 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Tue, 9 Jun 2009 18:11:59 -0400
Subject: Some standard library reorgs and additions; handle mutual datatypes
 better in Specialize

---
 lib/ur/basis.urs    |  1 -
 lib/ur/list.ur      | 24 ++++++++++++++++++++++++
 lib/ur/list.urs     |  4 +++-
 lib/ur/listPair.ur  | 14 ++++++++++++++
 lib/ur/listPair.urs |  3 +++
 lib/ur/option.ur    | 12 ++++++++++++
 lib/ur/option.urs   |  3 +++
 7 files changed, 59 insertions(+), 2 deletions(-)

(limited to 'lib')

diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index c5c4f6f2..50909804 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -25,7 +25,6 @@ val eq_string : eq string
 val eq_char : eq char
 val eq_bool : eq bool
 val eq_time : eq time
-val eq_option : t ::: Type -> eq t -> eq (option t)
 val mkEq : t ::: Type -> (t -> t -> bool) -> eq t
 
 class num
diff --git a/lib/ur/list.ur b/lib/ur/list.ur
index 2e62facb..b99ef515 100644
--- a/lib/ur/list.ur
+++ b/lib/ur/list.ur
@@ -10,6 +10,17 @@ val show = fn [a] (_ : show a) =>
                   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 @@ fun foldl [a] [b] f =
         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) =
diff --git a/lib/ur/list.urs b/lib/ur/list.urs
index daf81074..f5495d41 100644
--- a/lib/ur/list.urs
+++ b/lib/ur/list.urs
@@ -1,8 +1,10 @@
 datatype t = datatype Basis.list
 
-val show : a ::: Type -> show a -> show (list a)
+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 rev : a ::: Type -> t a -> t a
 
diff --git a/lib/ur/listPair.ur b/lib/ur/listPair.ur
index 8d1c873e..745e436c 100644
--- a/lib/ur/listPair.ur
+++ b/lib/ur/listPair.ur
@@ -1,3 +1,17 @@
+fun foldlPartial [a] [b] [c] f =
+    let
+        fun foldlPartial' 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)
+              | _ => None
+    in
+        foldlPartial'
+    end
+
 fun mapX [a] [b] [ctx ::: {Unit}] f =
     let
         fun mapX' ls1 ls2 =
diff --git a/lib/ur/listPair.urs b/lib/ur/listPair.urs
index 0c5e5443..310a1a4e 100644
--- a/lib/ur/listPair.urs
+++ b/lib/ur/listPair.urs
@@ -1,3 +1,6 @@
+val foldlPartial : 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 [] []
 
diff --git a/lib/ur/option.ur b/lib/ur/option.ur
index 5ec093c0..1f044002 100644
--- a/lib/ur/option.ur
+++ b/lib/ur/option.ur
@@ -1,5 +1,12 @@
 datatype t = datatype Basis.option
 
+fun eq [a] (_ : eq a) =
+    mkEq (fn x y =>
+             case (x, y) of
+                 (None, None) => True
+               | (Some x, Some y) => x = y
+               | _ => False)
+
 fun isSome [a] x =
     case x of
         None => False
@@ -9,3 +16,8 @@ fun mp [a] [b] f x =
     case x of
         None => None
       | Some y => Some (f y)
+
+fun bind [a] [b] f x =
+    case x of
+        None => None
+      | Some y => f y
diff --git a/lib/ur/option.urs b/lib/ur/option.urs
index ced6156e..984bc681 100644
--- a/lib/ur/option.urs
+++ b/lib/ur/option.urs
@@ -1,5 +1,8 @@
 datatype t = datatype Basis.option
 
+val eq : a ::: Type -> eq a -> eq (t a)
+
 val isSome : a ::: Type -> t a -> bool
 
 val mp : a ::: Type -> b ::: Type -> (a -> b) -> t a -> t b
+val bind : a ::: Type -> b ::: Type -> (a -> option b) -> t a -> t b
-- 
cgit v1.2.3