From a612a0c55bed76b4192fb66ffeba43933bcfb6bf Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Wed, 2 May 2012 08:23:30 -0400 Subject: In simplifying constructors for error messages, unfold constructor synonyms from modules --- src/elab_ops.sml | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) (limited to 'src/elab_ops.sml') 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 -- cgit v1.2.3