summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2012-05-02 08:23:30 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2012-05-02 08:23:30 -0400
commita612a0c55bed76b4192fb66ffeba43933bcfb6bf (patch)
tree26303dd728d5c14aa23107593fda4ddf5e616110
parent88ea557055dc5cb1dcb15aeb65d058132ac24e22 (diff)
In simplifying constructors for error messages, unfold constructor synonyms from modules
-rw-r--r--src/elab_ops.sml16
-rw-r--r--tests/tcsimp.ur3
2 files changed, 18 insertions, 1 deletions
diff --git a/src/elab_ops.sml b/src/elab_ops.sml
index 1546feef..6ff5e03a 100644
--- a/src/elab_ops.sml
+++ b/src/elab_ops.sml
@@ -336,7 +336,21 @@ fun reduceCon env (cAll as (c, loc)) =
(case E.lookupCNamed env xn of
(_, _, SOME c') => reduceCon env c'
| _ => cAll)
- | CModProj _ => cAll
+ | CModProj (n, ms, x) =>
+ let
+ val (_, sgn) = E.lookupStrNamed env n
+ val (str, sgn) = foldl (fn (m, (str, sgn)) =>
+ case E.projectStr env {sgn = sgn, str = str, field = m} of
+ NONE => raise Fail "reduceCon: Unknown substructure"
+ | SOME sgn => ((StrProj (str, m), loc), sgn))
+ ((StrVar n, loc), sgn) ms
+ in
+ case E.projectCon env {sgn = sgn, str = str, field = x} of
+ NONE => raise Fail "reduceCon: kindof: Unknown con in structure"
+ | SOME (_, NONE) => cAll
+ | SOME (_, SOME c) => reduceCon env c
+ end
+
| CApp (c1, c2) =>
let
val c1 = reduceCon env c1
diff --git a/tests/tcsimp.ur b/tests/tcsimp.ur
new file mode 100644
index 00000000..5e471e6e
--- /dev/null
+++ b/tests/tcsimp.ur
@@ -0,0 +1,3 @@
+val x : $(mapU string [A, B]) = {A = "hi", B = "bye"}
+
+val y = show x