diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2009-06-06 14:09:30 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2009-06-06 14:09:30 -0400 |
| commit | 4d4d6e4aea6565fa167296d16f94f4b768d5414e (patch) | |
| tree | 1d3da14055d91262a0e36315573406b564790fdc /src | |
| parent | a144d74a7fb416108f643daaa3a734e416683737 (diff) | |
List library additions; fix another substructure unification bug
Diffstat (limited to 'src')
| -rw-r--r-- | src/elab_util.sig | 3 | ||||
| -rw-r--r-- | src/elab_util.sml | 7 | ||||
| -rw-r--r-- | src/elaborate.sml | 6 | ||||
| -rw-r--r-- | src/list_util.sig | 1 | ||||
| -rw-r--r-- | src/list_util.sml | 13 |
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 = |