Mercurial > urweb
changeset 839:b2413e4dd109
List library additions; fix another substructure unification bug
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sat, 06 Jun 2009 14:09:30 -0400 |
| parents | 5154a047c6bc |
| children | e4a02e4fa35c |
| files | lib/ur/list.ur lib/ur/list.urs src/elab_util.sig src/elab_util.sml src/elaborate.sml src/list_util.sig src/list_util.sml |
| diffstat | 7 files changed, 60 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- 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 +
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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 =