diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2012-05-02 08:23:30 -0400 |
|---|---|---|
| committer | Adam Chlipala <adam@chlipala.net> | 2012-05-02 08:23:30 -0400 |
| commit | 59ea8e278e94c7ea7989a6ece4bbb1a99110e93f (patch) | |
| tree | 26303dd728d5c14aa23107593fda4ddf5e616110 | |
| parent | 31f7a291af3dea4e5a9d20def3e5443401d07a50 (diff) | |
In simplifying constructors for error messages, unfold constructor synonyms from modules
| -rw-r--r-- | src/elab_ops.sml | 16 | ||||
| -rw-r--r-- | tests/tcsimp.ur | 3 |
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 |