summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2013-08-19 12:38:43 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2013-08-19 12:38:43 -0400
commit2381ce64a2360a35fe37f23b97bd40760dc8f82a (patch)
tree716b2e80fc50d94f43e6543a244c67ca906131bd
parentbcaa5ca71b45500fa2df7ca1d19202fe7807ab36 (diff)
Potentially exponential search through where to head-normalize in [decompileCon]
-rw-r--r--src/elaborate.sml17
1 files changed, 13 insertions, 4 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 18010244..45aca382 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -3553,11 +3553,16 @@ and wildifyStr env (str, sgn) =
| L'.KFun _ => NONE
fun maybeHnorm env c =
- hnormCon env c
- handle E.UnboundNamed _ => c
+ hnormCon env c
+ handle E.UnboundNamed _ => c
- fun decompileCon env (c as (_, loc)) =
- case #1 (maybeHnorm env c) of
+ fun decompileCon env c =
+ case decompileCon' env c of
+ SOME v => SOME v
+ | NONE => decompileCon' env (maybeHnorm env c)
+
+ and decompileCon' env (c as (_, loc)) =
+ case #1 c of
L'.CRel i =>
let
val (s, _) = E.lookupCRel env i
@@ -3619,6 +3624,10 @@ and wildifyStr env (str, sgn) =
end
| L'.CMap _ => SOME (L.CMap, loc)
+ | L'.TRecord c =>
+ (case decompileCon env c of
+ NONE => NONE
+ | SOME c' => SOME (L.TRecord c', loc))
| c => (Print.preface ("WTF?", p_con env (c, loc)); NONE)