Mercurial > urweb

comparison src/elaborate.sml @ 467:3f1b9231a37b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Inserted a NULL value
author Adam Chlipala <adamc@hcoop.net>
date Thu, 06 Nov 2008 15:37:38 -0500
parents d34834af4512
children b393c2fc80f8
comparison
equal deleted inserted replaced
466:1626dcba13ee 467:3f1b9231a37b
1387 | SOME (_, SOME (c as (L'.CModProj _, _))) => unmodCon env c 1387 | SOME (_, SOME (c as (L'.CModProj _, _))) => unmodCon env c
1388 | _ => (c, loc) 1388 | _ => (c, loc)
1389 end 1389 end
1390 | _ => (c, loc) 1390 | _ => (c, loc)
1391 1391
1392 fun normClassConstraint envs (c, loc) = 1392 fun normClassKey envs c =
1393 let
1394 val c = ElabOps.hnormCon envs c
1395 in
1396 case #1 c of
1397 L'.CApp (c1, c2) =>
1398 let
1399 val c1 = normClassKey envs c1
1400 val c2 = normClassKey envs c2
1401 in
1402 (L'.CApp (c1, c2), #2 c)
1403 end
1404 | _ => c
1405 end
1406
1407 fun normClassConstraint env (c, loc) =
1393 case c of 1408 case c of
1394 L'.CApp (f, x) => 1409 L'.CApp (f, x) =>
1395 let 1410 let
1396 val f = unmodCon (#1 envs) f 1411 val f = unmodCon env f
1397 val (x, gs) = hnormCon envs x 1412 val x = normClassKey env x
1398 in 1413 in
1399 ((L'.CApp (f, x), loc), gs) 1414 (L'.CApp (f, x), loc)
1400 end 1415 end
1401 | L'.CUnif (_, _, _, ref (SOME c)) => normClassConstraint envs c 1416 | L'.CUnif (_, _, _, ref (SOME c)) => normClassConstraint env c
1402 | _ => ((c, loc), []) 1417 | _ => (c, loc)
1403 1418
1404 1419
1405 val makeInstantiable = 1420 val makeInstantiable =
1406 let 1421 let
1407 fun kind k = k 1422 fun kind k = k
1489 val (t', tk, gs) = elabCon (env, denv) t 1504 val (t', tk, gs) = elabCon (env, denv) t
1490 in 1505 in
1491 checkKind env t' tk ktype; 1506 checkKind env t' tk ktype;
1492 (t', gs) 1507 (t', gs)
1493 end 1508 end
1494 val (dom, gs2) = normClassConstraint (env, denv) t' 1509 val dom = normClassConstraint env t'
1495 val (e', et, gs3) = elabExp (E.pushERel env x dom, denv) e 1510 val (e', et, gs2) = elabExp (E.pushERel env x dom, denv) e
1496 in 1511 in
1497 ((L'.EAbs (x, t', et, e'), loc), 1512 ((L'.EAbs (x, t', et, e'), loc),
1498 (L'.TFun (t', et), loc), 1513 (L'.TFun (t', et), loc),
1499 enD gs1 @ enD gs2 @ gs3) 1514 enD gs1 @ gs2)
1500 end 1515 end
1501 | L.ECApp (e, c) => 1516 | L.ECApp (e, c) =>
1502 let 1517 let
1503 val (e', et, gs1) = elabExp (env, denv) e 1518 val (e', et, gs1) = elabExp (env, denv) e
1504 val oldEt = et 1519 val oldEt = et
1706 NONE => (cunif (loc, ktype), ktype, []) 1721 NONE => (cunif (loc, ktype), ktype, [])
1707 | SOME c => elabCon (env, denv) c 1722 | SOME c => elabCon (env, denv) c
1708 1723
1709 val (e', et, gs2) = elabExp (env, denv) e 1724 val (e', et, gs2) = elabExp (env, denv) e
1710 val gs3 = checkCon (env, denv) e' et c' 1725 val gs3 = checkCon (env, denv) e' et c'
1711 val (c', gs4) = normClassConstraint (env, denv) c' 1726 val c' = normClassConstraint env c'
1712 val env' = E.pushERel env x c' 1727 val env' = E.pushERel env x c'
1713 val c' = makeInstantiable c' 1728 val c' = makeInstantiable c'
1714 in 1729 in
1715 ((L'.EDVal (x, c', e'), loc), (env', enD gs1 @ gs2 @ enD gs3 @ enD gs4 @ gs)) 1730 ((L'.EDVal (x, c', e'), loc), (env', enD gs1 @ gs2 @ enD gs3 @ gs))
1716 end 1731 end
1717 | L.EDValRec vis => 1732 | L.EDValRec vis =>
1718 let 1733 let
1719 fun allowable (e, _) = 1734 fun allowable (e, _) =
1720 case e of 1735 case e of
1882 | L.SgiVal (x, c) => 1897 | L.SgiVal (x, c) =>
1883 let 1898 let
1884 val (c', ck, gs') = elabCon (env, denv) c 1899 val (c', ck, gs') = elabCon (env, denv) c
1885 1900
1886 val (env', n) = E.pushENamed env x c' 1901 val (env', n) = E.pushENamed env x c'
1887 val (c', gs'') = normClassConstraint (env, denv) c' 1902 val c' = normClassConstraint env c'
1888 in 1903 in
1889 (unifyKinds ck ktype 1904 (unifyKinds ck ktype
1890 handle KUnify ue => strError env (NotType (ck, ue))); 1905 handle KUnify ue => strError env (NotType (ck, ue)));
1891 1906
1892 ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs'' @ gs)) 1907 ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs))
1893 end 1908 end
1894 1909
1895 | L.SgiStr (x, sgn) => 1910 | L.SgiStr (x, sgn) =>
1896 let 1911 let
1897 val (sgn', gs') = elabSgn (env, denv) sgn 1912 val (sgn', gs') = elabSgn (env, denv) sgn
2873 NONE => (cunif (loc, ktype), ktype, []) 2888 NONE => (cunif (loc, ktype), ktype, [])
2874 | SOME c => elabCon (env, denv) c 2889 | SOME c => elabCon (env, denv) c
2875 2890
2876 val (e', et, gs2) = elabExp (env, denv) e 2891 val (e', et, gs2) = elabExp (env, denv) e
2877 val gs3 = checkCon (env, denv) e' et c' 2892 val gs3 = checkCon (env, denv) e' et c'
2878 val (c', gs4) = normClassConstraint (env, denv) c' 2893 val c = normClassConstraint env c'
2879 val (env', n) = E.pushENamed env x c' 2894 val (env', n) = E.pushENamed env x c'
2880 val c' = makeInstantiable c' 2895 val c' = makeInstantiable c'
2881 in 2896 in
2882 (*prefaces "DVal" [("x", Print.PD.string x), 2897 (*prefaces "DVal" [("x", Print.PD.string x),
2883 ("c'", p_con env c')];*) 2898 ("c'", p_con env c')];*)
2884 ([(L'.DVal (x, n, c', e'), loc)], (env', denv, enD gs1 @ gs2 @ enD gs3 @ enD gs4 @ gs)) 2899 ([(L'.DVal (x, n, c', e'), loc)], (env', denv, enD gs1 @ gs2 @ enD gs3 @ gs))
2885 end 2900 end
2886 | L.DValRec vis => 2901 | L.DValRec vis =>
2887 let 2902 let
2888 fun allowable (e, _) = 2903 fun allowable (e, _) =
2889 case e of 2904 case e of
3402 ("Con 2", p_con env c2), 3417 ("Con 2", p_con env c2),
3403 ("Hnormed 1", p_con env (ElabOps.hnormCon env c1)), 3418 ("Hnormed 1", p_con env (ElabOps.hnormCon env c1)),
3404 ("Hnormed 2", p_con env (ElabOps.hnormCon env c2))])) 3419 ("Hnormed 2", p_con env (ElabOps.hnormCon env c2))]))
3405 | TypeClass (env, c, r, loc) => 3420 | TypeClass (env, c, r, loc) =>
3406 let 3421 let
3407 val c = ElabOps.hnormCon env c 3422 val c = normClassKey env c
3408 in 3423 in
3409 case E.resolveClass env c of 3424 case E.resolveClass env c of
3410 SOME e => r := SOME e 3425 SOME e => r := SOME e
3411 | NONE => expError env (Unresolvable (loc, c)) 3426 | NONE => expError env (Unresolvable (loc, c))
3412 end) gs; 3427 end) gs;