Mercurial > urweb

comparison src/elaborate.sml @ 216:38b299373676

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Looking up in a type class from a module
author Adam Chlipala <adamc@hcoop.net>
date Sat, 16 Aug 2008 15:58:25 -0400
parents 0343557355fc
children 56db662ebcfd
comparison
equal deleted inserted replaced
215:2f574c07df2e 216:38b299373676
1371 | Record _ => (List.all (fn c2 => coverageImp (c, c2)) (enumerateCases t), []) 1371 | Record _ => (List.all (fn c2 => coverageImp (c, c2)) (enumerateCases t), [])
1372 in 1372 in
1373 isTotal (combinedCoverage ps, t) 1373 isTotal (combinedCoverage ps, t)
1374 end 1374 end
1375 1375
1376 fun normClassConstraint envs c =
1377 let
1378 val ((c, loc), gs1) = hnormCon envs c
1379 in
1380 case c of
1381 L'.CApp (f, x) =>
1382 let
1383 val (f, gs2) = hnormCon envs f
1384 val (x, gs3) = hnormCon envs x
1385 in
1386 ((L'.CApp (f, x), loc), gs1 @ gs2 @ gs3)
1387 end
1388 | _ => ((c, loc), gs1)
1389 end
1390
1376 fun elabExp (env, denv) (eAll as (e, loc)) = 1391 fun elabExp (env, denv) (eAll as (e, loc)) =
1377 let 1392 let
1378 1393
1379 in 1394 in
1380 (*eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)];*) 1395 (*eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)];*)
1428 val (e1', t1, gs2) = elabHead (env, denv) e1' t1 1443 val (e1', t1, gs2) = elabHead (env, denv) e1' t1
1429 val (t1, gs3) = hnormCon (env, denv) t1 1444 val (t1, gs3) = hnormCon (env, denv) t1
1430 in 1445 in
1431 case t1 of 1446 case t1 of
1432 (L'.TFun (dom, ran), _) => 1447 (L'.TFun (dom, ran), _) =>
1433 (case E.resolveClass env dom of 1448 let
1434 NONE => (expError env (Unresolvable (loc, dom)); 1449 val (dom, gs4) = normClassConstraint (env, denv) dom
1435 (eerror, cerror, [])) 1450 in
1436 | SOME pf => ((L'.EApp (e1', pf), loc), ran, gs1 @ gs2 @ gs3)) 1451 case E.resolveClass env dom of
1452 NONE => (expError env (Unresolvable (loc, dom));
1453 (eerror, cerror, []))
1454 | SOME pf => ((L'.EApp (e1', pf), loc), ran, gs1 @ gs2 @ gs3 @ gs4)
1455 end
1437 | _ => (expError env (OutOfContext loc); 1456 | _ => (expError env (OutOfContext loc);
1438 (eerror, cerror, [])) 1457 (eerror, cerror, []))
1439 end 1458 end
1440 | L.EWild => (expError env (OutOfContext loc); 1459 | L.EWild => (expError env (OutOfContext loc);
1441 (eerror, cerror, [])) 1460 (eerror, cerror, []))