diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/corify.sml | 12 | ||||
-rw-r--r-- | src/expl.sml | 4 | ||||
-rw-r--r-- | src/expl_env.sml | 76 | ||||
-rw-r--r-- | src/expl_print.sml | 14 | ||||
-rw-r--r-- | src/expl_util.sml | 31 | ||||
-rw-r--r-- | src/explify.sml | 16 |
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) => |