## 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 |