Mercurial > urweb

changeset 2087:834b438d57f3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Move code from last changeset, to improve performance
author Adam Chlipala <adam@chlipala.net>
date Fri, 05 Dec 2014 19:41:27 -0500
parents 3d22f761a4b7
children 4be82596b8e3
files src/elab_env.sml src/elaborate.sml
diffstat 2 files changed, 20 insertions(+), 18 deletions(-) [+]
line wrap: on
line diff
--- a/src/elab_env.sml	Thu Dec 04 20:22:39 2014 -0500
+++ b/src/elab_env.sml	Fri Dec 05 19:41:27 2014 -0500
@@ -1114,24 +1114,7 @@
     case sgn of
         SgnError => all
       | SgnVar n => hnormSgn env (#2 (lookupSgnNamed env n))
-      | SgnConst sgis =>
-        let
-            (* This reshuffling was added to avoid some unfortunate unification behavior.
-             * In particular, in sub-signature checking, constraints might be unified,
-             * even when we don't expect them to be unifiable, deciding on bad values
-             * for unification variables and dooming later unification.
-             * By putting all the constraints _last_, we allow all the other unifications
-             * to happen first, hoping that no unification variables survive to confuse
-             * constraint unification. *)
-
-            val (constraint, others) = List.partition
-                                           (fn (SgiConstraint _, _) => true
-                                           | _ => false) sgis
-        in
-            case constraint of
-                [] => all
-              | _ => (SgnConst (others @ constraint), loc)
-        end
+      | SgnConst _ => all
       | SgnFun _ => all
       | SgnProj (m, ms, x) =>
         let
--- a/src/elaborate.sml	Thu Dec 04 20:22:39 2014 -0500
+++ b/src/elaborate.sml	Fri Dec 05 19:41:27 2014 -0500
@@ -3020,6 +3020,25 @@
 
       | (L'.SgnConst sgis1, L'.SgnConst sgis2) =>
         let
+            (* This reshuffling was added to avoid some unfortunate unification behavior.
+             * In particular, in sub-signature checking, constraints might be unified,
+             * even when we don't expect them to be unifiable, deciding on bad values
+             * for unification variables and dooming later unification.
+             * By putting all the constraints _last_, we allow all the other unifications
+             * to happen first, hoping that no unification variables survive to confuse
+             * constraint unification. *)
+
+            val sgis2 =
+                let
+                    val (constraints, others) = List.partition
+                                                   (fn (L'.SgiConstraint _, _) => true
+                                                   | _ => false) sgis2
+                in
+                    case constraints of
+                        [] => sgis2
+                      | _ => others @ constraints
+                end
+
             (*val () = prefaces "subSgn" [("sgn1", p_sgn env sgn1),
                                         ("sgn2", p_sgn env sgn2),
                                         ("sgis1", p_sgn env (L'.SgnConst sgis1, loc2)),