Mercurial > urweb
diff src/elaborate.sml @ 194:df5fd8f6913a
A multi-parameter datatype all the way through
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sat, 09 Aug 2008 08:47:36 -0400 |
| parents | aa54250f58ac |
| children | dd82457fda82 |
line wrap: on
line diff
--- a/src/elaborate.sml Fri Aug 08 17:55:51 2008 -0400 +++ b/src/elaborate.sml Sat Aug 09 08:47:36 2008 -0400 @@ -954,7 +954,8 @@ val k = (L'.KType, loc) val unifs = map (fn _ => cunif (loc, k)) xs - val t = ListUtil.foldli (fn (i, u, t) => subConInCon (i, u) t) t unifs + val nxs = length unifs - 1 + val t = ListUtil.foldli (fn (i, u, t) => subConInCon (nxs - i, u) t) t unifs val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs in ignore (checkPatCon (env, denv) p' pt t); @@ -1600,7 +1601,8 @@ val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs val (env, n) = E.pushCNamed env x k' NONE val t = (L'.CNamed n, loc) - val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel i, loc)), loc)) t xs + val nxs = length xs - 1 + val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs val (xcs, (used, env, gs)) = ListUtil.foldlMap @@ -2269,7 +2271,8 @@ val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs val (env, n) = E.pushCNamed env x k' NONE val t = (L'.CNamed n, loc) - val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel i, loc)), loc)) t xs + val nxs = length xs - 1 + val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs val (env', denv') = foldl (fn (x, (env', denv')) => (E.pushCRel env' x k,