diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-08-14 18:35:08 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-08-14 18:35:08 -0400 |
| commit | 7bdc4cabdb8e5efbc4a194fe0bfe9442c7644798 (patch) | |
| tree | ce4be93140bacbd8900ff57affd5f866fbbf3ad0 /src/elab_util.sml | |
| parent | 5c9a5278b49ccf481468d5a766a8c4ab0cde2658 (diff) | |
Non-star SELECT
Diffstat (limited to 'src/elab_util.sml')
| -rw-r--r-- | src/elab_util.sml | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/src/elab_util.sml b/src/elab_util.sml index 3c1860c7..b0bca7bf 100644 --- a/src/elab_util.sml +++ b/src/elab_util.sml @@ -68,6 +68,11 @@ fun mapfold f = | KUnit => S.return2 kAll + | KTuple ks => + S.map2 (ListUtil.mapfold mfk ks, + fn ks' => + (KTuple ks', loc)) + | KError => S.return2 kAll | KUnif (_, _, ref (SOME k)) => mfk' k @@ -180,6 +185,16 @@ fun mapfoldB {kind = fk, con = fc, bind} = | 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)) + | CError => S.return2 cAll | CUnif (_, _, _, ref (SOME c)) => mfc' ctx c | CUnif _ => S.return2 cAll |