Mercurial > urweb
changeset 809:81fce435e255
Mutual datatypes through Cjrize
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sat, 16 May 2009 16:02:17 -0400 |
| parents | d8f58d488cfb |
| children | c1f8963ebb18 |
| files | src/cjr.sml src/cjr_env.sml src/cjr_print.sml src/cjrize.sml |
| diffstat | 4 files changed, 98 insertions(+), 81 deletions(-) [+] |
line wrap: on
line diff
--- a/src/cjr.sml Sat May 16 15:55:15 2009 -0400 +++ b/src/cjr.sml Sat May 16 16:02:17 2009 -0400 @@ -100,7 +100,7 @@ datatype decl' = DStruct of int * (string * typ) list - | DDatatype of datatype_kind * string * int * (string * int * typ option) list + | DDatatype of (datatype_kind * string * int * (string * int * typ option) list) list | DDatatypeForward of datatype_kind * string * int | DVal of string * int * typ * exp | DFun of string * int * (string * typ) list * typ * exp
--- a/src/cjr_env.sml Sat May 16 15:55:15 2009 -0400 +++ b/src/cjr_env.sml Sat May 16 16:02:17 2009 -0400 @@ -137,15 +137,16 @@ fun declBinds env (d, loc) = case d of - DDatatype (_, x, n, xncs) => - let - val env = pushDatatype env x n xncs - val dt = (TDatatype (classifyDatatype xncs, n, ref xncs), loc) - in - foldl (fn ((x', n', NONE), env) => pushENamed env x' n' dt - | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, dt), loc)) - env xncs - end + DDatatype dts => + foldl (fn ((_, x, n, xncs), env) => + let + val env = pushDatatype env x n xncs + val dt = (TDatatype (classifyDatatype xncs, n, ref xncs), loc) + in + foldl (fn ((x', n', NONE), env) => pushENamed env x' n' dt + | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, dt), loc)) + env xncs + end) env dts | DDatatypeForward (_, x, n) => pushDatatype env x n [] | DStruct (n, xts) => pushStruct env n xts | DVal (x, n, t, _) => pushENamed env x n t
--- a/src/cjr_print.sml Sat May 16 15:55:15 2009 -0400 +++ b/src/cjr_print.sml Sat May 16 16:02:17 2009 -0400 @@ -2037,63 +2037,72 @@ newline]) xts, string "};"] end - | DDatatype (Enum, x, n, xncs) => - box [string "enum", - space, - string ("__uwe_" ^ ident x ^ "_" ^ Int.toString n), - space, - string "{", - space, - p_list_sep (box [string ",", space]) (fn (x, n, _) => - string ("__uwc_" ^ ident x ^ "_" ^ Int.toString n)) xncs, - space, - string "};"] - | DDatatype (Option, _, _, _) => box [] - | DDatatype (Default, x, n, xncs) => + | DDatatype dts => let - val xncsArgs = List.mapPartial (fn (x, n, NONE) => NONE - | (x, n, SOME t) => SOME (x, n, t)) xncs + val dts = ListMergeSort.sort (fn ((dk1, _, _, _), (dk2, _, _, _)) => + dk1 = Enum andalso dk2 <> Enum) dts + + fun p_one (Enum, x, n, xncs) = + box [string "enum", + space, + string ("__uwe_" ^ ident x ^ "_" ^ Int.toString n), + space, + string "{", + space, + p_list_sep (box [string ",", space]) (fn (x, n, _) => + string ("__uwc_" ^ ident x ^ "_" ^ Int.toString n)) xncs, + space, + string "};"] + | p_one (Option, _, _, _) = box [] + | p_one (Default, x, n, xncs) = + let + val xncsArgs = List.mapPartial (fn (x, n, NONE) => NONE + | (x, n, SOME t) => SOME (x, n, t)) xncs + in + box [string "enum", + space, + string ("__uwe_" ^ ident x ^ "_" ^ Int.toString n), + space, + string "{", + space, + p_list_sep (box [string ",", space]) (fn (x, n, _) => + string ("__uwc_" ^ ident x ^ "_" ^ Int.toString n)) + xncs, + space, + string "};", + newline, + newline, + string "struct", + space, + string ("__uwd_" ^ ident x ^ "_" ^ Int.toString n), + space, + string "{", + newline, + string "enum", + space, + string ("__uwe_" ^ ident x ^ "_" ^ Int.toString n), + space, + string "tag;", + newline, + box (case xncsArgs of + [] => [] + | _ => [string "union", + space, + string "{", + newline, + p_list_sep newline (fn (x, n, t) => box [p_typ env t, + space, + string ("uw_" ^ ident x), + string ";"]) xncsArgs, + newline, + string "}", + space, + string "data;", + newline]), + string "};"] + end in - box [string "enum", - space, - string ("__uwe_" ^ ident x ^ "_" ^ Int.toString n), - space, - string "{", - space, - p_list_sep (box [string ",", space]) (fn (x, n, _) => - string ("__uwc_" ^ ident x ^ "_" ^ Int.toString n)) xncs, - space, - string "};", - newline, - newline, - string "struct", - space, - string ("__uwd_" ^ ident x ^ "_" ^ Int.toString n), - space, - string "{", - newline, - string "enum", - space, - string ("__uwe_" ^ ident x ^ "_" ^ Int.toString n), - space, - string "tag;", - newline, - box (case xncsArgs of - [] => [] - | _ => [string "union", - space, - string "{", - newline, - p_list_sep newline (fn (x, n, t) => box [p_typ env t, - space, - string ("uw_" ^ ident x), - string ";"]) xncsArgs, - newline, - string "}", - space, - string "data;", - newline]), - string "};"] + p_list_sep (box []) p_one dts end | DDatatypeForward _ => box []
--- a/src/cjrize.sml Sat May 16 15:55:15 2009 -0400 +++ b/src/cjrize.sml Sat May 16 16:02:17 2009 -0400 @@ -483,22 +483,28 @@ fun cifyDecl ((d, loc), sm) = case d of - L.DDatatype _ => raise Fail "Cjrize DDatatype" - (*L.DDatatype (x, n, xncs) => + L.DDatatype dts => let - val dk = ElabUtil.classifyDatatype xncs - val (xncs, sm) = ListUtil.foldlMap (fn ((x, n, to), sm) => - case to of - NONE => ((x, n, NONE), sm) - | SOME t => - let - val (t, sm) = cifyTyp (t, sm) - in - ((x, n, SOME t), sm) - end) sm xncs + val (dts, sm) = ListUtil.foldlMap + (fn ((x, n, xncs), sm) => + let + val dk = ElabUtil.classifyDatatype xncs + val (xncs, sm) = ListUtil.foldlMap (fn ((x, n, to), sm) => + case to of + NONE => ((x, n, NONE), sm) + | SOME t => + let + val (t, sm) = cifyTyp (t, sm) + in + ((x, n, SOME t), sm) + end) sm xncs + in + ((dk, x, n, xncs), sm) + end) + sm dts in - (SOME (L'.DDatatype (dk, x, n, xncs), loc), NONE, sm) - end*) + (SOME (L'.DDatatype dts, loc), NONE, sm) + end | L.DVal (x, n, t, e, _) => let @@ -643,8 +649,9 @@ val (dop, pop, sm) = cifyDecl (d, sm) val dsF = case dop of - SOME (L'.DDatatype (dk, x, n, _), loc) => - (L'.DDatatypeForward (dk, x, n), loc) :: dsF + SOME (L'.DDatatype dts, loc) => + map (fn (dk, x, n, _) => + (L'.DDatatypeForward (dk, x, n), loc)) dts @ dsF | _ => dsF val dsF = map (fn v => (L'.DStruct v, ErrorMsg.dummySpan)) (Sm.declares sm)