From d6cee9f01237ec6c6ebb2843a33eda0da89fd5bb Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 6 Jan 2011 19:26:31 -0500 Subject: Handle opening of modules that define signatures --- src/elaborate.sml | 21 ++++++++++++--------- 1 file changed, 12 insertions(+), 9 deletions(-) (limited to 'src') diff --git a/src/elaborate.sml b/src/elaborate.sml index 4e59a8ed..3dc351b7 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -2682,15 +2682,18 @@ and selfify env {str, strs, sgn} = | L'.SgnVar _ => sgn | L'.SgnConst sgis => - (L'.SgnConst (ListUtil.mapConcat (fn (L'.SgiConAbs (x, n, k), loc) => - [(L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)] - | (L'.SgiDatatype dts, loc) => - map (fn (x, n, xs, xncs) => (L'.SgiDatatypeImp (x, n, str, strs, x, xs, xncs), loc)) dts - | (L'.SgiClassAbs (x, n, k), loc) => - [(L'.SgiClass (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) + (L'.SgnConst (#1 (ListUtil.foldlMapConcat + (fn (sgi, env) => + (case sgi of (L'.SgiConAbs (x, n, k), loc) => + [(L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)] + | (L'.SgiDatatype dts, loc) => + map (fn (x, n, xs, xncs) => (L'.SgiDatatypeImp (x, n, str, strs, x, xs, xncs), loc)) dts + | (L'.SgiClassAbs (x, n, k), loc) => + [(L'.SgiClass (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], + E.sgiBinds env sgi)) env sgis)), #2 sgn) | L'.SgnFun _ => sgn | L'.SgnWhere _ => sgn | L'.SgnProj (m, ms, x) => -- cgit v1.2.3