summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-06-16 14:38:01 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-06-16 14:38:01 -0400
commit4dce690086c8d6132c22d5c47a0561a4b1261293 (patch)
tree58dd4551f8c5d971e12e1c704f7abd9d90f3373e /src
parentc23f27988ff76b4923a63ced2452c4fd7787a745 (diff)
Fix a bug in type class enrichment from substructures
Diffstat (limited to 'src')
-rw-r--r--src/elab_env.sml16
-rw-r--r--src/elab_err.sml4
-rw-r--r--src/elaborate.sml1
-rw-r--r--src/list_util.sig3
-rw-r--r--src/list_util.sml31
5 files changed, 48 insertions, 7 deletions
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 =