diff options
author | Adam Chlipala <adamc@hcoop.net> | 2008-06-29 11:05:38 -0400 |
---|---|---|
committer | Adam Chlipala <adamc@hcoop.net> | 2008-06-29 11:05:38 -0400 |
commit | c8f3f6b28d235722dc56a4df73e43e802bdbd67d (patch) | |
tree | c133857b23ef592fe2d9c40080e7dfd3c52430aa /src | |
parent | b7f84c57522b12bdbd4a7056e5d4f58009a48c95 (diff) |
Implicit structure members
Diffstat (limited to 'src')
-rw-r--r-- | src/elaborate.sml | 55 |
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 |