summaryrefslogtreecommitdiff
path: root/src/elaborate.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-09-14 15:10:04 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-09-14 15:10:04 -0400
commit8cc7053b00237cd468290cb5f2042898e7a80329 (patch)
tree0138b56c392844cd8033fa03e81715b8b1ca4f8a /src/elaborate.sml
parentc81c24b4feb3fae3c13861f1bcaafab697a6bb7e (diff)
Crud supports INSERT
Diffstat (limited to 'src/elaborate.sml')
-rw-r--r--src/elaborate.sml28
1 files changed, 21 insertions, 7 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 0c313f14..70404cf1 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1019,9 +1019,11 @@ fun elabHead (env, denv) (e as (_, loc)) t =
let
val u = cunif (loc, k)
- val (e, t, gs') = unravel (subConInCon (0, u) t',
- (L'.ECApp (e, u), loc))
+ val t'' = subConInCon (0, u) t'
+ val (e, t, gs') = unravel (t'', (L'.ECApp (e, u), loc))
in
+ (*prefaces "Unravel" [("t'", p_con env t'),
+ ("t''", p_con env t'')];*)
(e, t, enD gs @ gs')
end
| _ => (e, t, enD gs)
@@ -1477,7 +1479,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
let
val () = checkKind env c' ck k
val eb' = subConInCon (0, c') eb
- handle SynUnif => (expError env (Unif ("substitution", eb));
+ handle SynUnif => (expError env (Unif ("substitution", loc, eb));
cerror)
in
(*prefaces "Elab ECApp" [("e", SourcePrint.p_exp eAll),
@@ -1489,10 +1491,6 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
((L'.ECApp (e', c'), loc), eb', gs1 @ gs2 @ enD gs3 @ enD gs4)
end
- | L'.CUnif _ =>
- (expError env (Unif ("application", et));
- (eerror, cerror, []))
-
| _ =>
(expError env (WrongForm ("constructor function", e', et));
(eerror, cerror, []))
@@ -1586,6 +1584,22 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
((L'.EField (e', c', {field = ft, rest = rest}), loc), ft, gs1 @ enD gs2 @ enD gs3 @ enD gs4)
end
+ | L.EWith (e1, c, e2) =>
+ let
+ val (e1', e1t, gs1) = elabExp (env, denv) e1
+ val (c', ck, gs2) = elabCon (env, denv) c
+ val (e2', e2t, gs3) = elabExp (env, denv) e2
+
+ val rest = cunif (loc, ktype_record)
+ val first = (L'.CRecord (ktype, [(c', e2t)]), loc)
+
+ val gs4 = checkCon (env, denv) e1' e1t (L'.TRecord rest, loc)
+ val gs5 = D.prove env denv (first, rest, loc)
+ in
+ ((L'.EWith (e1', c', e2', {field = e2t, rest = rest}), loc),
+ (L'.TRecord ((L'.CConcat (first, rest), loc)), loc),
+ gs1 @ enD gs2 @ gs3 @ enD gs4 @ enD gs5)
+ end
| L.ECut (e, c) =>
let
val (e', et, gs1) = elabExp (env, denv) e