diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2014-12-05 19:41:27 -0500 |
|---|---|---|
| committer | Adam Chlipala <adam@chlipala.net> | 2014-12-05 19:41:27 -0500 |
| commit | e7efbdedad7625a14d9a8b0438ddaf5dea36fc8f (patch) | |
| tree | ccb61a8d0924daad1ac2f13bd19af21d80581c2b | |
| parent | b37758f320183d5d94fc469e66dd288cfb65ca53 (diff) | |
Move code from last changeset, to improve performance
| -rw-r--r-- | src/elab_env.sml | 19 | ||||
| -rw-r--r-- | src/elaborate.sml | 19 |
2 files changed, 20 insertions, 18 deletions
diff --git a/src/elab_env.sml b/src/elab_env.sml index 711db166..9fbe7bd7 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -1114,24 +1114,7 @@ and hnormSgn env (all as (sgn, loc)) = 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 diff --git a/src/elaborate.sml b/src/elaborate.sml index c55dec01..749bd2f1 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -3020,6 +3020,25 @@ and subSgn' counterparts env strLoc sgn1 (sgn2 as (_, loc2)) = | (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)), |