Mercurial > urweb

comparison src/elab_env.sml @ 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 22117edf8fd3
comparison
equal deleted inserted replaced
2086:3d22f761a4b7 2087:834b438d57f3
1112 1112
1113 and hnormSgn env (all as (sgn, loc)) = 1113 and hnormSgn env (all as (sgn, loc)) =
1114 case sgn of 1114 case sgn of
1115 SgnError => all 1115 SgnError => all
1116 | SgnVar n => hnormSgn env (#2 (lookupSgnNamed env n)) 1116 | SgnVar n => hnormSgn env (#2 (lookupSgnNamed env n))
1117 | SgnConst sgis => 1117 | SgnConst _ => all
1118 let
1119 (* This reshuffling was added to avoid some unfortunate unification behavior.
1120 * In particular, in sub-signature checking, constraints might be unified,
1121 * even when we don't expect them to be unifiable, deciding on bad values
1122 * for unification variables and dooming later unification.
1123 * By putting all the constraints _last_, we allow all the other unifications
1124 * to happen first, hoping that no unification variables survive to confuse
1125 * constraint unification. *)
1126
1127 val (constraint, others) = List.partition
1128 (fn (SgiConstraint _, _) => true
1129 | _ => false) sgis
1130 in
1131 case constraint of
1132 [] => all
1133 | _ => (SgnConst (others @ constraint), loc)
1134 end
1135 | SgnFun _ => all 1118 | SgnFun _ => all
1136 | SgnProj (m, ms, x) => 1119 | SgnProj (m, ms, x) =>
1137 let 1120 let
1138 val (_, sgn) = lookupStrNamed env m 1121 val (_, sgn) = lookupStrNamed env m
1139 in 1122 in