diff options
| -rw-r--r-- | src/core.sml | 4 | ||||
| -rw-r--r-- | src/core_print.sml | 10 | ||||
| -rw-r--r-- | src/core_util.sml | 28 | ||||
| -rw-r--r-- | src/corify.sml | 6 | ||||
| -rw-r--r-- | src/monoize.sml | 3 |
5 files changed, 48 insertions, 3 deletions
diff --git a/src/core.sml b/src/core.sml index ce14ac04..30bd8b76 100644 --- a/src/core.sml +++ b/src/core.sml @@ -35,6 +35,7 @@ datatype kind' = | KName | KRecord of kind | KUnit + | KTuple of kind list withtype kind = kind' located @@ -57,6 +58,9 @@ datatype con' = | CUnit + | CTuple of con list + | CProj of con * int + withtype con = con' located datatype datatype_kind = datatype Elab.datatype_kind diff --git a/src/core_print.sml b/src/core_print.sml index 52c7648d..66432866 100644 --- a/src/core_print.sml +++ b/src/core_print.sml @@ -49,6 +49,9 @@ fun p_kind' par (k, _) = | KName => string "Name" | KRecord k => box [string "{", p_kind k, string "}"] | KUnit => string "Unit" + | KTuple ks => box [string "(", + p_list_sep (box [space, string "*", space]) p_kind ks, + string ")"] and p_kind k = p_kind' false k @@ -137,6 +140,13 @@ fun p_con' par env (c, _) = p_con env c2]) | CFold _ => string "fold" | CUnit => string "()" + + | CTuple cs => box [string "(", + p_list (p_con env) cs, + string ")"] + | CProj (c, n) => box [p_con env c, + string ".", + string (Int.toString n)] and p_con env = p_con' false env 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 diff --git a/src/corify.sml b/src/corify.sml index 1badcb9a..60baf903 100644 --- a/src/corify.sml +++ b/src/corify.sml @@ -380,7 +380,7 @@ structure St : sig | L.KName => (L'.KName, loc) | L.KRecord k => (L'.KRecord (corifyKind k), loc) | L.KUnit => (L'.KUnit, loc) - | L.KTuple _ => raise Fail "Corify KTuple" + | L.KTuple ks => (L'.KTuple (map corifyKind ks), loc) fun corifyCon st (c, loc) = case c of @@ -414,8 +414,8 @@ structure St : sig | L.CFold (k1, k2) => (L'.CFold (corifyKind k1, corifyKind k2), loc) | L.CUnit => (L'.CUnit, loc) - | L.CTuple _ => raise Fail "Corify CTuple" - | L.CProj _ => raise Fail "Corify CProj" + | L.CTuple cs => (L'.CTuple (map (corifyCon st) cs), loc) + | L.CProj (c, n) => (L'.CProj (corifyCon st c, n), loc) fun corifyPatCon st pc = case pc of diff --git a/src/monoize.sml b/src/monoize.sml index fe360d75..ba9c2087 100644 --- a/src/monoize.sml +++ b/src/monoize.sml @@ -98,6 +98,9 @@ fun monoType env = | L.CConcat _ => poly () | L.CFold _ => poly () | L.CUnit => poly () + + | L.CTuple _ => poly () + | L.CProj _ => poly () end in mt env IM.empty |