diff src/elaborate.sml @ 1640:dc986eb6113c

Order constructors properly in wildification, to avoid spuriously displeasing the new scoping check
author Adam Chlipala <adam@chlipala.net>
date Sun, 18 Dec 2011 12:00:36 -0500
parents 6c00d8af6239
children 2b7d3d99dc42
line wrap: on
line diff
--- a/src/elaborate.sml	Sun Dec 18 11:29:13 2011 -0500
+++ b/src/elaborate.sml	Sun Dec 18 12:00:36 2011 -0500
@@ -1900,17 +1900,21 @@
         findHead e
     end
 
-datatype needed = Needed of {Cons : L'.kind SM.map,
+datatype needed = Needed of {Cons : (L'.kind * int) SM.map,
+                             NextCon : int,
                              Constraints : (E.env * (L'.con * L'.con) * ErrorMsg.span) list,
                              Vals : SS.set,
                              Mods : (E.env * needed) SM.map}
 
-fun ncons (Needed r) = #Cons r
+fun ncons (Needed r) = map (fn (k, (v, _)) => (k, v))
+                       (ListMergeSort.sort (fn ((_, (_, n1)), (_, (_, n2))) => n1 > n2)
+                                           (SM.listItemsi (#Cons r)))
 fun nconstraints (Needed r) = #Constraints r
 fun nvals (Needed r) = #Vals r
 fun nmods (Needed r) = #Mods r
 
 val nempty = Needed {Cons = SM.empty,
+                     NextCon = 0,
                      Constraints = nil,
                      Vals = SS.empty,
                      Mods = SM.empty}
@@ -1919,7 +1923,8 @@
     let
         val Needed r = r
     in
-        Needed {Cons = SM.insert (#Cons r, k, v),
+        Needed {Cons = SM.insert (#Cons r, k, (v, #NextCon r)),
+                NextCon = #NextCon r + 1,
                 Constraints = #Constraints r,
                 Vals = #Vals r,
                 Mods = #Mods r}
@@ -1930,6 +1935,7 @@
         val Needed r = r
     in
         Needed {Cons = #Cons r,
+                NextCon = #NextCon r,
                 Constraints = v :: #Constraints r,
                 Vals = #Vals r,
                 Mods = #Mods r}
@@ -1940,6 +1946,7 @@
         val Needed r = r
     in
         Needed {Cons = #Cons r,
+                NextCon = #NextCon r,
                 Constraints = #Constraints r,
                 Vals = SS.add (#Vals r, k),
                 Mods = #Mods r}
@@ -1950,6 +1957,7 @@
         val Needed r = r
     in
         Needed {Cons = #Cons r,
+                NextCon = #NextCon r,
                 Constraints = #Constraints r,
                 Vals = #Vals r,
                 Mods = SM.insert (#Mods r, k, v)}
@@ -1960,6 +1968,7 @@
         val Needed r = r
     in
         Needed {Cons = #1 (SM.remove (#Cons r, k)) handle NotFound => #Cons r,
+                NextCon = #NextCon r,
                 Constraints = #Constraints r,
                 Vals = #Vals r,
                 Mods = #Mods r}
@@ -1970,6 +1979,7 @@
         val Needed r = r
     in
         Needed {Cons = #Cons r,
+                NextCon = #NextCon r,
                 Constraints = #Constraints r,
                 Vals = SS.delete (#Vals r, k) handle NotFound => #Vals r,
                 Mods = #Mods r}
@@ -3649,7 +3659,7 @@
                                  end
 
                          val ds' =
-                             case SM.listItemsi (ncons nd) of
+                             case ncons nd of
                                  [] => ds'
                                | xs =>
                                  map (fn (x, k) =>