summaryrefslogtreecommitdiff
path: root/src/elaborate.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-11-11 19:20:37 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-11-11 19:20:37 -0500
commit1c1a33420c69bd2c75aa9986830020869e983e6e (patch)
tree99c1c46f59df9c378621aa8d05b072d50a81698e /src/elaborate.sml
parent1d3089850988710149c0fd8d4a72aa3339e6caca (diff)
Add CutMulti
Diffstat (limited to 'src/elaborate.sml')
-rw-r--r--src/elaborate.sml67
1 files changed, 58 insertions, 9 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 70429c1b..e3d334eb 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1664,6 +1664,21 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
((L'.ECut (e', c', {field = ft, rest = rest}), loc), (L'.TRecord rest, loc),
gs1 @ enD gs2 @ enD gs3 @ enD gs4)
end
+ | L.ECutMulti (e, c) =>
+ let
+ val (e', et, gs1) = elabExp (env, denv) e
+ val (c', ck, gs2) = elabCon (env, denv) c
+
+ val rest = cunif (loc, ktype_record)
+
+ val gs3 =
+ checkCon (env, denv) e' et
+ (L'.TRecord (L'.CConcat (c', rest), loc), loc)
+ val gs4 = D.prove env denv (c', rest, loc)
+ in
+ ((L'.ECutMulti (e', c', {rest = rest}), loc), (L'.TRecord rest, loc),
+ gs1 @ enD gs2 @ enD gs3 @ enD gs4)
+ end
| L.EFold =>
let
@@ -2694,6 +2709,33 @@ fun wildifyStr env (str, sgn) =
(case #1 str of
L.StrConst ds =>
let
+ fun decompileKind (k, loc) =
+ case k of
+ L'.KType => SOME (L.KType, loc)
+ | L'.KArrow (k1, k2) =>
+ (case (decompileKind k1, decompileKind k2) of
+ (SOME k1, SOME k2) => SOME (L.KArrow (k1, k2), loc)
+ | _ => NONE)
+ | L'.KName => SOME (L.KName, loc)
+ | L'.KRecord k =>
+ (case decompileKind k of
+ SOME k => SOME (L.KRecord k, loc)
+ | _ => NONE)
+ | L'.KUnit => SOME (L.KUnit, loc)
+ | L'.KTuple ks =>
+ let
+ val ks' = List.mapPartial decompileKind ks
+ in
+ if length ks' = length ks then
+ SOME (L.KTuple ks', loc)
+ else
+ NONE
+ end
+
+ | L'.KError => NONE
+ | L'.KUnif (_, _, ref (SOME k)) => decompileKind k
+ | L'.KUnif _ => NONE
+
fun decompileCon env (c, loc) =
case c of
L'.CRel i =>
@@ -2741,7 +2783,7 @@ fun wildifyStr env (str, sgn) =
let
val (needed, constraints, neededV) =
case sgi of
- L'.SgiConAbs (x, _, _) => (SS.add (neededC, x), constraints, neededV)
+ L'.SgiConAbs (x, _, k) => (SM.insert (neededC, x, k), constraints, neededV)
| L'.SgiConstraint cs => (neededC, (env', cs, loc) :: constraints, neededV)
| L'.SgiVal (x, _, t) =>
@@ -2764,18 +2806,18 @@ fun wildifyStr env (str, sgn) =
in
(needed, constraints, neededV, E.sgiBinds env' (sgi, loc))
end)
- (SS.empty, [], SS.empty, env) sgis
+ (SM.empty, [], SS.empty, env) sgis
val (neededC, neededV) = foldl (fn ((d, _), needed as (neededC, neededV)) =>
case d of
- L.DCon (x, _, _) => ((SS.delete (neededC, x), neededV)
+ L.DCon (x, _, _) => ((#1 (SM.remove (neededC, x)), neededV)
handle NotFound =>
needed)
- | L.DClass (x, _) => ((SS.delete (neededC, x), neededV)
+ | L.DClass (x, _) => ((#1 (SM.remove (neededC, x)), neededV)
handle NotFound => needed)
| L.DVal (x, _, _) => ((neededC, SS.delete (neededV, x))
handle NotFound => needed)
- | L.DOpen _ => (SS.empty, SS.empty)
+ | L.DOpen _ => (SM.empty, SS.empty)
| _ => needed)
(neededC, neededV) ds
@@ -2797,13 +2839,20 @@ fun wildifyStr env (str, sgn) =
end
val ds' =
- case SS.listItems neededC of
+ case SM.listItemsi neededC of
[] => ds'
| xs =>
let
- val kwild = (L.KWild, #2 str)
- val cwild = (L.CWild kwild, #2 str)
- val ds'' = map (fn x => (L.DCon (x, NONE, cwild), #2 str)) xs
+ val ds'' = map (fn (x, k) =>
+ let
+ val k =
+ case decompileKind k of
+ NONE => (L.KWild, #2 str)
+ | SOME k => k
+ val cwild = (L.CWild k, #2 str)
+ in
+ (L.DCon (x, NONE, cwild), #2 str)
+ end) xs
in
ds'' @ ds'
end