From 4dce690086c8d6132c22d5c47a0561a4b1261293 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 16 Jun 2009 14:38:01 -0400 Subject: Fix a bug in type class enrichment from substructures --- src/elab_env.sml | 16 ++++++++++++---- src/elab_err.sml | 4 ++-- src/elaborate.sml | 1 - src/list_util.sig | 3 +++ src/list_util.sml | 31 +++++++++++++++++++++++++++++++ tests/mproj.ur | 21 +++++++++++++++++++++ tests/mproj.urp | 3 +++ 7 files changed, 72 insertions(+), 7 deletions(-) create mode 100644 tests/mproj.ur create mode 100644 tests/mproj.urp diff --git a/src/elab_env.sml b/src/elab_env.sml index 2296d819..c7dfc0b1 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -1070,6 +1070,9 @@ and hnormSgn env (all as (sgn, loc)) = end | _ => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [2]" +fun manifest (m, ms, loc) = + foldl (fn (m, str) => (StrProj (str, m), loc)) (StrVar m, loc) ms + fun enrichClasses env classes (m1, ms) sgn = case #1 (hnormSgn env sgn) of SgnConst sgis => @@ -1089,10 +1092,15 @@ fun enrichClasses env classes (m1, ms) sgn = in case #1 sgi of SgiStr (x, _, sgn) => - (enrichClasses env classes (m1, ms @ [x]) sgn, - newClasses, - sgiSeek (#1 sgi, fmap), - env) + let + val str = manifest (m1, ms, #2 sgi) + val sgn' = sgnSubSgn (str, fmap) sgn + in + (enrichClasses env classes (m1, ms @ [x]) sgn', + newClasses, + sgiSeek (#1 sgi, fmap), + env) + end | SgiSgn (x, n, sgn) => (classes, newClasses, diff --git a/src/elab_err.sml b/src/elab_err.sml index dc34560b..f6fec25b 100644 --- a/src/elab_err.sml +++ b/src/elab_err.sml @@ -218,7 +218,7 @@ fun expError env err = ("Type", p_con env c)]) co) | Unresolvable (loc, c) => (ErrorMsg.errorAt loc "Can't resolve type class instance"; - eprefaces' [("Class constraint", p_con env c)(*, + eprefaces' [("Class constraint", p_con env c), ("Class database", p_list (fn (c, rules) => box [P.p_con env c, PD.string ":", @@ -228,7 +228,7 @@ fun expError env err = PD.string ":", space, P.p_con env c]) rules]) - (E.listClasses env))*)]) + (E.listClasses env))]) | IllegalRec (x, e) => (ErrorMsg.errorAt (#2 e) "Illegal 'val rec' righthand side (must be a function abstraction)"; eprefaces' [("Variable", PD.string x), diff --git a/src/elaborate.sml b/src/elaborate.sml index e78132c4..f0aa8d7a 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -696,7 +696,6 @@ and unifySummaries env (loc, k, s1 : record_summary, s2 : record_summary) = let - val loc = #2 k (*val () = eprefaces "Summaries" [("loc", PD.string (ErrorMsg.spanToString loc)), ("#1", p_summary env s1), ("#2", p_summary env s2)]*) diff --git a/src/list_util.sig b/src/list_util.sig index a89998b2..6e1cd5a5 100644 --- a/src/list_util.sig +++ b/src/list_util.sig @@ -36,6 +36,8 @@ signature LIST_UTIL = sig val foldlMap : ('data1 * 'state -> 'data2 * 'state) -> 'state -> 'data1 list -> 'data2 list * 'state val foldlMapPartial : ('data1 * 'state -> 'data2 option * 'state) -> 'state -> 'data1 list -> 'data2 list * 'state + val foldlMapiPartial : (int * 'data1 * 'state -> 'data2 option * 'state) + -> 'state -> 'data1 list -> 'data2 list * 'state val foldlMapConcat : ('data1 * 'state -> 'data2 list * 'state) -> 'state -> 'data1 list -> 'data2 list * 'state val foldlMapAbort : ('data1 * 'state -> ('data2 * 'state) option) -> 'state -> 'data1 list -> ('data2 list * 'state) option @@ -44,6 +46,7 @@ signature LIST_UTIL = sig val searchi : (int * 'a -> 'b option) -> 'a list -> 'b option val mapi : (int * 'a -> 'b) -> 'a list -> 'b list + val mapiPartial : (int * 'a -> 'b option) -> 'a list -> 'b list val foldli : (int * 'a * 'b -> 'b) -> 'b -> 'a list -> 'b val foldri : (int * 'a * 'b -> 'b) -> 'b -> 'a list -> 'b diff --git a/src/list_util.sml b/src/list_util.sml index 1f6b24ee..03c9549e 100644 --- a/src/list_util.sml +++ b/src/list_util.sml @@ -123,6 +123,24 @@ fun foldlMapPartial f s = fm ([], s) end +fun foldlMapiPartial f s = + let + fun fm (n, ls', s) ls = + case ls of + nil => (rev ls', s) + | h :: t => + let + val (h', s') = f (n, h, s) + val ls' = case h' of + NONE => ls' + | SOME h' => h' :: ls' + in + fm (n + 1, ls', s') t + end + in + fm (0, [], s) + end + fun foldlMapAbort f s = let fun fm (ls', s) ls = @@ -172,6 +190,19 @@ fun mapi f = m 0 [] end +fun mapiPartial f = + let + fun m i acc ls = + case ls of + [] => rev acc + | h :: t => + m (i + 1) (case f (i, h) of + NONE => acc + | SOME v => v :: acc) t + in + m 0 [] + end + fun appi f = let fun m i ls = diff --git a/tests/mproj.ur b/tests/mproj.ur new file mode 100644 index 00000000..8e4317c7 --- /dev/null +++ b/tests/mproj.ur @@ -0,0 +1,21 @@ +structure M : sig + type t + val x : t + + structure S : sig + type u = t + + val eq : eq u + end +end = struct + type t = int + val x = 0 + + structure S = struct + type u = t + + val eq = _ + end +end + +val y = M.x = M.x diff --git a/tests/mproj.urp b/tests/mproj.urp new file mode 100644 index 00000000..d222e3d6 --- /dev/null +++ b/tests/mproj.urp @@ -0,0 +1,3 @@ +debug + +mproj -- cgit v1.2.3