Monoize transaction identifiers; improve disjointness prover on irreducible folds; change 'query' type

7 files changed, 112 insertions, 13 deletions

diff --git a/src/cjrize.sml b/src/cjrize.sml
index c745f43a..aa8ae562 100644
--- a/src/cjrize.sml
+++ b/src/cjrize.sml
@@ -275,6 +275,8 @@ fun cifyExp ((e, loc), sm) =
             ((L'.ESeq (e1, e2), loc), sm)
         end
 
+      | L.ELet _ => raise Fail "Cjrize ELet"
+
       | L.EClosure _ => (ErrorMsg.errorAt loc "Nested closure remains in code generation";
                          (dummye, sm))
 
diff --git a/src/corify.sml b/src/corify.sml
index c03fcf3a..50d47068 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -817,6 +817,7 @@ fun corifyDecl ((d, loc : EM.span), st) =
 
                                           val ef = (L.EModProj (basis, [], "bind"), loc)
                                           val ef = (L.ECApp (ef, ran'), loc)
+                                          val ef = (L.ECApp (ef, ran), loc)
                                           val ef = (L.EApp (ef, (L.EApp (e, (L.ERel 0, loc)), loc)), loc)
 
                                           val eat = (L.CApp ((L.CModProj (basis, [], "transaction"), loc),
diff --git a/src/disjoint.sml b/src/disjoint.sml
index dacb7161..069d3ec2 100644
--- a/src/disjoint.sml
+++ b/src/disjoint.sml
@@ -104,7 +104,9 @@ structure PM = BinaryMapFn(PK)
 
 type env = PS.set PM.map
 
-type goal = ErrorMsg.span * ElabEnv.env * env * Elab.con * Elab.con
+structure E = ElabEnv
+
+type goal = ErrorMsg.span * E.env * env * Elab.con * Elab.con
 
 val empty = PM.empty
 
@@ -151,6 +153,8 @@ fun prove1 denv (p1, p2) =
 
 fun decomposeRow (env, denv) c =
     let
+        val loc = #2 c
+
         fun decomposeProj c =
             let
                 val (c, gs) = hnormCon (env, denv) c
@@ -179,21 +183,59 @@ fun decomposeRow (env, denv) c =
                 (acc, gs' @ gs)
             end
 
-        fun decomposeRow (c, (acc, gs)) =
+        fun decomposeRow' (c, (acc, gs)) =
             let
-                val (cAll as (c, _), ns, gs') = decomposeProj c
-                val gs = gs' @ gs
+                fun default () =
+                    let
+                        val (cAll as (c, _), ns, gs') = decomposeProj c
+                        val gs = gs' @ gs
+                    in
+                        case c of
+                            CRecord (_, xcs) => foldl (fn ((x, _), acc_gs) => decomposeName (x, acc_gs)) (acc, gs) xcs
+                          | CConcat (c1, c2) => decomposeRow' (c1, decomposeRow' (c2, (acc, gs)))
+                          | CRel n => (Piece (RowR n, ns) :: acc, gs)
+                          | CNamed n => (Piece (RowN n, ns) :: acc, gs)
+                          | CModProj (m1, ms, x) => (Piece (RowM (m1, ms, x), ns) :: acc, gs)
+                          | _ => (Unknown cAll :: acc, gs)
+                    end
             in
-                case c of
-                    CRecord (_, xcs) => foldl (fn ((x, _), acc_gs) => decomposeName (x, acc_gs)) (acc, gs) xcs
-                  | CConcat (c1, c2) => decomposeRow (c1, decomposeRow (c2, (acc, gs)))
-                  | CRel n => (Piece (RowR n, ns) :: acc, gs)
-                  | CNamed n => (Piece (RowN n, ns) :: acc, gs)
-                  | CModProj (m1, ms, x) => (Piece (RowM (m1, ms, x), ns) :: acc, gs)
-                  | _ => (Unknown cAll :: acc, gs)
+                case #1 (#1 (hnormCon (env, denv) c)) of
+                    CApp (
+                    (CApp (
+                     (CApp ((CFold (dom, ran), _), f), _),
+                     i), _),
+                    r) =>
+                    let
+                        val (env', nm) = E.pushCNamed env "nm" (KName, loc) NONE
+                        val (env', v) = E.pushCNamed env' "v" dom NONE
+                        val (env', st) = E.pushCNamed env' "st" ran NONE
+
+                        val (denv', gs') = assert env' denv ((CRecord (dom, [((CNamed nm, loc),
+                                                                              (CUnit, loc))]), loc),
+                                                             (CNamed st, loc))
+
+                        val c' = (CApp (f, (CNamed nm, loc)), loc)
+                        val c' = (CApp (c', (CNamed v, loc)), loc)
+                        val c' = (CApp (c', (CNamed st, loc)), loc)
+                        val (ps, gs'') = decomposeRow (env', denv') c'
+
+                        fun covered p =
+                            case p of
+                                Unknown _ => false
+                              | Piece p =>
+                                case p of
+                                    (NameN n, []) => n = nm
+                                  | (RowN n, []) => n = st
+                                  | _ => false
+
+                        val ps = List.filter (not o covered) ps
+                    in
+                        decomposeRow' (i, decomposeRow' (r, (ps @ acc, gs'' @ gs' @ gs)))
+                    end
+                  | _ => default ()
             end
     in
-        decomposeRow (c, ([], []))
+        decomposeRow' (c, ([], []))
     end
 
 and assert env denv (c1, c2) =
diff --git a/src/mono.sml b/src/mono.sml
index 9599433c..c38e58ed 100644
--- a/src/mono.sml
+++ b/src/mono.sml
@@ -71,6 +71,7 @@ datatype exp' =
 
        | EWrite of exp
        | ESeq of exp * exp
+       | ELet of string * typ * exp * exp
 
        | EClosure of int * exp list
 
diff --git a/src/mono_print.sml b/src/mono_print.sml
index 7acb05b5..9ac80b42 100644
--- a/src/mono_print.sml
+++ b/src/mono_print.sml
@@ -185,6 +185,21 @@ fun p_exp' par env (e, _) =
                               string ";",
                               space,
                               p_exp env e2]
+      | ELet (x, t, e1, e2) => box [string "let",
+                                    space,
+                                    string x,
+                                    space,
+                                    string ":",
+                                    space,
+                                    p_typ env t,
+                                    space,
+                                    string "=",
+                                    space,
+                                    p_exp env e1,
+                                    space,
+                                    string "in",
+                                    space,
+                                    p_exp (E.pushERel env x t NONE) e2]
 
       | EClosure (n, es) => box [string "CLOSURE(",
                                  p_enamed env n,
diff --git a/src/mono_util.sml b/src/mono_util.sml
index 50927ac9..8f5b29e8 100644
--- a/src/mono_util.sml
+++ b/src/mono_util.sml
@@ -213,6 +213,14 @@ fun mapfoldB {typ = fc, exp = fe, bind} =
                          S.map2 (mfe ctx e2,
                               fn e2' =>
                                  (ESeq (e1', e2'), loc)))
+              | ELet (x, t, e1, e2) =>
+                S.bind2 (mft t,
+                         fn t' =>
+                            S.bind2 (mfe ctx e1,
+                                  fn e1' =>
+                                     S.map2 (mfe (bind (ctx, RelE (x, t))) e2,
+                                          fn e2' =>
+                                             (ELet (x, t', e1', e2'), loc))))
 
               | EClosure (n, es) =>
                 S.map2 (ListUtil.mapfold (mfe ctx) es,
diff --git a/src/monoize.sml b/src/monoize.sml
index 9142e63c..b1a38558 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -70,6 +70,9 @@ fun monoType env =
                   | L.CApp ((L.CApp ((L.CFfi ("Basis", "xhtml"), _), _), _), _) =>
                     (L'.TFfi ("Basis", "string"), loc)
 
+                  | L.CApp ((L.CFfi ("Basis", "transaction"), _), t) =>
+                    (L'.TFun (mt env dtmap t, (L'.TRecord [], loc)), loc)
+
                   | L.CRel _ => poly ()
                   | L.CNamed n =>
                     (case IM.find (dtmap, n) of
@@ -378,6 +381,24 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
                 ((L'.EFfiApp (m, x, es), loc), fm)
             end
 
+          | L.ECApp ((L.EFfi ("Basis", "return"), _), t) =>
+            ((L'.EAbs ("x", monoType env t, (L'.TRecord [], loc), (L'.ERel 0, loc)), loc), fm)
+          | L.ECApp ((L.ECApp ((L.EFfi ("Basis", "bind"), _), t1), _), t2) =>
+            let
+                val t1 = monoType env t1
+                val t2 = monoType env t2
+                val un = (L'.TRecord [], loc)
+                val mt1 = (L'.TFun (t1, un), loc)
+                val mt2 = (L'.TFun (t2, un), loc)
+            in
+                ((L'.EAbs ("m1", mt1, (L'.TFun (mt1, (L'.TFun (mt2, un), loc)), loc),
+                           (L'.EAbs ("m2", mt2, un,
+                                     (L'.ELet ("r", t1, (L'.ERel 1, loc),
+                                               (L'.EApp ((L'.ERel 1, loc), (L'.ERel 0, loc)),
+                                                loc)), loc)), loc)), loc),
+                 fm)
+            end
+
           | L.EApp (
             (L.ECApp (
              (L.ECApp ((L.EFfi ("Basis", "cdata"), _), _), _),
@@ -809,7 +830,16 @@ fun monoDecl (env, fm) (all as (d, loc)) =
             in
                 SOME (env, fm, (L'.DExport (ek, s, n, ts), loc))
             end
-          | L.DTable _ => raise Fail "Monoize DTable"
+          | L.DTable (x, n, _, s) =>
+            let
+                val t = (L.CFfi ("Basis", "string"), loc)
+                val t' = (L'.TFfi ("Basis", "string"), loc)
+                val e = (L'.EPrim (Prim.String s), loc)
+            in
+                SOME (Env.pushENamed env x n t NONE s,
+                      fm,
+                      (L'.DVal (x, n, t', e, s), loc))
+            end
     end
 
 fun monoize env ds =