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 (2009-06-16)
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
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/mproj.urp	Tue Jun 16 14:38:01 2009 -0400
@@ -0,0 +1,3 @@
+debug
+
+mproj