Mercurial > urweb
diff src/elaborate.sml @ 249:b6b75e6e0898
Corify transaction wrappers
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 31 Aug 2008 09:45:23 -0400 |
parents | 2b9dfaffb008 |
children | 69d337f186eb |
line wrap: on
line diff
--- a/src/elaborate.sml Sun Aug 31 09:05:33 2008 -0400 +++ b/src/elaborate.sml Sun Aug 31 09:45:23 2008 -0400 @@ -3036,27 +3036,36 @@ ((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) arg1, - hnormCon (env, denv) arg2) of - ((tf, []), (domR, []), (arg1, []), - ((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 + ((L'.CApp (tf, arg), _), [])) => + (case (hnormCon (env, denv) tf, hnormCon (env, denv) arg) of + (((L'.CModProj (basis, [], "transaction"), _), []), + ((L'.CApp (tf, arg3), _), [])) => + (case (basis = !basis_r, + hnormCon (env, denv) tf, hnormCon (env, denv) arg3) of + (true, + ((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) arg1, + hnormCon (env, denv) arg2) of + ((tf, []), (domR, []), (arg1, []), + ((L'.CRecord (_, []), _), [])) => + let + val t = (L'.CApp (tf, arg1), loc) + val t = (L'.CApp (t, arg2), loc) + val t = (L'.CApp (t, arg3), loc) + val t = (L'.CApp ( + (L'.CModProj (basis, [], "transaction"), loc), + t), loc) + in + (L'.SgiVal (x, n, (L'.TFun ((L'.TRecord domR, loc), + t), + loc)), loc) + end + | _ => all) | _ => all) | _ => all) | _ => all)