Mercurial > urweb

comparison src/disjoint.sml @ 83:0a1baddd8ab2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Threading disjointness conditions through Elaborate
author Adam Chlipala <adamc@hcoop.net>
date Tue, 01 Jul 2008 11:39:14 -0400
parents b4f2a258e52c
children e86370850c30
comparison
equal deleted inserted replaced
82:b4f2a258e52c 83:0a1baddd8ab2
275 val ps2 = decomposeRow env c2 275 val ps2 = decomposeRow env c2
276 276
277 val hasUnknown = List.exists (fn p => p = Unknown) 277 val hasUnknown = List.exists (fn p => p = Unknown)
278 in 278 in
279 if hasUnknown ps1 orelse hasUnknown ps2 then 279 if hasUnknown ps1 orelse hasUnknown ps2 then
280 (ErrorMsg.errorAt loc "Structure of row is too complicated to prove disjointness"; 280 [(c1, c2)]
281 Print.eprefaces' [("Row 1", ElabPrint.p_con env c1),
282 ("Row 2", ElabPrint.p_con env c2)];
283 [])
284 else 281 else
285 foldl (fn (p1, rem) => 282 foldl (fn (p1, rem) =>
286 foldl (fn (p2, rem) => 283 foldl (fn (p2, rem) =>
287 if prove1 denv (p1, p2) then 284 if prove1 denv (p1, p2) then
288 rem 285 rem