diff src/elaborate.sml @ 78:a6d45c6819c9

Implicit structure members
author Adam Chlipala <adamc@hcoop.net>
date Sun, 29 Jun 2008 11:05:38 -0400
parents 522f4bd3955e
children 37847b504cc6
line wrap: on
line diff
--- a/src/elaborate.sml	Sun Jun 29 10:44:36 2008 -0400
+++ b/src/elaborate.sml	Sun Jun 29 11:05:38 2008 -0400
@@ -1569,13 +1569,56 @@
       | L.DStr (x, sgno, str) =>
         let
             val formal = Option.map (elabSgn env) sgno
-            val (str', actual) = elabStr env str
 
-            val sgn' = case formal of
-                           NONE => selfifyAt env {str = str', sgn = actual}
-                         | SOME formal =>
-                           (subSgn env actual formal;
-                            formal)
+            val (str', sgn') =
+                case formal of
+                    NONE =>
+                    let
+                        val (str', actual) = elabStr env str
+                    in
+                        (str', selfifyAt env {str = str', sgn = actual})
+                    end
+                  | SOME formal =>
+                    let
+                        val str =
+                            case #1 (hnormSgn env formal) of
+                                L'.SgnConst sgis =>
+                                (case #1 str of
+                                     L.StrConst ds =>
+                                     let
+                                         val needed = foldl (fn ((sgi, _), needed) =>
+                                                                case sgi of
+                                                                    L'.SgiConAbs (x, _, _) => SS.add (needed, x)
+                                                                  | _ => needed)
+                                                            SS.empty sgis
+                                                      
+                                         val needed = foldl (fn ((d, _), needed) =>
+                                                                case d of
+                                                                    L.DCon (x, _, _) => (SS.delete (needed, x)
+                                                                                         handle NotFound => needed)
+                                                                  | L.DOpen _ => SS.empty
+                                                                  | _ => needed)
+                                                            needed ds
+                                     in
+                                         case SS.listItems needed of
+                                             [] => str
+                                           | xs =>
+                                             let
+                                                 val kwild = (L.KWild, #2 str)
+                                                 val cwild = (L.CWild kwild, #2 str)
+                                                 val ds' = map (fn x => (L.DCon (x, NONE, cwild), #2 str)) xs
+                                             in
+                                                 (L.StrConst (ds @ ds'), #2 str)
+                                             end
+                                     end
+                                   | _ => str)
+                              | _ => str
+
+                        val (str', actual) = elabStr env str
+                    in
+                        subSgn env actual formal;
+                        (str', formal)
+                    end
 
             val (env', n) = E.pushStrNamed env x sgn'
         in