diff src/reduce.sml @ 908:ed06e25c70ef

Convert to requiring explicit 'rpc' marker
author Adam Chlipala <adamc@hcoop.net>
date Sat, 22 Aug 2009 12:55:18 -0400
parents 669ac5e9a69e
children 1d3f60e74ec7
line wrap: on
line diff
--- a/src/reduce.sml	Tue Aug 11 12:01:54 2009 -0400
+++ b/src/reduce.sml	Sat Aug 22 12:55:18 2009 -0400
@@ -33,6 +33,14 @@
 
 structure IM = IntBinaryMap
 
+structure E = CoreEnv
+
+fun multiLiftExpInExp n e =
+    if n = 0 then
+        e
+    else
+        multiLiftExpInExp (n - 1) (E.liftExpInExp 0 e)
+
 datatype env_item =
          UnknownK
        | KnownK of kind
@@ -254,6 +262,98 @@
               | EFfi _ => all
               | EFfiApp (m, f, es) => (EFfiApp (m, f, map (exp env) es), loc)
 
+              | EApp (
+                (EApp
+                     ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _), t1), _), t2), _),
+                             _), _),
+                      (EApp (
+                       (EApp (
+                        (ECApp (
+                         (ECApp ((EFfi ("Basis", "return"), _), _), _),
+                         _), _),
+                        _), _), v), _)), _), trans2) => exp env (EApp (trans2, v), loc)
+
+              (*| EApp (
+                (EApp
+                     ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _), t1), _), t2), _),
+                             (EFfi ("Basis", "transaction_monad"), _)), _),
+                      (ECase (ed, pes, {disc, ...}), _)), _),
+                trans2) =>
+                let
+                    val e' = (EFfi ("Basis", "bind"), loc)
+                    val e' = (ECApp (e', (CFfi ("Basis", "transaction"), loc)), loc)
+                    val e' = (ECApp (e', t1), loc)
+                    val e' = (ECApp (e', t2), loc)
+                    val e' = (EApp (e', (EFfi ("Basis", "transaction_monad"), loc)), loc)
+
+                    val pes = map (fn (p, e) =>
+                                      let
+                                          val e' = (EApp (e', e), loc)
+                                          val e' = (EApp (e',
+                                                          multiLiftExpInExp (E.patBindsN p)
+                                                                            trans2), loc)
+                                          val e' = exp env e'
+                                      in
+                                          (p, e')
+                                      end) pes
+                in
+                    (ECase (exp env ed,
+                            pes,
+                            {disc = con env disc,
+                             result = (CApp ((CFfi ("Basis", "transaction"), loc), con env t2), loc)}),
+                     loc)
+                end*)
+
+              | EApp (
+                (EApp
+                     ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _), t1), _), t2), _),
+                             (EFfi ("Basis", "transaction_monad"), _)), _),
+                      (EServerCall (n, es, ke, dom, ran), _)), _),
+                trans2) =>
+                let
+                    val e' = (EFfi ("Basis", "bind"), loc)
+                    val e' = (ECApp (e', (CFfi ("Basis", "transaction"), loc)), loc)
+                    val e' = (ECApp (e', dom), loc)
+                    val e' = (ECApp (e', t2), loc)
+                    val e' = (EApp (e', (EFfi ("Basis", "transaction_monad"), loc)), loc)
+                    val e' = (EApp (e', (EApp (E.liftExpInExp 0 ke, (ERel 0, loc)), loc)), loc)
+                    val e' = (EApp (e', E.liftExpInExp 0 trans2), loc)
+                    val e' = (EAbs ("x", dom, t2, e'), loc)
+                    val e' = (EServerCall (n, es, e', dom, t2), loc)
+                in
+                    exp env e'
+                end
+
+              | EApp (
+                (EApp
+                     ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _), _), _), t3), _),
+                             (EFfi ("Basis", "transaction_monad"), _)), _),
+                      (EApp ((EApp
+                                  ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), _), _), _), t1), _), t2), _),
+                                          (EFfi ("Basis", "transaction_monad"), _)), _),
+                                   trans1), _), trans2), _)), _),
+                trans3) =>
+                let
+                    val e'' = (EFfi ("Basis", "bind"), loc)
+                    val e'' = (ECApp (e'', (CFfi ("Basis", "transaction"), loc)), loc)
+                    val e'' = (ECApp (e'', t2), loc)
+                    val e'' = (ECApp (e'', t3), loc)
+                    val e'' = (EApp (e'', (EFfi ("Basis", "transaction_monad"), loc)), loc)
+                    val e'' = (EApp (e'', (EApp (E.liftExpInExp 0 trans2, (ERel 0, loc)), loc)), loc)
+                    val e'' = (EApp (e'', E.liftExpInExp 0 trans3), loc)
+                    val e'' = (EAbs ("x", t1, (CApp ((CFfi ("Basis", "transaction"), loc), t3), loc), e''), loc)
+
+                    val e' = (EFfi ("Basis", "bind"), loc)
+                    val e' = (ECApp (e', (CFfi ("Basis", "transaction"), loc)), loc)
+                    val e' = (ECApp (e', t1), loc)
+                    val e' = (ECApp (e', t3), loc)
+                    val e' = (EApp (e', (EFfi ("Basis", "transaction_monad"), loc)), loc)
+                    val e' = (EApp (e', trans1), loc)
+                    val e' = (EApp (e', e''), loc)
+                in
+                    exp env e'
+                end
+
               | EApp (e1, e2) =>
                 let
                     val e1 = exp env e1
@@ -424,7 +524,8 @@
 
               | ELet (x, t, e1, e2) => (ELet (x, con env t, exp env e1, exp (UnknownE :: env) e2), loc)
 
-              | EServerCall (n, es, e, t) => (EServerCall (n, map (exp env) es, exp env e, con env t), loc))
+              | EServerCall (n, es, e, t1, t2) => (EServerCall (n, map (exp env) es, exp env e,
+                                                                con env t1, con env t2), loc))
     in
         {kind = kind, con = con, exp = exp}
     end