summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-06-06 14:09:30 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-06-06 14:09:30 -0400
commit4d4d6e4aea6565fa167296d16f94f4b768d5414e (patch)
tree1d3da14055d91262a0e36315573406b564790fdc /src
parenta144d74a7fb416108f643daaa3a734e416683737 (diff)
List library additions; fix another substructure unification bug
Diffstat (limited to 'src')
-rw-r--r--src/elab_util.sig3
-rw-r--r--src/elab_util.sml7
-rw-r--r--src/elaborate.sml6
-rw-r--r--src/list_util.sig1
-rw-r--r--src/list_util.sml13
5 files changed, 28 insertions, 2 deletions
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 =