summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-06-29 11:05:38 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-06-29 11:05:38 -0400
commitc8f3f6b28d235722dc56a4df73e43e802bdbd67d (patch)
treec133857b23ef592fe2d9c40080e7dfd3c52430aa /src
parentb7f84c57522b12bdbd4a7056e5d4f58009a48c95 (diff)
Implicit structure members
Diffstat (limited to 'src')
-rw-r--r--src/elaborate.sml55
1 files changed, 49 insertions, 6 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 307af12e..e9d8d925 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1569,13 +1569,56 @@ fun elabDecl ((d, loc), env) =
| 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