summaryrefslogtreecommitdiff
path: root/src/elaborate.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2010-06-13 10:55:20 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2010-06-13 10:55:20 -0400
commitab23256c70d97509cf4dea53fd9ec8969966cfa9 (patch)
tree59064e362b29f62b3790517e3bb247a63ad369c7 /src/elaborate.sml
parenta4ef3cc14bd6d90ad6ed58832fd77b4155d27105 (diff)
More generous wildification, covering map-records
Diffstat (limited to 'src/elaborate.sml')
-rw-r--r--src/elaborate.sml30
1 files changed, 22 insertions, 8 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index f219e2f2..505699bd 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -3281,15 +3281,29 @@ and wildifyStr env (str, sgn) =
| L'.SgiConstraint cs => naddConstraint (nd, (env', cs, loc))
| L'.SgiVal (x, _, t) =>
let
- val t = normClassConstraint env' t
+ fun should t =
+ let
+ val t = normClassConstraint env' t
+ in
+ case #1 t of
+ L'.CApp (f, _) => isClassOrFolder env' f
+ | L'.TRecord t =>
+ (case hnormCon env' t of
+ (L'.CApp (f, _), _) =>
+ (case hnormCon env' f of
+ (L'.CApp (f, cl), loc) =>
+ (case hnormCon env' f of
+ (L'.CMap _, _) => isClassOrFolder env' cl
+ | _ => false)
+ | _ => false)
+ | _ => false)
+ | _ => false
+ end
in
- case #1 t of
- L'.CApp (f, _) =>
- if isClassOrFolder env' f then
- naddVal (nd, x)
- else
- nd
- | _ => nd
+ if should t then
+ naddVal (nd, x)
+ else
+ nd
end
| L'.SgiStr (x, _, s) =>
(case #1 (hnormSgn env' s) of