From 4d4d6e4aea6565fa167296d16f94f4b768d5414e Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Sat, 6 Jun 2009 14:09:30 -0400
Subject: List library additions; fix another substructure unification bug

---
 lib/ur/list.ur    | 28 ++++++++++++++++++++++++++++
 lib/ur/list.urs   |  4 ++++
 src/elab_util.sig |  3 +++
 src/elab_util.sml |  7 +++++++
 src/elaborate.sml |  6 ++++--
 src/list_util.sig |  1 +
 src/list_util.sml | 13 +++++++++++++
 7 files changed, 60 insertions(+), 2 deletions(-)

diff --git a/lib/ur/list.ur b/lib/ur/list.ur
index 0776ff30..0aae9010 100644
--- a/lib/ur/list.ur
+++ b/lib/ur/list.ur
@@ -122,3 +122,31 @@ fun foldlMap [a] [b] [c] f =
     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 --git a/lib/ur/list.urs b/lib/ur/list.urs
index 92589508..1b80a9d3 100644
--- a/lib/ur/list.urs
+++ b/lib/ur/list.urs
@@ -26,3 +26,7 @@ val exists : a ::: Type -> (a -> bool) -> t a -> bool
 
 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 --git a/src/elab_util.sig b/src/elab_util.sig
index fbe208ad..934779ff 100644
--- a/src/elab_util.sig
+++ b/src/elab_util.sig
@@ -73,6 +73,9 @@ structure Con : sig
                  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 --git a/src/elab_util.sml b/src/elab_util.sml
index 8082cb1e..e7985026 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -280,6 +280,13 @@ fun foldB {kind, con, bind} ctx st c =
         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 --git a/src/elaborate.sml b/src/elaborate.sml
index d60f19f7..92792cd5 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -2637,7 +2637,8 @@ and subSgn' counterparts env sgn1 (sgn2 as (_, loc2)) =
                                                          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 @@ and subSgn' counterparts env sgn1 (sgn2 as (_, loc2)) =
                                                          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 --git a/src/list_util.sig b/src/list_util.sig
index 11af6826..8b6f49d8 100644
--- a/src/list_util.sig
+++ b/src/list_util.sig
@@ -39,6 +39,7 @@ signature LIST_UTIL = sig
     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 --git a/src/list_util.sml b/src/list_util.sml
index a2b6aeb2..bafac51b 100644
--- a/src/list_util.sml
+++ b/src/list_util.sml
@@ -136,6 +136,19 @@ fun search f =
         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 =
-- 
cgit v1.2.3