Mercurial > urweb

comparison src/elaborate.sml @ 217:56db662ebcfd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fun with type classes and modules
author Adam Chlipala <adamc@hcoop.net>
date Sat, 16 Aug 2008 16:30:07 -0400
parents 38b299373676
children a3413288cce1
comparison
equal deleted inserted replaced
216:38b299373676 217:56db662ebcfd
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 = 1376 fun unmodCon env (c, loc) =
1377 let 1377 case c of
1378 val ((c, loc), gs1) = hnormCon envs c 1378 L'.CNamed n =>
1379 in 1379 (case E.lookupCNamed env n of
1380 case c of 1380 (_, _, SOME (c as (L'.CModProj _, _))) => unmodCon env c
1381 L'.CApp (f, x) => 1381 | _ => (c, loc))
1382 let 1382 | L'.CModProj (m1, ms, x) =>
1383 val (f, gs2) = hnormCon envs f 1383 let
1384 val (x, gs3) = hnormCon envs x 1384 val (str, sgn) = E.chaseMpath env (m1, ms)
1385 in 1385 in
1386 ((L'.CApp (f, x), loc), gs1 @ gs2 @ gs3) 1386 case E.projectCon env {str = str, sgn = sgn, field = x} of
1387 end 1387 NONE => raise Fail "unmodCon: Can't projectCon"
1388 | _ => ((c, loc), gs1) 1388 | SOME (_, SOME (c as (L'.CModProj _, _))) => unmodCon env c
1389 end 1389 | _ => (c, loc)
1390 end
1391 | _ => (c, loc)
1392
1393 fun normClassConstraint envs (c, loc) =
1394 case c of
1395 L'.CApp (f, x) =>
1396 let
1397 val f = unmodCon (#1 envs) f
1398 val (x, gs) = hnormCon envs x
1399 in
1400 ((L'.CApp (f, x), loc), gs)
1401 end
1402 | _ => ((c, loc), [])
1390 1403
1391 fun elabExp (env, denv) (eAll as (e, loc)) = 1404 fun elabExp (env, denv) (eAll as (e, loc)) =
1392 let 1405 let
1393 1406
1394 in 1407 in
2726 val (c', _, gs1) = case co of 2739 val (c', _, gs1) = case co of
2727 NONE => (cunif (loc, ktype), ktype, []) 2740 NONE => (cunif (loc, ktype), ktype, [])
2728 | SOME c => elabCon (env, denv) c 2741 | SOME c => elabCon (env, denv) c
2729 2742
2730 val (e', et, gs2) = elabExp (env, denv) e 2743 val (e', et, gs2) = elabExp (env, denv) e
2744 val gs3 = checkCon (env, denv) e' et c'
2745 val (c', gs4) = normClassConstraint (env, denv) c'
2731 val (env', n) = E.pushENamed env x c' 2746 val (env', n) = E.pushENamed env x c'
2732 2747 in
2733 val gs3 = checkCon (env, denv) e' et c' 2748 (*prefaces "DVal" [("x", Print.PD.string x),
2734 in 2749 ("c'", p_con env c')];*)
2735 ([(L'.DVal (x, n, c', e'), loc)], (env', denv, gs1 @ gs2 @ gs3 @ gs)) 2750 ([(L'.DVal (x, n, c', e'), loc)], (env', denv, gs1 @ gs2 @ gs3 @ gs4 @ gs))
2736 end 2751 end
2737 | L.DValRec vis => 2752 | L.DValRec vis =>
2738 let 2753 let
2739 val (vis, gs) = ListUtil.foldlMap 2754 val (vis, gs) = ListUtil.foldlMap
2740 (fn ((x, co, e), gs) => 2755 (fn ((x, co, e), gs) =>