diff options
author | Adam Chlipala <adamc@hcoop.net> | 2008-08-09 08:47:36 -0400 |
---|---|---|
committer | Adam Chlipala <adamc@hcoop.net> | 2008-08-09 08:47:36 -0400 |
commit | bd2d0fe6c8deedc88d985b2c38978b730ff0cd19 (patch) | |
tree | 2daf2365908cb5776cc09bcfc90146e1984efb6f /src/corify.sml | |
parent | b9b67597324deb6e6dfc8ef33c60c110abc2af7b (diff) |
A multi-parameter datatype all the way through
Diffstat (limited to 'src/corify.sml')
-rw-r--r-- | src/corify.sml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/corify.sml b/src/corify.sml index 075939bf..9c350aee 100644 --- a/src/corify.sml +++ b/src/corify.sml @@ -534,11 +534,12 @@ structure St : sig val dk = CoreUtil.classifyDatatype xncs 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 k = (L'.KType, loc) val dcons = map (fn (x, n, to) => let - val args = ListUtil.mapi (fn (i, _) => (L'.CRel i, loc)) xs + val args = ListUtil.mapi (fn (i, _) => (L'.CRel (nxs - i), loc)) xs val (e, t) = case to of NONE => ((L'.ECon (dk, L'.PConVar n, args, NONE), loc), t) @@ -575,7 +576,8 @@ structure St : sig ((x, n, co), st) end) st xncs - val c = ListUtil.foldli (fn (i, _, c) => (L'.CApp (c, (L'.CRel i, loc)), loc)) c xs + val nxs = length xs - 1 + val c = ListUtil.foldli (fn (i, _, c) => (L'.CApp (c, (L'.CRel (nxs - i), loc)), loc)) c xs val k = (L'.KType, loc) val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs |