Mercurial > urweb
changeset 35:1dfbd9e3e790
Proper selfification
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 17 Jun 2008 17:08:28 -0400 |
parents | 44b5405e74c7 |
children | ca58de3cb72b |
files | src/elaborate.sml tests/modproj.lac |
diffstat | 2 files changed, 51 insertions(+), 11 deletions(-) [+] |
line wrap: on
line diff
--- a/src/elaborate.sml Tue Jun 17 16:38:54 2008 -0400 +++ b/src/elaborate.sml Tue Jun 17 17:08:28 2008 -0400 @@ -1105,15 +1105,19 @@ | L'.DSgn _ => NONE | L'.DStr (x, n, sgn, _) => SOME (L'.SgiStr (x, n, sgn), loc) -fun subSgn env (all1 as (sgn1, _)) (all2 as (sgn2, loc2)) = - case (sgn1, sgn2) of +fun hnormSgn env (all as (sgn, _)) = + case sgn of + L'.SgnError => all + | L'.SgnVar n => hnormSgn env (#2 (E.lookupSgnNamed env n)) + | L'.SgnConst _ => all + +fun subSgn env sgn1 (sgn2 as (_, loc2)) = + case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of (L'.SgnError, _) => () | (_, L'.SgnError) => () - | (L'.SgnVar n, _) => - subSgn env (#2 (E.lookupSgnNamed env n)) all2 - | (_, L'.SgnVar n) => - subSgn env all1 (#2 (E.lookupSgnNamed env n)) + | (L'.SgnVar n, _) => raise Fail "subSgn: Variable remains" + | (_, L'.SgnVar n) => raise Fail "subSgn: Variable remains" | (L'.SgnConst sgis1, L'.SgnConst sgis2) => let @@ -1195,6 +1199,18 @@ ignore (foldl folder env sgis2) end +fun selfify env {str, strs, sgn} = + case #1 (hnormSgn env sgn) of + L'.SgnError => sgn + | L'.SgnVar _ => sgn + + | L'.SgnConst sgis => + (L'.SgnConst (map (fn (L'.SgiConAbs (x, n, k), loc) => + (L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc) + | (L'.SgiStr (x, n, sgn), loc) => + (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc) + | x => x) sgis), #2 sgn) + fun elabDecl ((d, loc), env) = let @@ -1279,8 +1295,20 @@ val formal = Option.map (elabSgn env) sgno val (str', actual) = elabStr env str + fun self (str, _) = + case str of + L'.StrVar x => SOME (x, []) + | L'.StrProj (str, x) => + (case self str of + NONE => NONE + | SOME (m, ms) => SOME (m, ms @ [x])) + | _ => NONE + val sgn' = case formal of - NONE => actual + NONE => + (case self str' of + NONE => actual + | SOME (str, strs) => selfify env {sgn = actual, str = str, strs = strs}) | SOME formal => (subSgn env actual formal; formal)
--- a/tests/modproj.lac Tue Jun 17 16:38:54 2008 -0400 +++ b/tests/modproj.lac Tue Jun 17 17:08:28 2008 -0400 @@ -1,11 +1,23 @@ -signature S = sig +signature S1 = sig type t val zero : t end -structure S : S = struct +signature S2 = sig + type t = int + val zero : t +end +structure S = struct type t = int val zero = 0 end +structure S1 : S1 = S +structure S2 : S2 = S -type t = S.t -val zero : t = S.zero +type t = S1.t +val zero : t = S1.zero + +type t = S2.t +val zero : int = S2.zero + +structure T = S1 +val zero : S1.t = T.zero