Mercurial > urweb
changeset 849:e571fb150a9f
Fix a bug in type class enrichment from substructures
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 16 Jun 2009 14:38:01 -0400 |
| parents | e8594cfa3236 |
| children | 1c2f335297b7 |
| files | src/elab_env.sml src/elab_err.sml src/elaborate.sml src/list_util.sig src/list_util.sml tests/mproj.ur tests/mproj.urp |
| diffstat | 7 files changed, 72 insertions(+), 7 deletions(-) [+] |
line wrap: on
line diff
--- a/src/elab_env.sml Sat Jun 13 15:42:24 2009 -0400 +++ b/src/elab_env.sml Tue Jun 16 14:38:01 2009 -0400 @@ -1070,6 +1070,9 @@ 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 @@ 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,
--- a/src/elab_err.sml Sat Jun 13 15:42:24 2009 -0400 +++ b/src/elab_err.sml Tue Jun 16 14:38:01 2009 -0400 @@ -218,7 +218,7 @@ ("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 @@ 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),
--- a/src/elaborate.sml Sat Jun 13 15:42:24 2009 -0400 +++ b/src/elaborate.sml Tue Jun 16 14:38:01 2009 -0400 @@ -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)]*)
--- a/src/list_util.sig Sat Jun 13 15:42:24 2009 -0400 +++ b/src/list_util.sig Tue Jun 16 14:38:01 2009 -0400 @@ -36,6 +36,8 @@ 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 @@ 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
--- a/src/list_util.sml Sat Jun 13 15:42:24 2009 -0400 +++ b/src/list_util.sml Tue Jun 16 14:38:01 2009 -0400 @@ -123,6 +123,24 @@ 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 @@ 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 =
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/mproj.ur Tue Jun 16 14:38:01 2009 -0400 @@ -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