Mercurial > urweb
diff src/expl_env.sml @ 806:0e554bfd6d6a
Mutual datatypes through Corify
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sat, 16 May 2009 15:22:05 -0400 |
parents | 8688e01ae469 |
children | b2311dfb3158 |
line wrap: on
line diff
--- a/src/expl_env.sml Sat May 16 15:14:17 2009 -0400 +++ b/src/expl_env.sml Sat May 16 15:22:05 2009 -0400 @@ -255,22 +255,33 @@ 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 @@ 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