Mercurial > urweb

comparison src/elaborate.sml @ 447:b77863cd0be2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Elaborating 'let'
author Adam Chlipala <adamc@hcoop.net>
date Sat, 01 Nov 2008 11:17:29 -0400
parents dfc8c991abd0
children 222cbc1da232
comparison
equal deleted inserted replaced
446:86c063fedc4d 447:b77863cd0be2
1398 in 1398 in
1399 ((L'.CApp (f, x), loc), gs) 1399 ((L'.CApp (f, x), loc), gs)
1400 end 1400 end
1401 | _ => ((c, loc), []) 1401 | _ => ((c, loc), [])
1402 1402
1403
1404 val makeInstantiable =
1405 let
1406 fun kind k = k
1407 fun con c =
1408 case c of
1409 L'.CDisjoint (L'.LeaveAlone, c1, c2, c) => L'.CDisjoint (L'.Instantiate, c1, c2, c)
1410 | _ => c
1411 in
1412 U.Con.map {kind = kind, con = con}
1413 end
1414
1403 fun elabExp (env, denv) (eAll as (e, loc)) = 1415 fun elabExp (env, denv) (eAll as (e, loc)) =
1404 let 1416 let
1405 (*val () = eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)];*) 1417 (*val () = eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)];*)
1406 1418
1407 val r = case e of 1419 val r = case e of
1668 else 1680 else
1669 expError env (Inexhaustive loc); 1681 expError env (Inexhaustive loc);
1670 1682
1671 ((L'.ECase (e', pes', {disc = et, result = result}), loc), result, enD gs' @ gs) 1683 ((L'.ECase (e', pes', {disc = et, result = result}), loc), result, enD gs' @ gs)
1672 end 1684 end
1685
1686 | L.ELet (eds, e) =>
1687 let
1688 val (eds, (env, gs1)) = ListUtil.foldlMap (elabEdecl denv) (env, []) eds
1689 val (e, t, gs2) = elabExp (env, denv) e
1690 in
1691 ((L'.ELet (eds, e), loc), t, gs1 @ gs2)
1692 end
1673 in 1693 in
1674 (*prefaces "/elabExp" [("e", SourcePrint.p_exp eAll)];*) 1694 (*prefaces "/elabExp" [("e", SourcePrint.p_exp eAll)];*)
1695 r
1696 end
1697
1698 and elabEdecl denv (dAll as (d, loc), (env, gs : constraint list)) =
1699 let
1700 val r =
1701 case d of
1702 L.EDVal (x, co, e) =>
1703 let
1704 val (c', _, gs1) = case co of
1705 NONE => (cunif (loc, ktype), ktype, [])
1706 | SOME c => elabCon (env, denv) c
1707
1708 val (e', et, gs2) = elabExp (env, denv) e
1709 val gs3 = checkCon (env, denv) e' et c'
1710 val (c', gs4) = normClassConstraint (env, denv) c'
1711 val env' = E.pushERel env x c'
1712 val c' = makeInstantiable c'
1713 in
1714 ((L'.EDVal (x, c', e'), loc), (env', enD gs1 @ gs2 @ enD gs3 @ enD gs4 @ gs))
1715 end
1716 | L.EDValRec vis =>
1717 let
1718 fun allowable (e, _) =
1719 case e of
1720 L.EAbs _ => true
1721 | L.ECAbs (_, _, _, e) => allowable e
1722 | L.EDisjoint (_, _, e) => allowable e
1723 | _ => false
1724
1725 val (vis, gs) = ListUtil.foldlMap
1726 (fn ((x, co, e), gs) =>
1727 let
1728 val (c', _, gs1) = case co of
1729 NONE => (cunif (loc, ktype), ktype, [])
1730 | SOME c => elabCon (env, denv) c
1731 in
1732 ((x, c', e), enD gs1 @ gs)
1733 end) gs vis
1734
1735 val env = foldl (fn ((x, c', _), env) => E.pushERel env x c') env vis
1736
1737 val (vis, gs) = ListUtil.foldlMap (fn ((x, c', e), gs) =>
1738 let
1739 val (e', et, gs1) = elabExp (env, denv) e
1740
1741 val gs2 = checkCon (env, denv) e' et c'
1742
1743 val c' = makeInstantiable c'
1744 in
1745 if allowable e then
1746 ()
1747 else
1748 expError env (IllegalRec (x, e'));
1749 ((x, c', e'), gs1 @ enD gs2 @ gs)
1750 end) gs vis
1751 in
1752 ((L'.EDValRec vis, loc), (env, gs))
1753 end
1754 in
1675 r 1755 r
1676 end 1756 end
1677 1757
1678 val hnormSgn = E.hnormSgn 1758 val hnormSgn = E.hnormSgn
1679 1759
2740 end 2820 end
2741 end 2821 end
2742 | _ => str) 2822 | _ => str)
2743 | _ => str 2823 | _ => str
2744 2824
2745 val makeInstantiable =
2746 let
2747 fun kind k = k
2748 fun con c =
2749 case c of
2750 L'.CDisjoint (L'.LeaveAlone, c1, c2, c) => L'.CDisjoint (L'.Instantiate, c1, c2, c)
2751 | _ => c
2752 in
2753 U.Con.map {kind = kind, con = con}
2754 end
2755
2756 fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) = 2825 fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) =
2757 let 2826 let
2758 (*val () = preface ("elabDecl", SourcePrint.p_decl (d, loc))*) 2827 (*val () = preface ("elabDecl", SourcePrint.p_decl (d, loc))*)
2759 2828
2760 val r = 2829 val r =