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)