summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-05-16 15:22:05 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-05-16 15:22:05 -0400
commit6cb3888614811abc30c6a00a1644e256d1d1c780 (patch)
tree2880c44d43f0095ce5c1ac7531a4cdff3ce4b730 /src
parent0159bec5067ac88f3f222595ac6f5e2f94c1d41f (diff)
Mutual datatypes through Corify
Diffstat (limited to 'src')
-rw-r--r--src/corify.sml12
-rw-r--r--src/expl.sml4
-rw-r--r--src/expl_env.sml76
-rw-r--r--src/expl_print.sml14
-rw-r--r--src/expl_util.sml31
-rw-r--r--src/explify.sml16
6 files changed, 93 insertions, 60 deletions
diff --git a/src/corify.sml b/src/corify.sml
index 65f32fc2..9ac5c84e 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -621,7 +621,8 @@ fun corifyDecl mods (all as (d, loc : EM.span), st) =
in
([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st)
end
- | L.DDatatype (x, n, xs, xncs) =>
+ | L.DDatatype _ => raise Fail "Corify DDatatype"
+ (*| L.DDatatype (x, n, xs, xncs) =>
let
val (st, n) = St.bindCon st x n
val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) =>
@@ -658,7 +659,7 @@ fun corifyDecl mods (all as (d, loc : EM.span), st) =
end) xncs
in
((L'.DDatatype (x, n, xs, xncs), loc) :: dcons, st)
- end
+ end*)
| L.DDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
let
val (st, n) = St.bindCon st x n
@@ -795,7 +796,8 @@ fun corifyDecl mods (all as (d, loc : EM.span), st) =
trans)
end
- | L.SgiDatatype (x, n, xs, xnts) =>
+ | L.SgiDatatype _ => raise Fail "Corify SgiDatatype"
+ (*| L.SgiDatatype (x, n, xs, xnts) =>
let
val k = (L'.KType, loc)
val dk = ElabUtil.classifyDatatype xnts
@@ -856,7 +858,7 @@ fun corifyDecl mods (all as (d, loc : EM.span), st) =
conmap,
st,
trans)
- end
+ end*)
| L.SgiVal (x, _, c) =>
let
@@ -1061,7 +1063,7 @@ and corifyStr mods ((str, _), st) =
fun maxName ds = foldl (fn ((d, _), n) =>
case d of
L.DCon (_, n', _, _) => Int.max (n, n')
- | L.DDatatype (_, n', _, _) => Int.max (n, n')
+ | L.DDatatype dts => foldl (fn ((_, n', _, _), n) => Int.max (n, n')) n dts
| L.DDatatypeImp (_, n', _, _, _, _, _) => Int.max (n, n')
| L.DVal (_, n', _, _) => Int.max (n, n')
| L.DValRec vis => foldl (fn ((_, n', _, _), n) => Int.max (n, n)) n vis
diff --git a/src/expl.sml b/src/expl.sml
index cc40e8b4..4a9acd8a 100644
--- a/src/expl.sml
+++ b/src/expl.sml
@@ -115,7 +115,7 @@ withtype exp = exp' located
datatype sgn_item' =
SgiConAbs of string * int * kind
| SgiCon of string * int * kind * con
- | SgiDatatype of string * int * string list * (string * int * con option) list
+ | SgiDatatype of (string * int * string list * (string * int * con option) list) list
| SgiDatatypeImp of string * int * int * string list * string * string list * (string * int * con option) list
| SgiVal of string * int * con
| SgiSgn of string * int * sgn
@@ -133,7 +133,7 @@ and sgn = sgn' located
datatype decl' =
DCon of string * int * kind * con
- | DDatatype of string * int * string list * (string * int * con option) list
+ | DDatatype of (string * int * string list * (string * int * con option) list) list
| DDatatypeImp of string * int * int * string list * string * string list * (string * int * con option) list
| DVal of string * int * con * exp
| DValRec of (string * int * con * exp) list
diff --git a/src/expl_env.sml b/src/expl_env.sml
index 2bb049a3..836af42c 100644
--- a/src/expl_env.sml
+++ b/src/expl_env.sml
@@ -255,22 +255,33 @@ fun lookupStrNamed (env : env) n =
fun declBinds env (d, loc) =
case d of
DCon (x, n, k, c) => pushCNamed env x n k (SOME c)
- | DDatatype (x, n, xs, xncs) =>
+ | DDatatype dts =>
let
- val env = pushCNamed env x n (KType, loc) NONE
+ fun doOne ((x, n, xs, xncs), env) =
+ let
+ val k = (KType, loc)
+ val nxs = length xs
+ val (tb, kb) = ListUtil.foldli (fn (i, x', (tb, kb)) =>
+ ((CApp (tb, (CRel (nxs - i - 1), loc)), loc),
+ (KArrow (k, kb), loc)))
+ ((CNamed n, loc), k) xs
+
+ val env = pushCNamed env x n kb NONE
+ in
+ foldl (fn ((x', n', to), env) =>
+ let
+ val t =
+ case to of
+ NONE => tb
+ | SOME t => (TFun (t, tb), loc)
+ val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs
+ in
+ pushENamed env x' n' t
+ end)
+ env xncs
+ end
in
- foldl (fn ((x', n', to), env) =>
- let
- val t =
- case to of
- NONE => (CNamed n, loc)
- | SOME t => (TFun (t, (CNamed n, loc)), loc)
- val k = (KType, loc)
- val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs
- in
- pushENamed env x' n' t
- end)
- env xncs
+ foldl doOne env dts
end
| DDatatypeImp (x, n, m, ms, x', xs, xncs) =>
let
@@ -337,22 +348,31 @@ fun sgiBinds env (sgi, loc) =
case sgi of
SgiConAbs (x, n, k) => pushCNamed env x n k NONE
| SgiCon (x, n, k, c) => pushCNamed env x n k (SOME c)
- | SgiDatatype (x, n, xs, xncs) =>
+ | SgiDatatype dts =>
let
- val env = pushCNamed env x n (KType, loc) NONE
+ fun doOne ((x, n, xs, xncs), env) =
+ let
+ val k = (KType, loc)
+ val k' = foldr (fn (_, k') => (KArrow (k, k'), loc)) k xs
+
+ val env = pushCNamed env x n k' NONE
+ in
+ foldl (fn ((x', n', to), env) =>
+ let
+ val t =
+ case to of
+ NONE => (CNamed n, loc)
+ | SOME t => (TFun (t, (CNamed n, loc)), loc)
+
+ val k = (KType, loc)
+ val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs
+ in
+ pushENamed env x' n' t
+ end)
+ env xncs
+ end
in
- foldl (fn ((x', n', to), env) =>
- let
- val t =
- case to of
- NONE => (CNamed n, loc)
- | SOME t => (TFun (t, (CNamed n, loc)), loc)
- val k = (KType, loc)
- val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs
- in
- pushENamed env x' n' t
- end)
- env xncs
+ foldl doOne env dts
end
| SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
let
diff --git a/src/expl_print.sml b/src/expl_print.sml
index 7aa36c6d..0783facc 100644
--- a/src/expl_print.sml
+++ b/src/expl_print.sml
@@ -460,9 +460,7 @@ fun p_datatype env (x, n, xs, cons) =
val env = E.pushCNamed env x n k NONE
val env = foldl (fn (x, env) => E.pushCRel env x k) env xs
in
- box [string "datatype",
- space,
- string x,
+ box [string x,
p_list_sep (box []) (fn x => box [space, string x]) xs,
space,
string "=",
@@ -475,7 +473,7 @@ fun p_datatype env (x, n, xs, cons) =
cons]
end
-fun p_sgn_item env (sgi, _) =
+fun p_sgn_item env (sgiAll as (sgi, _)) =
case sgi of
SgiConAbs (x, n, k) => box [string "con",
space,
@@ -495,7 +493,9 @@ fun p_sgn_item env (sgi, _) =
string "=",
space,
p_con env c]
- | SgiDatatype x => p_datatype env x
+ | SgiDatatype x => box [string "datatype",
+ space,
+ p_list_sep (box [space, string "and", space]) (p_datatype (E.sgiBinds env sgiAll)) x]
| SgiDatatypeImp (x, _, m1, ms, x', _, _) =>
let
val m1x = #1 (E.lookupStrNamed env m1)
@@ -609,7 +609,9 @@ fun p_decl env (dAll as (d, _) : decl) =
string "=",
space,
p_con env c]
- | DDatatype x => p_datatype env x
+ | DDatatype x => box [string "datatype",
+ space,
+ p_list_sep (box [space, string "and", space]) (p_datatype (E.declBinds env dAll)) x]
| DDatatypeImp (x, _, m1, ms, x', _, _) =>
let
val m1x = #1 (E.lookupStrNamed env m1)
diff --git a/src/expl_util.sml b/src/expl_util.sml
index 9e150b87..1932d52d 100644
--- a/src/expl_util.sml
+++ b/src/expl_util.sml
@@ -453,15 +453,17 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
S.map2 (con ctx c,
fn c' =>
(SgiCon (x, n, k', c'), loc)))
- | SgiDatatype (x, n, xs, xncs) =>
- S.map2 (ListUtil.mapfold (fn (x, n, c) =>
- case c of
- NONE => S.return2 (x, n, c)
- | SOME c =>
- S.map2 (con ctx c,
- fn c' => (x, n, SOME c'))) xncs,
- fn xncs' =>
- (SgiDatatype (x, n, xs, xncs'), loc))
+ | SgiDatatype dts =>
+ S.map2 (ListUtil.mapfold (fn (x, n, xs, xncs) =>
+ S.map2 (ListUtil.mapfold (fn (x, n, c) =>
+ case c of
+ NONE => S.return2 (x, n, c)
+ | SOME c =>
+ S.map2 (con ctx c,
+ fn c' => (x, n, SOME c'))) xncs,
+ fn xncs' => (x, n, xs, xncs'))) dts,
+ fn dts' =>
+ (SgiDatatype dts', loc))
| SgiDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
S.map2 (ListUtil.mapfold (fn (x, n, c) =>
case c of
@@ -496,8 +498,15 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
bind (ctx, NamedC (x, k))
| SgiCon (x, _, k, _) =>
bind (ctx, NamedC (x, k))
- | SgiDatatype (x, n, _, xncs) =>
- bind (ctx, NamedC (x, (KType, loc)))
+ | SgiDatatype dts =>
+ foldl (fn ((x, _, ks, _), ctx) =>
+ let
+ val k' = (KType, loc)
+ val k = foldl (fn (_, k) => (KArrow (k', k), loc))
+ k' ks
+ in
+ bind (ctx, NamedC (x, k))
+ end) ctx dts
| SgiDatatypeImp (x, _, _, _, _, _, _) =>
bind (ctx, NamedC (x, (KType, loc)))
| SgiVal _ => ctx
diff --git a/src/explify.sml b/src/explify.sml
index 145fccd2..d8bd6bff 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -137,10 +137,10 @@ fun explifySgi (sgi, loc) =
case sgi of
L.SgiConAbs (x, n, k) => SOME (L'.SgiConAbs (x, n, explifyKind k), loc)
| L.SgiCon (x, n, k, c) => SOME (L'.SgiCon (x, n, explifyKind k, explifyCon c), loc)
- (*| L.SgiDatatype (x, n, xs, xncs) => SOME (L'.SgiDatatype (x, n, xs,
- map (fn (x, n, co) =>
- (x, n, Option.map explifyCon co)) xncs), loc)*)
- | L.SgiDatatype _ => raise Fail "Explify SgiDatatype"
+ | L.SgiDatatype dts => SOME (L'.SgiDatatype (map (fn (x, n, xs, xncs) =>
+ (x, n, xs,
+ map (fn (x, n, co) =>
+ (x, n, Option.map explifyCon co)) xncs)) dts), loc)
| L.SgiDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
SOME (L'.SgiDatatypeImp (x, n, m1, ms, s, xs, map (fn (x, n, co) =>
(x, n, Option.map explifyCon co)) xncs), loc)
@@ -164,10 +164,10 @@ and explifySgn (sgn, loc) =
fun explifyDecl (d, loc : EM.span) =
case d of
L.DCon (x, n, k, c) => SOME (L'.DCon (x, n, explifyKind k, explifyCon c), loc)
- (*| L.DDatatype (x, n, xs, xncs) => SOME (L'.DDatatype (x, n, xs,
- map (fn (x, n, co) =>
- (x, n, Option.map explifyCon co)) xncs), loc)*)
- | L.DDatatype _ => raise Fail "Explify DDatatype"
+ | L.DDatatype dts => SOME (L'.DDatatype (map (fn (x, n, xs, xncs) =>
+ (x, n, xs,
+ map (fn (x, n, co) =>
+ (x, n, Option.map explifyCon co)) xncs)) dts), loc)
| L.DDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
SOME (L'.DDatatypeImp (x, n, m1, ms, s, xs,
map (fn (x, n, co) =>