Mercurial > urweb
comparison src/elaborate.sml @ 146:80ac94b54e41
Fix opening and corifying of functors
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 22 Jul 2008 18:20:13 -0400 |
parents | 63c699450281 |
children | eb16f2aadbe9 |
comparison
equal
deleted
inserted
replaced
145:b1b33f7cf555 | 146:80ac94b54e41 |
---|---|
1986 | 1986 |
1987 val sgn = | 1987 val sgn = |
1988 case #1 (hnormSgn env sgn) of | 1988 case #1 (hnormSgn env sgn) of |
1989 L'.SgnConst sgis => | 1989 L'.SgnConst sgis => |
1990 let | 1990 let |
1991 fun doOne (all as (sgi, _)) = | 1991 fun doOne (all as (sgi, _), env) = |
1992 case sgi of | 1992 (case sgi of |
1993 L'.SgiVal (x, n, t) => | 1993 L'.SgiVal (x, n, t) => |
1994 (case hnormCon (env, denv) t of | 1994 (case hnormCon (env, denv) t of |
1995 ((L'.TFun (dom, ran), _), []) => | 1995 ((L'.TFun (dom, ran), _), []) => |
1996 (case (hnormCon (env, denv) dom, hnormCon (env, denv) ran) of | 1996 (case (hnormCon (env, denv) dom, hnormCon (env, denv) ran) of |
1997 (((L'.TRecord domR, _), []), | 1997 (((L'.TRecord domR, _), []), |
1998 ((L'.CApp (tf, arg3), _), [])) => | 1998 ((L'.CApp (tf, arg3), _), [])) => |
1999 (case (hnormCon (env, denv) tf, hnormCon (env, denv) arg3) of | 1999 (case (hnormCon (env, denv) tf, hnormCon (env, denv) arg3) of |
2000 (((L'.CApp (tf, arg2), _), []), | 2000 (((L'.CApp (tf, arg2), _), []), |
2001 (((L'.CRecord (_, []), _), []))) => | 2001 (((L'.CRecord (_, []), _), []))) => |
2002 (case (hnormCon (env, denv) tf) of | 2002 (case (hnormCon (env, denv) tf) of |
2003 ((L'.CApp (tf, arg1), _), []) => | 2003 ((L'.CApp (tf, arg1), _), []) => |
2004 (case (hnormCon (env, denv) tf, | 2004 (case (hnormCon (env, denv) tf, |
2005 hnormCon (env, denv) domR, | 2005 hnormCon (env, denv) domR, |
2006 hnormCon (env, denv) arg2) of | 2006 hnormCon (env, denv) arg2) of |
2007 ((tf, []), (domR, []), | 2007 ((tf, []), (domR, []), |
2008 ((L'.CRecord (_, []), _), [])) => | 2008 ((L'.CRecord (_, []), _), [])) => |
2009 let | 2009 let |
2010 val t = (L'.CApp (tf, arg1), loc) | 2010 val t = (L'.CApp (tf, arg1), loc) |
2011 val t = (L'.CApp (t, arg2), loc) | 2011 val t = (L'.CApp (t, arg2), loc) |
2012 val t = (L'.CApp (t, arg3), loc) | 2012 val t = (L'.CApp (t, arg3), loc) |
2013 in | 2013 in |
2014 (L'.SgiVal (x, n, (L'.TFun ((L'.TRecord domR, loc), | 2014 (L'.SgiVal (x, n, (L'.TFun ((L'.TRecord domR, loc), |
2015 t), | 2015 t), |
2016 loc)), loc) | 2016 loc)), loc) |
2017 end | 2017 end |
2018 | _ => all) | 2018 | _ => all) |
2019 | _ => all) | 2019 | _ => all) |
2020 | _ => all) | 2020 | _ => all) |
2021 | _ => all) | 2021 | _ => all) |
2022 | _ => all) | 2022 | _ => all) |
2023 | _ => all | 2023 | _ => all, |
2024 E.sgiBinds env all) | |
2024 in | 2025 in |
2025 (L'.SgnConst (map doOne sgis), loc) | 2026 (L'.SgnConst (#1 (ListUtil.foldlMap doOne env sgis)), loc) |
2026 end | 2027 end |
2027 | _ => sgn | 2028 | _ => sgn |
2028 in | 2029 in |
2029 ([(L'.DExport (E.newNamed (), sgn, str'), loc)], (env, denv, gs)) | 2030 ([(L'.DExport (E.newNamed (), sgn, str'), loc)], (env, denv, gs)) |
2030 end | 2031 end |