Mercurial > urweb

comparison src/elaborate.sml @ 243:2b9dfaffb008

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Transactions and queries, at source level
author Adam Chlipala <adamc@hcoop.net>
date Thu, 28 Aug 2008 14:48:33 -0400
parents 44a1663ad893
children b6b75e6e0898
comparison
equal deleted inserted replaced
242:cc193f680193 243:2b9dfaffb008
1266 Wild 1266 Wild
1267 | None 1267 | None
1268 | Datatype of coverage IM.map 1268 | Datatype of coverage IM.map
1269 | Record of coverage SM.map list 1269 | Record of coverage SM.map list
1270 1270
1271 fun c2s c =
1272 case c of
1273 Wild => "Wild"
1274 | None => "None"
1275 | Datatype _ => "Datatype"
1276 | Record _ => "Record"
1277
1271 fun exhaustive (env, denv, t, ps) = 1278 fun exhaustive (env, denv, t, ps) =
1272 let 1279 let
1273 fun pcCoverage pc = 1280 fun pcCoverage pc =
1274 case pc of 1281 case pc of
1275 L'.PConVar n => n 1282 L'.PConVar n => n
1357 | _ => [Wild]) 1364 | _ => [Wild])
1358 | _ => [Wild] 1365 | _ => [Wild]
1359 end 1366 end
1360 1367
1361 fun coverageImp (c1, c2) = 1368 fun coverageImp (c1, c2) =
1362 case (c1, c2) of 1369 let
1363 (Wild, _) => true 1370 val r =
1364 1371 case (c1, c2) of
1365 | (Datatype cmap1, Datatype cmap2) => 1372 (Wild, _) => true
1366 List.all (fn (n, c2) => 1373
1367 case IM.find (cmap1, n) of 1374 | (Datatype cmap1, Datatype cmap2) =>
1368 NONE => false 1375 List.all (fn (n, c2) =>
1369 | SOME c1 => coverageImp (c1, c2)) (IM.listItemsi cmap2) 1376 case IM.find (cmap1, n) of
1370 1377 NONE => false
1371 | (Record fmaps1, Record fmaps2) => 1378 | SOME c1 => coverageImp (c1, c2)) (IM.listItemsi cmap2)
1372 List.all (fn fmap2 => 1379 | (Datatype cmap1, Wild) =>
1373 List.exists (fn fmap1 => 1380 List.all (fn (n, c1) => coverageImp (c1, Wild)) (IM.listItemsi cmap1)
1374 List.all (fn (x, c2) => 1381
1375 case SM.find (fmap1, x) of 1382 | (Record fmaps1, Record fmaps2) =>
1376 NONE => true 1383 List.all (fn fmap2 =>
1377 | SOME c1 => coverageImp (c1, c2)) 1384 List.exists (fn fmap1 =>
1378 (SM.listItemsi fmap2)) 1385 List.all (fn (x, c2) =>
1379 fmaps1) fmaps2 1386 case SM.find (fmap1, x) of
1380 1387 NONE => true
1381 | _ => false 1388 | SOME c1 => coverageImp (c1, c2))
1389 (SM.listItemsi fmap2))
1390 fmaps1) fmaps2
1391
1392 | (Record fmaps1, Wild) =>
1393 List.exists (fn fmap1 =>
1394 List.all (fn (x, c1) => coverageImp (c1, Wild))
1395 (SM.listItemsi fmap1)) fmaps1
1396
1397 | _ => false
1398 in
1399 (*TextIO.print ("coverageImp(" ^ c2s c1 ^ ", " ^ c2s c2 ^ ") = " ^ Bool.toString r ^ "\n");*)
1400 r
1401 end
1382 1402
1383 fun isTotal (c, t) = 1403 fun isTotal (c, t) =
1384 case c of 1404 case c of
1385 None => (false, []) 1405 None => (false, [])
1386 | Wild => (true, []) 1406 | Wild => (true, [])