Mercurial > urweb
diff src/elaborate.sml @ 35:1dfbd9e3e790
Proper selfification
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 17 Jun 2008 17:08:28 -0400 |
parents | 44b5405e74c7 |
children | e3d3c2791105 |
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)