Mercurial > urweb
diff 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 |
line wrap: on
line diff
--- a/src/elaborate.sml Tue Jul 22 15:22:34 2008 -0400 +++ b/src/elaborate.sml Tue Jul 22 18:20:13 2008 -0400 @@ -1988,41 +1988,42 @@ case #1 (hnormSgn env sgn) of L'.SgnConst sgis => let - fun doOne (all as (sgi, _)) = - case sgi of - L'.SgiVal (x, n, t) => - (case hnormCon (env, denv) t of - ((L'.TFun (dom, ran), _), []) => - (case (hnormCon (env, denv) dom, hnormCon (env, denv) ran) of - (((L'.TRecord domR, _), []), - ((L'.CApp (tf, arg3), _), [])) => - (case (hnormCon (env, denv) tf, hnormCon (env, denv) arg3) of - (((L'.CApp (tf, arg2), _), []), - (((L'.CRecord (_, []), _), []))) => - (case (hnormCon (env, denv) tf) of - ((L'.CApp (tf, arg1), _), []) => - (case (hnormCon (env, denv) tf, - hnormCon (env, denv) domR, - hnormCon (env, denv) arg2) of - ((tf, []), (domR, []), - ((L'.CRecord (_, []), _), [])) => - let - val t = (L'.CApp (tf, arg1), loc) - val t = (L'.CApp (t, arg2), loc) - val t = (L'.CApp (t, arg3), loc) - in - (L'.SgiVal (x, n, (L'.TFun ((L'.TRecord domR, loc), - t), - loc)), loc) - end - | _ => all) - | _ => all) - | _ => all) - | _ => all) - | _ => all) - | _ => all + fun doOne (all as (sgi, _), env) = + (case sgi of + L'.SgiVal (x, n, t) => + (case hnormCon (env, denv) t of + ((L'.TFun (dom, ran), _), []) => + (case (hnormCon (env, denv) dom, hnormCon (env, denv) ran) of + (((L'.TRecord domR, _), []), + ((L'.CApp (tf, arg3), _), [])) => + (case (hnormCon (env, denv) tf, hnormCon (env, denv) arg3) of + (((L'.CApp (tf, arg2), _), []), + (((L'.CRecord (_, []), _), []))) => + (case (hnormCon (env, denv) tf) of + ((L'.CApp (tf, arg1), _), []) => + (case (hnormCon (env, denv) tf, + hnormCon (env, denv) domR, + hnormCon (env, denv) arg2) of + ((tf, []), (domR, []), + ((L'.CRecord (_, []), _), [])) => + let + val t = (L'.CApp (tf, arg1), loc) + val t = (L'.CApp (t, arg2), loc) + val t = (L'.CApp (t, arg3), loc) + in + (L'.SgiVal (x, n, (L'.TFun ((L'.TRecord domR, loc), + t), + loc)), loc) + end + | _ => all) + | _ => all) + | _ => all) + | _ => all) + | _ => all) + | _ => all, + E.sgiBinds env all) in - (L'.SgnConst (map doOne sgis), loc) + (L'.SgnConst (#1 (ListUtil.foldlMap doOne env sgis)), loc) end | _ => sgn in