diff src/elab_ops.sml @ 1735:ec47f49c6aa3

In simplifying constructors for error messages, unfold constructor synonyms from modules
author Adam Chlipala <adam@chlipala.net>
date Wed, 02 May 2012 08:23:30 -0400
parents dd12d6d9e9a7
children
line wrap: on
line diff
--- a/src/elab_ops.sml	Sun Apr 29 20:37:45 2012 -0400
+++ b/src/elab_ops.sml	Wed May 02 08:23:30 2012 -0400
@@ -336,7 +336,21 @@
         (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