diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-08-16 15:03:05 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-08-16 15:03:05 -0400 |
| commit | 6cac02596e21666de5658f83957d3fa7d7b60a8c (patch) | |
| tree | ba8d7f45822b7cba62fe659ce25ea3504475ef73 /src/core_util.sml | |
| parent | e9456cb231725d65a9cdd11dc3d4549fe7254e06 (diff) | |
Corifying con-tuples
Diffstat (limited to 'src/core_util.sml')
| -rw-r--r-- | src/core_util.sml | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/src/core_util.sml b/src/core_util.sml index f79e6d20..3403a9d1 100644 --- a/src/core_util.sml +++ b/src/core_util.sml @@ -54,6 +54,10 @@ fun compare ((k1, _), (k2, _)) = | (_, KRecord _) => GREATER | (KUnit, KUnit) => EQUAL + | (KUnit, _) => LESS + | (_, KUnit) => GREATER + + | (KTuple ks1, KTuple ks2) => joinL compare (ks1, ks2) fun mapfold f = let @@ -79,6 +83,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 @@ -170,6 +179,15 @@ fun compare ((c1, _), (c2, _)) = | (_, CFold _) => GREATER | (CUnit, CUnit) => EQUAL + | (CUnit, _) => LESS + | (_, CUnit) => GREATER + + | (CTuple cs1, CTuple cs2) => joinL compare (cs1, cs2) + | (CTuple _, _) => LESS + | (_, CTuple _) => GREATER + + | (CProj (c1, n1), CProj (c2, n2)) => join (Int.compare (n1, n2), + fn () => compare (c1, c2)) datatype binder = Rel of string * kind @@ -245,6 +263,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 |