summaryrefslogtreecommitdiff
path: root/src/corify.sml
diff options
context:
space:
mode:
Diffstat (limited to 'src/corify.sml')
-rw-r--r--src/corify.sml217
1 files changed, 127 insertions, 90 deletions
diff --git a/src/corify.sml b/src/corify.sml
index 9ac5c84e..6793cd32 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -621,45 +621,65 @@ fun corifyDecl mods (all as (d, loc : EM.span), st) =
in
([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st)
end
- | L.DDatatype _ => raise Fail "Corify DDatatype"
- (*| L.DDatatype (x, n, xs, xncs) =>
+ | L.DDatatype dts =>
let
- val (st, n) = St.bindCon st x n
- val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) =>
- let
- val st = St.bindConstructor st x n (L'.PConVar n)
- val st = St.bindConstructorVal st x n
- val co = Option.map (corifyCon st) co
- in
- ((x, n, co), st)
- end) st xncs
-
- val dk = ElabUtil.classifyDatatype xncs
- val t = (L'.CNamed n, loc)
- val nxs = length xs - 1
- val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs
- val k = (L'.KType, loc)
- val dcons = map (fn (x, n, to) =>
- let
- val args = ListUtil.mapi (fn (i, _) => (L'.CRel (nxs - i), loc)) xs
- val (e, t) =
- case to of
- NONE => ((L'.ECon (dk, L'.PConVar n, args, NONE), loc), t)
- | SOME t' => ((L'.EAbs ("x", t', t,
- (L'.ECon (dk, L'.PConVar n, args,
- SOME (L'.ERel 0, loc)),
- loc)),
- loc),
- (L'.TFun (t', t), loc))
-
- val t = foldr (fn (x, t) => (L'.TCFun (x, k, t), loc)) t xs
- val e = foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc)) e xs
- in
- (L'.DVal (x, n, t, e, ""), loc)
- end) xncs
+ val (dts, st) = ListUtil.foldlMap (fn ((x, n, xs, xncs), st) =>
+ let
+ val (st, n) = St.bindCon st x n
+ in
+ ((x, n, xs, xncs), st)
+ end)
+ st dts
+
+ val (dts, (st, dcons)) =
+ ListUtil.foldlMap
+ (fn ((x, n, xs, xncs), (st, dcons)) =>
+ let
+ val (xncs, st) = ListUtil.foldlMap
+ (fn ((x, n, co), st) =>
+ let
+ val st = St.bindConstructor st x n (L'.PConVar n)
+ val st = St.bindConstructorVal st x n
+ val co = Option.map (corifyCon st) co
+ in
+ ((x, n, co), st)
+ end) st xncs
+
+ val dk = ElabUtil.classifyDatatype xncs
+ val t = (L'.CNamed n, loc)
+ val nxs = length xs - 1
+ val t = ListUtil.foldli
+ (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs
+ val k = (L'.KType, loc)
+ val dcons' = map (fn (x, n, to) =>
+ let
+ val args = ListUtil.mapi
+ (fn (i, _) => (L'.CRel (nxs - i), loc)) xs
+ val (e, t) =
+ case to of
+ NONE => ((L'.ECon (dk, L'.PConVar n, args, NONE),
+ loc), t)
+ | SOME t' => ((L'.EAbs ("x", t', t,
+ (L'.ECon (dk, L'.PConVar n,
+ args,
+ SOME (L'.ERel 0,
+ loc)),
+ loc)),
+ loc),
+ (L'.TFun (t', t), loc))
+
+ val t = foldr (fn (x, t) => (L'.TCFun (x, k, t), loc)) t xs
+ val e = foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc)) e xs
+ in
+ (L'.DVal (x, n, t, e, ""), loc)
+ end) xncs
+ in
+ ((x, n, xs, xncs), (st, dcons' @ dcons))
+ end)
+ (st, []) dts
in
- ((L'.DDatatype (x, n, xs, xncs), loc) :: dcons, st)
- end*)
+ ((L'.DDatatype dts, loc) :: dcons, st)
+ end
| L.DDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
let
val (st, n) = St.bindCon st x n
@@ -796,69 +816,86 @@ fun corifyDecl mods (all as (d, loc : EM.span), st) =
trans)
end
- | L.SgiDatatype _ => raise Fail "Corify SgiDatatype"
- (*| L.SgiDatatype (x, n, xs, xnts) =>
+ | L.SgiDatatype dts =>
let
val k = (L'.KType, loc)
- val dk = ElabUtil.classifyDatatype xnts
- val (st, n') = St.bindCon st x n
- val (xnts, (ds', st, cmap, conmap)) =
+
+ val (dts, (ds', st, cmap, conmap)) =
ListUtil.foldlMap
- (fn ((x', n, to), (ds', st, cmap, conmap)) =>
+ (fn ((x, n, xs, xnts), (ds', st, cmap, conmap)) =>
let
- val dt = (L'.CNamed n', loc)
- val args = ListUtil.mapi (fn (i, _) => (L'.CRel i, loc)) xs
-
- val to = Option.map (corifyCon st) to
-
- val pc = L'.PConFfi {mod = m,
- datatyp = x,
- params = xs,
- con = x',
- arg = to,
- kind = dk}
-
- fun wrapT t =
- foldr (fn (x, t) => (L'.TCFun (x, k, t), loc)) t xs
- fun wrapE e =
- foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc)) e xs
-
- val (cmap, d) =
- case to of
- NONE => (SM.insert (cmap, x', wrapT dt),
- (L'.DVal (x', n, wrapT dt,
- wrapE
- (L'.ECon (dk, pc, args, NONE),
- loc),
- ""), loc))
- | SOME t =>
- let
- val tf = (L'.TFun (t, dt), loc)
- val e = wrapE (L'.EAbs ("x", t, tf,
- (L'.ECon (dk, pc, args,
- SOME (L'.ERel 0,
- loc)),
- loc)), loc)
- val d = (L'.DVal (x', n, wrapT tf,
- e, ""), loc)
- in
- (SM.insert (cmap, x', wrapT tf), d)
- end
-
- val st = St.bindConstructor st x' n pc
-
- val conmap = SM.insert (conmap, x', (x, xs, to, dk))
+ val dk = ElabUtil.classifyDatatype xnts
+ val (st, n') = St.bindCon st x n
+ val (xnts, (ds', st, cmap, conmap)) =
+ ListUtil.foldlMap
+ (fn ((x', n, to), (ds', st, cmap, conmap)) =>
+ let
+ val dt = (L'.CNamed n', loc)
+ val args = ListUtil.mapi (fn (i, _) => (L'.CRel i, loc)) xs
+
+ val to = Option.map (corifyCon st) to
+
+ val pc = L'.PConFfi {mod = m,
+ datatyp = x,
+ params = xs,
+ con = x',
+ arg = to,
+ kind = dk}
+
+ fun wrapT t =
+ foldr (fn (x, t) => (L'.TCFun (x, k, t), loc))
+ t xs
+ fun wrapE e =
+ foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc))
+ e xs
+
+ val (cmap, d) =
+ case to of
+ NONE => (SM.insert (cmap, x', wrapT dt),
+ (L'.DVal (x', n, wrapT dt,
+ wrapE
+ (L'.ECon (dk, pc,
+ args,
+ NONE),
+ loc),
+ ""), loc))
+ | SOME t =>
+ let
+ val tf = (L'.TFun (t, dt), loc)
+ val e = wrapE
+ (L'.EAbs ("x", t, tf,
+ (L'.ECon (dk,
+ pc,
+ args,
+ SOME
+ (L'.ERel 0,
+ loc)),
+ loc)), loc)
+ val d = (L'.DVal (x', n, wrapT tf,
+ e, ""), loc)
+ in
+ (SM.insert (cmap, x', wrapT tf), d)
+ end
+
+ val st = St.bindConstructor st x' n pc
+
+ val conmap = SM.insert (conmap, x',
+ (x, xs, to, dk))
+ in
+ ((x', n, to),
+ (d :: ds', st, cmap, conmap))
+ end) (ds', st, cmap, conmap) xnts
in
- ((x', n, to),
- (d :: ds', st, cmap, conmap))
- end) ([], st, cmap, conmap) xnts
+ ((x, n', xs, xnts), (ds', st, cmap, conmap))
+ end)
+ ([], st, cmap, conmap) dts
in
- (ds' @ (L'.DDatatype (x, n', xs, xnts), loc) :: ds,
+ (ds' @ (L'.DDatatype dts, loc) :: ds,
cmap,
conmap,
st,
trans)
- end*)
+ end
| L.SgiVal (x, _, c) =>
let
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-09 11:08:20 +0000