summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/cjrize.sml2
-rw-r--r--src/corify.sml1
-rw-r--r--src/disjoint.sml66
-rw-r--r--src/mono.sml1
-rw-r--r--src/mono_print.sml15
-rw-r--r--src/mono_util.sml8
-rw-r--r--src/monoize.sml32
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 =
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-17 06:40:45 +0000