Mercurial > urweb
diff src/core_util.sml @ 214:766b5475477f
Corifying con-tuples
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sat, 16 Aug 2008 15:03:05 -0400 |
parents | ab86aa858e6c |
children | 5c50b17f5e4a |
line wrap: on
line diff
--- a/src/core_util.sml Sat Aug 16 14:45:23 2008 -0400 +++ b/src/core_util.sml Sat Aug 16 15:03:05 2008 -0400 @@ -54,6 +54,10 @@ | (_, 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 @@ (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 @@ | (_, 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 @@ (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