Mercurial > urweb

comparison src/elaborate.sml @ 123:e3041657d653

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Parsing and elaborating (non-mutual) 'val rec'
author Adam Chlipala <adamc@hcoop.net>
date Thu, 17 Jul 2008 10:09:34 -0400
parents 3739af9e727a
children adfa2c7a75da
comparison
equal deleted inserted replaced
122:f7c6ceb87bbd 123:e3041657d653
1591 denv 1591 denv
1592 end 1592 end
1593 1593
1594 fun sgiOfDecl (d, loc) = 1594 fun sgiOfDecl (d, loc) =
1595 case d of 1595 case d of
1596 L'.DCon (x, n, k, c) => SOME (L'.SgiCon (x, n, k, c), loc) 1596 L'.DCon (x, n, k, c) => [(L'.SgiCon (x, n, k, c), loc)]
1597 | L'.DVal (x, n, t, _) => SOME (L'.SgiVal (x, n, t), loc) 1597 | L'.DVal (x, n, t, _) => [(L'.SgiVal (x, n, t), loc)]
1598 | L'.DSgn (x, n, sgn) => SOME (L'.SgiSgn (x, n, sgn), loc) 1598 | L'.DValRec vis => map (fn (x, n, t, _) => (L'.SgiVal (x, n, t), loc)) vis
1599 | L'.DStr (x, n, sgn, _) => SOME (L'.SgiStr (x, n, sgn), loc) 1599 | L'.DSgn (x, n, sgn) => [(L'.SgiSgn (x, n, sgn), loc)]
1600 | L'.DFfiStr (x, n, sgn) => SOME (L'.SgiStr (x, n, sgn), loc) 1600 | L'.DStr (x, n, sgn, _) => [(L'.SgiStr (x, n, sgn), loc)]
1601 | L'.DConstraint cs => SOME (L'.SgiConstraint cs, loc) 1601 | L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (x, n, sgn), loc)]
1602 | L'.DExport _ => NONE 1602 | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)]
1603 | L'.DExport _ => []
1603 1604
1604 fun sgiBindsD (env, denv) (sgi, _) = 1605 fun sgiBindsD (env, denv) (sgi, _) =
1605 case sgi of 1606 case sgi of
1606 L'.SgiConstraint (c1, c2) => 1607 L'.SgiConstraint (c1, c2) =>
1607 (case D.assert env denv (c1, c2) of 1608 (case D.assert env denv (c1, c2) of
1787 1788
1788 ([(L'.DCon (x, n, k', c'), loc)], (env', denv, gs' @ gs)) 1789 ([(L'.DCon (x, n, k', c'), loc)], (env', denv, gs' @ gs))
1789 end 1790 end
1790 | L.DVal (x, co, e) => 1791 | L.DVal (x, co, e) =>
1791 let 1792 let
1792 val (c', ck, gs1) = case co of 1793 val (c', _, gs1) = case co of
1793 NONE => (cunif (loc, ktype), ktype, []) 1794 NONE => (cunif (loc, ktype), ktype, [])
1794 | SOME c => elabCon (env, denv) c 1795 | SOME c => elabCon (env, denv) c
1795 1796
1796 val (e', et, gs2) = elabExp (env, denv) e 1797 val (e', et, gs2) = elabExp (env, denv) e
1797 val (env', n) = E.pushENamed env x c' 1798 val (env', n) = E.pushENamed env x c'
1798 1799
1799 val gs3 = checkCon (env, denv) e' et c' 1800 val gs3 = checkCon (env, denv) e' et c'
1800 in 1801 in
1801 ([(L'.DVal (x, n, c', e'), loc)], (env', denv, gs1 @ gs2 @ gs3 @ gs)) 1802 ([(L'.DVal (x, n, c', e'), loc)], (env', denv, gs1 @ gs2 @ gs3 @ gs))
1803 end
1804 | L.DValRec vis =>
1805 let
1806 val (vis, gs) = ListUtil.foldlMap
1807 (fn ((x, co, e), gs) =>
1808 let
1809 val (c', _, gs1) = case co of
1810 NONE => (cunif (loc, ktype), ktype, [])
1811 | SOME c => elabCon (env, denv) c
1812 in
1813 ((x, c', e), gs1 @ gs)
1814 end) [] vis
1815
1816 val (vis, env) = ListUtil.foldlMap (fn ((x, c', e), env) =>
1817 let
1818 val (env, n) = E.pushENamed env x c'
1819 in
1820 ((x, n, c', e), env)
1821 end) env vis
1822
1823 val (vis, gs) = ListUtil.foldlMap (fn ((x, n, c', e), gs) =>
1824 let
1825 val (e', et, gs1) = elabExp (env, denv) e
1826
1827 val gs2 = checkCon (env, denv) e' et c'
1828 in
1829 ((x, n, c', e'), gs1 @ gs2 @ gs)
1830 end) gs vis
1831 in
1832 ([(L'.DValRec vis, loc)], (env, denv, gs))
1802 end 1833 end
1803 1834
1804 | L.DSgn (x, sgn) => 1835 | L.DSgn (x, sgn) =>
1805 let 1836 let
1806 val (sgn', gs') = elabSgn (env, denv) sgn 1837 val (sgn', gs') = elabSgn (env, denv) sgn
1968 and elabStr (env, denv) (str, loc) = 1999 and elabStr (env, denv) (str, loc) =
1969 case str of 2000 case str of
1970 L.StrConst ds => 2001 L.StrConst ds =>
1971 let 2002 let
1972 val (ds', (_, _, gs)) = ListUtil.foldlMapConcat elabDecl (env, denv, []) ds 2003 val (ds', (_, _, gs)) = ListUtil.foldlMapConcat elabDecl (env, denv, []) ds
1973 val sgis = List.mapPartial sgiOfDecl ds' 2004 val sgis = ListUtil.mapConcat sgiOfDecl ds'
1974 2005
1975 val (sgis, _, _, _, _) = 2006 val (sgis, _, _, _, _) =
1976 foldr (fn ((sgi, loc), (sgis, cons, vals, sgns, strs)) => 2007 foldr (fn ((sgi, loc), (sgis, cons, vals, sgns, strs)) =>
1977 case sgi of 2008 case sgi of
1978 L'.SgiConAbs (x, n, k) => 2009 L'.SgiConAbs (x, n, k) =>