summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-09-07 10:13:02 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-09-07 10:13:02 -0400
commit79c2e18d5d237d48f0803bb874d72b4354ba9b25 (patch)
tree3766580321bca3f077b2115ec5cbcd30dd9312a4 /src
parent700a48cc6e78f75166b6e322207a29981782c4e3 (diff)
intToString
Diffstat (limited to 'src')
-rw-r--r--src/c/urweb.c11
-rw-r--r--src/elaborate.sml8
2 files changed, 17 insertions, 2 deletions
diff --git a/src/c/urweb.c b/src/c/urweb.c
index c5f3a716..78a8e0f8 100644
--- a/src/c/urweb.c
+++ b/src/c/urweb.c
@@ -670,3 +670,14 @@ char *lw_Basis_ensqlBool(lw_Basis_bool b) {
else
return (char *)&true;
}
+
+lw_Basis_string lw_Basis_intToString(lw_context ctx, lw_Basis_int n) {
+ int len;
+ char *r;
+
+ lw_check_heap(ctx, INTS_MAX);
+ r = ctx->heap_front;
+ sprintf(r, "%lld%n", n, &len);
+ ctx->heap_front += len+1;
+ return r;
+}
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 5770fe5b..bf6137b5 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1923,6 +1923,10 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
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,
+ D.enter denv')) (env, denv) xs
+
val (xcs, (used, env, gs)) =
ListUtil.foldlMap
(fn ((x, to), (used, env, gs)) =>
@@ -1931,9 +1935,9 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
NONE => (NONE, t, gs)
| SOME t' =>
let
- val (t', tk, gs') = elabCon (env, denv) t'
+ val (t', tk, gs') = elabCon (env', denv') t'
in
- checkKind env t' tk k;
+ checkKind env' t' tk k;
(SOME t', (L'.TFun (t', t), loc), gs' @ gs)
end
val t = foldl (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) t xs