Mercurial > urweb

comparison src/elab_env.sml @ 1864:1aa9629e3a4c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Allow [where con] to descend within submodule structure; open submodule constraints while checking later signature items
author Adam Chlipala <adam@chlipala.net>
date Mon, 19 Aug 2013 12:25:32 -0400
parents bb942416bf1c
children 403f0cc65b9c
comparison
equal deleted inserted replaced
1863:32784d27b5bc 1864:1aa9629e3a4c
1124 sgn = sgn, 1124 sgn = sgn,
1125 field = x} of 1125 field = x} of
1126 NONE => raise Fail "ElabEnv.hnormSgn: projectSgn failed" 1126 NONE => raise Fail "ElabEnv.hnormSgn: projectSgn failed"
1127 | SOME sgn => hnormSgn env sgn 1127 | SOME sgn => hnormSgn env sgn
1128 end 1128 end
1129 | SgnWhere (sgn, x, c) => 1129 | SgnWhere (sgn, ms, x, c) =>
1130 case #1 (hnormSgn env sgn) of 1130 let
1131 SgnError => (SgnError, loc) 1131 fun rewrite (sgn, ms) =
1132 | SgnConst sgis => 1132 case #1 (hnormSgn env sgn) of
1133 let 1133 SgnError => (SgnError, loc)
1134 fun traverse (pre, post) = 1134 | SgnConst sgis =>
1135 case post of 1135 let
1136 [] => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [1]" 1136 fun traverse (ms, pre, post) =
1137 | (sgi as (SgiConAbs (x', n, k), loc)) :: rest => 1137 case post of
1138 if x = x' then 1138 [] => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [1]"
1139 List.revAppend (pre, (SgiCon (x', n, k, c), loc) :: rest) 1139
1140 else 1140 | (sgi as (SgiConAbs (x', n, k), loc)) :: rest =>
1141 traverse (sgi :: pre, rest) 1141 if List.null ms andalso x = x' then
1142 | sgi :: rest => traverse (sgi :: pre, rest) 1142 List.revAppend (pre, (SgiCon (x', n, k, c), loc) :: rest)
1143 1143 else
1144 val sgis = traverse ([], sgis) 1144 traverse (ms, sgi :: pre, rest)
1145 in 1145
1146 (SgnConst sgis, loc) 1146 | (sgi as (SgiStr (x', n, sgn'), loc)) :: rest =>
1147 end 1147 (case ms of
1148 | _ => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [2]" 1148 [] => traverse (ms, sgi :: pre, rest)
1149 | x :: ms' =>
1150 if x = x' then
1151 List.revAppend (pre,
1152 (SgiStr (x', n,
1153 rewrite (sgn', ms')), loc) :: rest)
1154 else
1155 traverse (ms, sgi :: pre, rest))
1156
1157 | sgi :: rest => traverse (ms, sgi :: pre, rest)
1158
1159 val sgis = traverse (ms, [], sgis)
1160 in
1161 (SgnConst sgis, loc)
1162 end
1163 | _ => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [2]"
1164 in
1165 rewrite (sgn, ms)
1166 end
1149 1167
1150 fun manifest (m, ms, loc) = 1168 fun manifest (m, ms, loc) =
1151 foldl (fn (m, str) => (StrProj (str, m), loc)) (StrVar m, loc) ms 1169 foldl (fn (m, str) => (StrProj (str, m), loc)) (StrVar m, loc) ms
1152 1170
1153 fun enrichClasses env classes (m1, ms) sgn = 1171 fun enrichClasses env classes (m1, ms) sgn =