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