# HG changeset patch # User Adam Chlipala # Date 1218912323 14400 # Node ID 0343557355fcfdd030b7bad02a34424fbac24558 # Parent ba4d7c33a45fda4e25a68d561e14d9b6654eacbc Explifying type classes diff -r ba4d7c33a45f -r 0343557355fc src/corify.sml --- a/src/corify.sml Sat Aug 16 14:36:17 2008 -0400 +++ b/src/corify.sml Sat Aug 16 14:45:23 2008 -0400 @@ -380,6 +380,7 @@ | L.KName => (L'.KName, loc) | L.KRecord k => (L'.KRecord (corifyKind k), loc) | L.KUnit => (L'.KUnit, loc) + | L.KTuple _ => raise Fail "Corify KTuple" fun corifyCon st (c, loc) = case c of @@ -413,6 +414,9 @@ | 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" + fun corifyPatCon st pc = case pc of L.PConVar n => St.lookupConstructorById st n diff -r ba4d7c33a45f -r 0343557355fc src/elab.sml --- a/src/elab.sml Sat Aug 16 14:36:17 2008 -0400 +++ b/src/elab.sml Sat Aug 16 14:45:23 2008 -0400 @@ -150,6 +150,7 @@ | DConstraint of con * con | DExport of int * sgn * str | DTable of int * string * int * con + | DClass of string * int * con and str' = StrConst of decl list diff -r ba4d7c33a45f -r 0343557355fc src/elab_env.sml --- a/src/elab_env.sml Sat Aug 16 14:36:17 2008 -0400 +++ b/src/elab_env.sml Sat Aug 16 14:45:23 2008 -0400 @@ -958,5 +958,12 @@ in pushENamedAs env x n t end + | DClass (x, n, c) => + let + val k = (KArrow ((KType, loc), (KType, loc)), loc) + val env = pushCNamedAs env x n k (SOME c) + in + pushClass env n + end end diff -r ba4d7c33a45f -r 0343557355fc src/elab_print.sml --- a/src/elab_print.sml Sat Aug 16 14:36:17 2008 -0400 +++ b/src/elab_print.sml Sat Aug 16 14:45:23 2008 -0400 @@ -630,6 +630,13 @@ string ":", space, p_con env c] + | DClass ( x, n, c) => box [string "class", + space, + p_named x n, + space, + string "=", + space, + p_con env c] and p_str env (str, _) = case str of diff -r ba4d7c33a45f -r 0343557355fc src/elab_util.sml --- a/src/elab_util.sml Sat Aug 16 14:36:17 2008 -0400 +++ b/src/elab_util.sml Sat Aug 16 14:45:23 2008 -0400 @@ -634,7 +634,9 @@ | DExport _ => ctx | DTable (tn, x, n, c) => bind (ctx, NamedE (x, (CApp ((CModProj (n, [], "table"), loc), - c), loc))), + c), loc))) + | DClass (x, _, _) => + bind (ctx, NamedC (x, (KArrow ((KType, loc), (KType, loc)), loc))), mfd ctx d)) ctx ds, fn ds' => (StrConst ds', loc)) | StrVar _ => S.return2 strAll @@ -727,6 +729,11 @@ fn c' => (DTable (tn, x, n, c'), loc)) + | DClass (x, n, c) => + S.map2 (mfc ctx c, + fn c' => + (DClass (x, n, c'), loc)) + and mfvi ctx (x, n, c, e) = S.bind2 (mfc ctx c, fn c' => diff -r ba4d7c33a45f -r 0343557355fc src/elaborate.sml --- a/src/elaborate.sml Sat Aug 16 14:36:17 2008 -0400 +++ b/src/elaborate.sml Sat Aug 16 14:45:23 2008 -0400 @@ -2235,6 +2235,7 @@ | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)] | L'.DExport _ => [] | L'.DTable (tn, x, n, c) => [(L'.SgiTable (tn, x, n, c), loc)] + | L'.DClass (x, n, c) => [(L'.SgiClass (x, n, c), loc)] fun sgiBindsD (env, denv) (sgi, _) = case sgi of @@ -2941,7 +2942,7 @@ val env = E.pushClass env n in checkKind env c' ck k; - ([(L'.DCon (x, n, k, c'), loc)], (env, denv, [])) + ([(L'.DClass (x, n, c'), loc)], (env, denv, [])) end and elabStr (env, denv) (str, loc) = diff -r ba4d7c33a45f -r 0343557355fc src/expl.sml --- a/src/expl.sml Sat Aug 16 14:36:17 2008 -0400 +++ b/src/expl.sml Sat Aug 16 14:45:23 2008 -0400 @@ -34,6 +34,7 @@ | KArrow of kind * kind | KName | KUnit + | KTuple of kind list | KRecord of kind withtype kind = kind' located @@ -57,6 +58,9 @@ | CUnit + | CTuple of con list + | CProj of con * int + withtype con = con' located datatype datatype_kind = datatype Elab.datatype_kind diff -r ba4d7c33a45f -r 0343557355fc src/expl_print.sml --- a/src/expl_print.sml Sat Aug 16 14:36:17 2008 -0400 +++ b/src/expl_print.sml Sat Aug 16 14:45:23 2008 -0400 @@ -49,6 +49,9 @@ | 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 @@ -147,6 +150,13 @@ 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 -r ba4d7c33a45f -r 0343557355fc src/expl_util.sml --- a/src/expl_util.sml Sat Aug 16 14:36:17 2008 -0400 +++ b/src/expl_util.sml Sat Aug 16 14:45:23 2008 -0400 @@ -57,6 +57,11 @@ (KRecord k', loc)) | KUnit => S.return2 kAll + + | KTuple ks => + S.map2 (ListUtil.mapfold mfk ks, + fn ks' => + (KTuple ks', loc)) in mfk end @@ -148,6 +153,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 diff -r ba4d7c33a45f -r 0343557355fc src/explify.sml --- a/src/explify.sml Sat Aug 16 14:36:17 2008 -0400 +++ b/src/explify.sml Sat Aug 16 14:45:23 2008 -0400 @@ -39,7 +39,7 @@ | L.KRecord k => (L'.KRecord (explifyKind k), loc) | L.KUnit => (L'.KUnit, loc) - | L.KTuple _ => raise Fail "Explify KTuple" + | L.KTuple ks => (L'.KTuple (map explifyKind ks), loc) | L.KError => raise Fail ("explifyKind: KError at " ^ EM.spanToString loc) | L.KUnif (_, _, ref (SOME k)) => explifyKind k @@ -68,8 +68,8 @@ | L.CUnit => (L'.CUnit, loc) - | L.CTuple _ => raise Fail "Explify CTuple" - | L.CProj _ => raise Fail "Explify CProj" + | L.CTuple cs => (L'.CTuple (map explifyCon cs), loc) + | L.CProj (c, n) => (L'.CProj (explifyCon c, n), loc) | L.CError => raise Fail ("explifyCon: CError at " ^ EM.spanToString loc) | L.CUnif (_, _, _, ref (SOME c)) => explifyCon c @@ -160,6 +160,8 @@ | L.DConstraint (c1, c2) => NONE | L.DExport (en, sgn, str) => SOME (L'.DExport (en, explifySgn sgn, explifyStr str), loc) | L.DTable _ => raise Fail "Explify DTable" + | L.DClass (x, n, c) => SOME (L'.DCon (x, n, + (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc), explifyCon c), loc) and explifyStr (str, loc) = case str of