Mercurial > urweb

comparison src/elaborate.sml @ 721:9864b64b1700

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Classes as optional arguments to Basis.tag
author Adam Chlipala <adamc@hcoop.net>
date Sun, 12 Apr 2009 14:19:15 -0400
parents acb8537f58f0
children 059074c8d2fc
comparison
equal deleted inserted replaced
720:acb8537f58f0 721:9864b64b1700
1491 | SOME (_, SOME (c as (L'.CModProj _, _))) => unmodCon env c 1491 | SOME (_, SOME (c as (L'.CModProj _, _))) => unmodCon env c
1492 | _ => (c, loc) 1492 | _ => (c, loc)
1493 end 1493 end
1494 | _ => (c, loc) 1494 | _ => (c, loc)
1495 1495
1496 fun normClassKey envs c = 1496 fun normClassKey env c =
1497 let 1497 let
1498 val c = hnormCon envs c 1498 val c = hnormCon env c
1499 in 1499 in
1500 case #1 c of 1500 case #1 c of
1501 L'.CApp (c1, c2) => 1501 L'.CApp (c1, c2) =>
1502 let 1502 let
1503 val c1 = normClassKey envs c1 1503 val c1 = normClassKey env c1
1504 val c2 = normClassKey envs c2 1504 val c2 = normClassKey env c2
1505 in 1505 in
1506 (L'.CApp (c1, c2), #2 c) 1506 (L'.CApp (c1, c2), #2 c)
1507 end 1507 end
1508 | _ => c 1508 | L'.CRecord (k, xcs) => (L'.CRecord (k, map (fn (x, c) => (normClassKey env x,
1509 normClassKey env c)) xcs), #2 c)
1510 | _ => unmodCon env c
1509 end 1511 end
1510 1512
1511 fun normClassConstraint env (c, loc) = 1513 fun normClassConstraint env (c, loc) =
1512 case c of 1514 case c of
1513 L'.CApp (f, x) => 1515 L'.CApp (f, x) =>
1514 let 1516 let
1515 val f = unmodCon env f 1517 val f = normClassKey env f
1516 val x = normClassKey env x 1518 val x = normClassKey env x
1517 in 1519 in
1518 (L'.CApp (f, x), loc) 1520 (L'.CApp (f, x), loc)
1519 end 1521 end
1520 | L'.TFun (c1, c2) => 1522 | L'.TFun (c1, c2) =>
1524 in 1526 in
1525 (L'.TFun (c1, c2), loc) 1527 (L'.TFun (c1, c2), loc)
1526 end 1528 end
1527 | L'.TCFun (expl, x, k, c1) => (L'.TCFun (expl, x, k, normClassConstraint env c1), loc) 1529 | L'.TCFun (expl, x, k, c1) => (L'.TCFun (expl, x, k, normClassConstraint env c1), loc)
1528 | L'.CUnif (_, _, _, ref (SOME c)) => normClassConstraint env c 1530 | L'.CUnif (_, _, _, ref (SOME c)) => normClassConstraint env c
1529 | _ => (c, loc) 1531 | _ => unmodCon env (c, loc)
1530 1532
1531 fun elabExp (env, denv) (eAll as (e, loc)) = 1533 fun elabExp (env, denv) (eAll as (e, loc)) =
1532 let 1534 let
1533 (*val () = eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)];*) 1535 (*val () = eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)];*)
1534 (*val befor = Time.now ()*) 1536 (*val befor = Time.now ()*)
2045 2047
2046 | L.SgiVal (x, c) => 2048 | L.SgiVal (x, c) =>
2047 let 2049 let
2048 val (c', ck, gs') = elabCon (env, denv) c 2050 val (c', ck, gs') = elabCon (env, denv) c
2049 2051
2052 val old = c'
2050 val c' = normClassConstraint env c' 2053 val c' = normClassConstraint env c'
2051 val (env', n) = E.pushENamed env x c' 2054 val (env', n) = E.pushENamed env x c'
2052 in 2055 in
2053 (unifyKinds env ck ktype 2056 (unifyKinds env ck ktype
2054 handle KUnify ue => strError env (NotType (loc, ck, ue))); 2057 handle KUnify ue => strError env (NotType (loc, ck, ue)));