comparison src/elaborate.sml @ 2087:834b438d57f3

Move code from last changeset, to improve performance
author Adam Chlipala <adam@chlipala.net>
date Fri, 05 Dec 2014 19:41:27 -0500
parents 459ccbf8cd08
children d4eb9b6729f8
comparison
equal deleted inserted replaced
2086:3d22f761a4b7 2087:834b438d57f3
3018 (L'.SgnError, _) => () 3018 (L'.SgnError, _) => ()
3019 | (_, L'.SgnError) => () 3019 | (_, L'.SgnError) => ()
3020 3020
3021 | (L'.SgnConst sgis1, L'.SgnConst sgis2) => 3021 | (L'.SgnConst sgis1, L'.SgnConst sgis2) =>
3022 let 3022 let
3023 (* This reshuffling was added to avoid some unfortunate unification behavior.
3024 * In particular, in sub-signature checking, constraints might be unified,
3025 * even when we don't expect them to be unifiable, deciding on bad values
3026 * for unification variables and dooming later unification.
3027 * By putting all the constraints _last_, we allow all the other unifications
3028 * to happen first, hoping that no unification variables survive to confuse
3029 * constraint unification. *)
3030
3031 val sgis2 =
3032 let
3033 val (constraints, others) = List.partition
3034 (fn (L'.SgiConstraint _, _) => true
3035 | _ => false) sgis2
3036 in
3037 case constraints of
3038 [] => sgis2
3039 | _ => others @ constraints
3040 end
3041
3023 (*val () = prefaces "subSgn" [("sgn1", p_sgn env sgn1), 3042 (*val () = prefaces "subSgn" [("sgn1", p_sgn env sgn1),
3024 ("sgn2", p_sgn env sgn2), 3043 ("sgn2", p_sgn env sgn2),
3025 ("sgis1", p_sgn env (L'.SgnConst sgis1, loc2)), 3044 ("sgis1", p_sgn env (L'.SgnConst sgis1, loc2)),
3026 ("sgis2", p_sgn env (L'.SgnConst sgis2, loc2))]*) 3045 ("sgis2", p_sgn env (L'.SgnConst sgis2, loc2))]*)
3027 3046