diff options
author | Adam Chlipala <adamc@hcoop.net> | 2008-01-26 16:44:39 -0500 |
---|---|---|
committer | Adam Chlipala <adamc@hcoop.net> | 2008-01-26 16:44:39 -0500 |
commit | 53109d697cd8ff1aa7e4b8c41f3bd71dd2671fc0 (patch) | |
tree | 0da23cead212d30f6066b38f5a13b7fdfb3e0a15 /src/elab_util.sml | |
parent | e7e2ffc58a4f120801ae69217032948e511af213 (diff) |
Check for leftover kind unifs
Diffstat (limited to 'src/elab_util.sml')
-rw-r--r-- | src/elab_util.sml | 99 |
1 files changed, 93 insertions, 6 deletions
diff --git a/src/elab_util.sml b/src/elab_util.sml index f889db30..37d58fcc 100644 --- a/src/elab_util.sml +++ b/src/elab_util.sml @@ -33,7 +33,7 @@ structure S = Search structure Kind = struct -fun mapfold (f : (Elab.kind', 'state, 'abort) S.mapfold_arg) : (Elab.kind, 'state, 'abort) S.mapfolder = +fun mapfold f = let fun mfk k acc = S.bindP (mfk' k acc, f) @@ -65,11 +65,98 @@ fun mapfold (f : (Elab.kind', 'state, 'abort) S.mapfold_arg) : (Elab.kind, 'stat end fun exists f k = - case mapfold (fn (k, ()) => - if f k then - S.Return () - else - S.Continue (k, ())) k () of + case mapfold (fn k => fn () => + if f k then + S.Return () + else + S.Continue (k, ())) k () of + S.Return _ => true + | S.Continue _ => false + +end + +structure Con = struct + +fun mapfold {kind = fk, con = fc} = + let + val mfk = Kind.mapfold fk + + fun mfc c acc = + S.bindP (mfc' c acc, fc) + + and mfc' (cAll as (c, loc)) = + case c of + TFun (c1, c2) => + S.bind2 (mfc c1, + fn c1' => + S.map2 (mfc c2, + fn c2' => + (TFun (c1', c2'), loc))) + | TCFun (e, x, k, c) => + S.bind2 (mfk k, + fn k' => + S.map2 (mfc c, + fn c' => + (TCFun (e, x, k', c'), loc))) + | TRecord c => + S.map2 (mfc c, + fn c' => + (TRecord c', loc)) + + | CRel _ => S.return2 cAll + | CNamed _ => S.return2 cAll + | CApp (c1, c2) => + S.bind2 (mfc c1, + fn c1' => + S.map2 (mfc c2, + fn c2' => + (CApp (c1', c2'), loc))) + | CAbs (e, x, k, c) => + S.bind2 (mfk k, + fn k' => + S.map2 (mfc c, + fn c' => + (CAbs (e, x, k', c'), loc))) + + | CName _ => S.return2 cAll + + | CRecord (k, xcs) => + S.bind2 (mfk k, + fn k' => + S.map2 (ListUtil.mapfold (fn (x, c) => + S.bind2 (mfc x, + fn x' => + S.map2 (mfc c, + fn c' => + (x', c')))) + xcs, + fn xcs' => + (CRecord (k', xcs'), loc))) + | CConcat (c1, c2) => + S.bind2 (mfc c1, + fn c1' => + S.map2 (mfc c2, + fn c2' => + (CConcat (c1', c2'), loc))) + + | CError => S.return2 cAll + | CUnif (_, _, ref (SOME c)) => mfc' c + | CUnif _ => S.return2 cAll + in + mfc + end + +fun exists {kind, con} k = + case mapfold {kind = fn k => fn () => + if kind k then + S.Return () + else + S.Continue (k, ()), + con = fn c => fn () => + if con c then + S.Return () + else + S.Continue (c, ())} k () of S.Return _ => true | S.Continue _ => false |