aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-08-25 17:12:21 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-08-25 17:12:21 -0400
commitf9d6e7f4d4e5f1c01fd10bf82232a938b930147f (patch)
tree5440f09ee20da6c2b64304679e7f9bc26f1d27e1
parentc2390ec66aed4fe73a7641ccc2141b0aec5aa733 (diff)
Fix structure wildification to take concrete con decls into account
-rw-r--r--src/elaborate.sml17
1 files changed, 14 insertions, 3 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 0a15dab1..b55aa61c 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -3086,6 +3086,7 @@ and wildifyStr env (str, sgn) =
(SOME c1, SOME c2) => SOME (L.CConcat (c1, c2), loc)
| _ => NONE)
| L'.CUnit => SOME (L.CUnit, loc)
+ | L'.CUnif (_, _, _, ref (SOME c)) => decompileCon env c
| _ => NONE
@@ -3094,7 +3095,9 @@ and wildifyStr env (str, sgn) =
let
val (needed, constraints, neededV) =
case sgi of
- L'.SgiConAbs (x, _, k) => (SM.insert (neededC, x, k), constraints, neededV)
+ L'.SgiCon (x, _, k, c) => (SM.insert (neededC, x, (k, SOME c)),
+ constraints, neededV)
+ | L'.SgiConAbs (x, _, k) => (SM.insert (neededC, x, (k, NONE)), constraints, neededV)
| L'.SgiConstraint cs => (neededC, (env', cs, loc) :: constraints, neededV)
| L'.SgiVal (x, _, t) =>
@@ -3154,15 +3157,23 @@ and wildifyStr env (str, sgn) =
[] => ds'
| xs =>
let
- val ds'' = map (fn (x, k) =>
+ val ds'' = map (fn (x, (k, co)) =>
let
val k =
case decompileKind k of
NONE => (L.KWild, #2 str)
| SOME k => k
+
val cwild = (L.CWild k, #2 str)
+ val c =
+ case co of
+ NONE => cwild
+ | SOME c =>
+ case decompileCon env c of
+ NONE => cwild
+ | SOME c' => c'
in
- (L.DCon (x, NONE, cwild), #2 str)
+ (L.DCon (x, NONE, c), #2 str)
end) xs
in
ds'' @ ds'