diff options
| -rw-r--r-- | lib/ur/list.ur | 28 | ||||
| -rw-r--r-- | lib/ur/list.urs | 4 | ||||
| -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 |
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 = |