summaryrefslogtreecommitdiff
path: root/src/corify.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-08-09 08:47:36 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-08-09 08:47:36 -0400
commitbd2d0fe6c8deedc88d985b2c38978b730ff0cd19 (patch)
tree2daf2365908cb5776cc09bcfc90146e1984efb6f /src/corify.sml
parentb9b67597324deb6e6dfc8ef33c60c110abc2af7b (diff)
A multi-parameter datatype all the way through
Diffstat (limited to 'src/corify.sml')
-rw-r--r--src/corify.sml8
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