summaryrefslogtreecommitdiff
path: root/src/expl_util.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-08-16 14:45:23 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-08-16 14:45:23 -0400
commite9456cb231725d65a9cdd11dc3d4549fe7254e06 (patch)
treed2582b97f013e5759f2c0aa3f9bc030b74e92991 /src/expl_util.sml
parent70cd2b655dd741ad04a98dbe6685ec2ec9e11fdd (diff)
Explifying type classes
Diffstat (limited to 'src/expl_util.sml')
-rw-r--r--src/expl_util.sml15
1 files changed, 15 insertions, 0 deletions
diff --git a/src/expl_util.sml b/src/expl_util.sml
index ef82af44..a90e6bed 100644
--- a/src/expl_util.sml
+++ b/src/expl_util.sml
@@ -57,6 +57,11 @@ fun mapfold f =
(KRecord k', loc))
| KUnit => S.return2 kAll
+
+ | KTuple ks =>
+ S.map2 (ListUtil.mapfold mfk ks,
+ fn ks' =>
+ (KTuple ks', loc))
in
mfk
end
@@ -148,6 +153,16 @@ fun mapfoldB {kind = fk, con = fc, bind} =
(CFold (k1', k2'), loc)))
| CUnit => S.return2 cAll
+
+ | CTuple cs =>
+ S.map2 (ListUtil.mapfold (mfc ctx) cs,
+ fn cs' =>
+ (CTuple cs', loc))
+
+ | CProj (c, n) =>
+ S.map2 (mfc ctx c,
+ fn c' =>
+ (CProj (c', n), loc))
in
mfc
end