# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1244311770 14400
# Node ID b2413e4dd1098021e3d5ac125aea762d4f0054f4
# Parent  5154a047c6bcdb25fb92adf4aebe9fd7e3ffb51f
List library additions; fix another substructure unification bug

diff -r 5154a047c6bc -r b2413e4dd109 lib/ur/list.ur
--- a/lib/ur/list.ur	Tue Jun 02 19:28:25 2009 -0400
+++ b/lib/ur/list.ur	Sat Jun 06 14:09:30 2009 -0400
@@ -122,3 +122,31 @@
     in
         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 =
+            case ls of
+                [] => None
+              | x :: ls =>
+                case f x of
+                    None => search' ls
+                  | v => v
+    in
+        search'
+    end
+
diff -r 5154a047c6bc -r b2413e4dd109 lib/ur/list.urs
--- a/lib/ur/list.urs	Tue Jun 02 19:28:25 2009 -0400
+++ b/lib/ur/list.urs	Sat Jun 06 14:09:30 2009 -0400
@@ -26,3 +26,7 @@
 
 val foldlMap : a ::: Type -> b ::: Type -> c ::: Type
                -> (a -> b -> c * b) -> b -> t a -> t c * b
+
+val assoc : a ::: Type -> b ::: Type -> eq a -> a -> t (a * b) -> option b
+
+val search : a ::: Type -> b ::: Type -> (a -> option b) -> t a -> option b
diff -r 5154a047c6bc -r b2413e4dd109 src/elab_util.sig
--- a/src/elab_util.sig	Tue Jun 02 19:28:25 2009 -0400
+++ b/src/elab_util.sig	Sat Jun 06 14:09:30 2009 -0400
@@ -73,6 +73,9 @@
                  con : 'context * Elab.con' * 'state -> 'state,
                  bind : 'context * binder -> 'context}
                 -> 'context -> 'state -> Elab.con -> 'state
+    val fold : {kind : Elab.kind' * 'state -> 'state,
+                 con : Elab.con' * 'state -> 'state}
+                -> 'state -> Elab.con -> 'state
 end
 
 structure Exp : sig
diff -r 5154a047c6bc -r b2413e4dd109 src/elab_util.sml
--- a/src/elab_util.sml	Tue Jun 02 19:28:25 2009 -0400
+++ b/src/elab_util.sml	Sat Jun 06 14:09:30 2009 -0400
@@ -280,6 +280,13 @@
         S.Continue (_, st) => st
       | S.Return _ => raise Fail "ElabUtil.Con.foldB: Impossible"
 
+fun fold {kind, con} st c =
+    case mapfoldB {kind = fn () => fn k => fn st => S.Continue (k, kind (k, st)),
+                   con = fn () => fn c => fn st => S.Continue (c, con (c, st)),
+                   bind = fn ((), _) => ()} () c st of
+        S.Continue (_, st) => st
+      | S.Return _ => raise Fail "ElabUtil.Con.fold: Impossible"
+
 end
 
 structure Exp = struct
diff -r 5154a047c6bc -r b2413e4dd109 src/elaborate.sml
--- a/src/elaborate.sml	Tue Jun 02 19:28:25 2009 -0400
+++ b/src/elaborate.sml	Sat Jun 06 14:09:30 2009 -0400
@@ -2637,7 +2637,8 @@
                                                          val env = if n1 = n2 then
                                                                        env
                                                                    else
-                                                                       E.pushCNamedAs env x n1 k1 (SOME c1)
+                                                                       (cparts (n2, n1);
+                                                                        E.pushCNamedAs env x n1 k1 (SOME c1))
                                                      in
                                                          SOME env
                                                      end
@@ -2894,7 +2895,8 @@
                                                          val env = if n1 = n2 then
                                                                        env
                                                                    else
-                                                                       E.pushCNamedAs env x n1 k2 (SOME c1)
+                                                                       (cparts (n2, n1);
+                                                                        E.pushCNamedAs env x n1 k2 (SOME c1))
                                                      in
                                                          SOME env
                                                      end
diff -r 5154a047c6bc -r b2413e4dd109 src/list_util.sig
--- a/src/list_util.sig	Tue Jun 02 19:28:25 2009 -0400
+++ b/src/list_util.sig	Sat Jun 06 14:09:30 2009 -0400
@@ -39,6 +39,7 @@
     val foldlMapConcat : ('data1 * 'state -> 'data2 list * 'state) -> 'state -> 'data1 list -> 'data2 list * 'state
 
     val search : ('a -> 'b option) -> 'a list -> 'b option
+    val searchi : (int * 'a -> 'b option) -> 'a list -> 'b option
 
     val mapi : (int * 'a -> 'b) -> 'a list -> 'b list
     val foldli : (int * 'a * 'b -> 'b) -> 'b -> 'a list -> 'b
diff -r 5154a047c6bc -r b2413e4dd109 src/list_util.sml
--- a/src/list_util.sml	Tue Jun 02 19:28:25 2009 -0400
+++ b/src/list_util.sml	Sat Jun 06 14:09:30 2009 -0400
@@ -136,6 +136,19 @@
         s
     end
 
+fun searchi f =
+    let
+        fun s n ls =
+            case ls of
+                [] => NONE
+              | h :: t =>
+                case f (n, h) of
+                    NONE => s (n + 1) t
+                  | v => v
+    in
+        s 0
+    end
+
 fun mapi f =
     let
         fun m i acc ls =