Mercurial > urweb

comparison src/elab_env.sml @ 2086:3d22f761a4b7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
In checking signature subsumption, be sure to try constraints last.
author Adam Chlipala <adam@chlipala.net>
date Thu, 04 Dec 2014 20:22:39 -0500
parents 403f0cc65b9c
children 834b438d57f3
comparison
equal deleted inserted replaced
2085:fd6d362666c0 2086:3d22f761a4b7
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 _ => all 1117 | SgnConst sgis =>
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
1118 | SgnFun _ => all 1135 | SgnFun _ => all
1119 | SgnProj (m, ms, x) => 1136 | SgnProj (m, ms, x) =>
1120 let 1137 let
1121 val (_, sgn) = lookupStrNamed env m 1138 val (_, sgn) = lookupStrNamed env m
1122 in 1139 in