summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-05-16 16:02:17 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-05-16 16:02:17 -0400
commit2396dd1bd2bdaeb7608d88bbb2f890b5788852c0 (patch)
treedf44fd4952ee16f262cce3e4a063352e534aee25 /src
parent30b78a96ae699fa2282c07a2dbf3e6303f99e32c (diff)
Mutual datatypes through Cjrize
Diffstat (limited to 'src')
-rw-r--r--src/cjr.sml2
-rw-r--r--src/cjr_env.sml19
-rw-r--r--src/cjr_print.sml119
-rw-r--r--src/cjrize.sml43
4 files changed, 100 insertions, 83 deletions
diff --git a/src/cjr.sml b/src/cjr.sml
index 6728e5c8..2b81de1a 100644
--- a/src/cjr.sml
+++ b/src/cjr.sml
@@ -100,7 +100,7 @@ withtype exp = exp' located
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
diff --git a/src/cjr_env.sml b/src/cjr_env.sml
index 54dbea17..217efb3a 100644
--- a/src/cjr_env.sml
+++ b/src/cjr_env.sml
@@ -137,15 +137,16 @@ fun classifyDatatype xncs =
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
diff --git a/src/cjr_print.sml b/src/cjr_print.sml
index 85e1c3f7..7f5dccde 100644
--- a/src/cjr_print.sml
+++ b/src/cjr_print.sml
@@ -2037,63 +2037,72 @@ fun p_decl env (dAll as (d, _) : decl) =
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 []
diff --git a/src/cjrize.sml b/src/cjrize.sml
index 9c2128bc..c4d916eb 100644
--- a/src/cjrize.sml
+++ b/src/cjrize.sml
@@ -483,22 +483,28 @@ fun cifyExp (eAll as (e, loc), sm) =
fun cifyDecl ((d, loc), sm) =
case d of
- L.DDatatype _ => raise Fail "Cjrize DDatatype"
- (*L.DDatatype (x, n, xncs) =>
- 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
- (SOME (L'.DDatatype (dk, x, n, xncs), loc), NONE, sm)
- end*)
+ L.DDatatype dts =>
+ let
+ 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 dts, loc), NONE, sm)
+ end
| L.DVal (x, n, t, e, _) =>
let
@@ -643,8 +649,9 @@ fun cjrize ds =
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)