Mercurial > urweb

comparison src/disjoint.sml @ 1034:a779402841f6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Hooks for measuring how much interesting proving is going on in elaboration
author Adam Chlipala <adamc@hcoop.net>
date Tue, 17 Nov 2009 12:44:14 -0500
parents 0406e9cccb72
children
comparison
equal deleted inserted replaced
1033:b734ff578ac7 1034:a779402841f6
159 | _ => 159 | _ =>
160 case PM.find (denv, p1) of 160 case PM.find (denv, p1) of
161 NONE => false 161 NONE => false
162 | SOME pset => PS.member (pset, p2) 162 | SOME pset => PS.member (pset, p2)
163 163
164 val proved = ref 0
165 fun reset () = (ElabOps.reset ();
166 proved := 0)
167
164 fun decomposeRow env c = 168 fun decomposeRow env c =
165 let 169 let
166 val loc = #2 c 170 val loc = #2 c
167 171
168 fun decomposeProj c = 172 fun decomposeProj c =
246 foldl (assertPiece ps1) denv ps2 250 foldl (assertPiece ps1) denv ps2
247 end 251 end
248 252
249 and prove env denv (c1, c2, loc) = 253 and prove env denv (c1, c2, loc) =
250 let 254 let
255 val () = proved := !proved + 1
251 val ps1 = decomposeRow env c1 256 val ps1 = decomposeRow env c1
252 val ps2 = decomposeRow env c2 257 val ps2 = decomposeRow env c2
253 258
254 val hasUnknown = List.exists (fn Unknown _ => true | _ => false) 259 val hasUnknown = List.exists (fn Unknown _ => true | _ => false)
255 val unUnknown = List.mapPartial (fn Unknown _ => NONE | Piece p => SOME p) 260 val unUnknown = List.mapPartial (fn Unknown _ => NONE | Piece p => SOME p)