aboutsummaryrefslogtreecommitdiffhomepage
path: root/src/elab_util.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-08-16 14:32:18 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-08-16 14:32:18 -0400
commitb4f1361d2dff2e180e4656efa491b275707cdf02 (patch)
treedc76b47422a5d2bcdbd78d9b9ab35fe30b4991c8 /src/elab_util.sml
parentc8fa648dbc2489ca4a56abbb27d94819fb75b5ec (diff)
Initial type class support
Diffstat (limited to 'src/elab_util.sml')
-rw-r--r--src/elab_util.sml19
1 files changed, 18 insertions, 1 deletions
diff --git a/src/elab_util.sml b/src/elab_util.sml
index b0bca7bf..c3ed2d19 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -376,6 +376,14 @@ fun exists {kind, con, exp} k =
S.Return _ => true
| S.Continue _ => false
+fun mapB {kind, con, exp, bind} ctx e =
+ case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()),
+ con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
+ exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()),
+ bind = bind} ctx e () of
+ S.Continue (e, ()) => e
+ | S.Return _ => raise Fail "ElabUtil.Exp.mapB: Impossible"
+
end
structure Sgn = struct
@@ -455,6 +463,11 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
S.map2 (con ctx c,
fn c' =>
(SgiTable (tn, x, n, c'), loc))
+ | SgiClassAbs _ => S.return2 siAll
+ | SgiClass (x, n, c) =>
+ S.map2 (con ctx c,
+ fn c' =>
+ (SgiClass (x, n, c'), loc))
and sg ctx s acc =
S.bindP (sg' ctx s acc, sgn ctx)
@@ -478,7 +491,11 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
| SgiSgn (x, _, sgn) =>
bind (ctx, Sgn (x, sgn))
| SgiConstraint _ => ctx
- | SgiTable _ => ctx,
+ | SgiTable _ => ctx
+ | SgiClassAbs (x, _) =>
+ bind (ctx, NamedC (x, (KArrow ((KType, loc), (KType, loc)), loc)))
+ | SgiClass (x, _, _) =>
+ bind (ctx, NamedC (x, (KArrow ((KType, loc), (KType, loc)), loc))),
sgi ctx si)) ctx sgis,
fn sgis' =>
(SgnConst sgis', loc))