Mercurial > urweb

comparison src/elab_env.sml @ 2190:22117edf8fd3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
After a tricky debugging session, limit visibility of type-class instances from anonymous modules
author Adam Chlipala <adam@chlipala.net>
date Sun, 01 Nov 2015 16:33:14 -0500
parents 834b438d57f3
children 100352dbae36
comparison
equal deleted inserted replaced
2189:43393a4a66ce 2190:22117edf8fd3
988 | SgiCon (x, n, _, _) => (sgns, strs, IM.insert (cons, n, x)) 988 | SgiCon (x, n, _, _) => (sgns, strs, IM.insert (cons, n, x))
989 | SgiDatatype dts => (sgns, strs, foldl (fn ((x, n, _, _), cons) => IM.insert (cons, n, x)) cons dts) 989 | SgiDatatype dts => (sgns, strs, foldl (fn ((x, n, _, _), cons) => IM.insert (cons, n, x)) cons dts)
990 | SgiDatatypeImp (x, n, _, _, _, _, _) => (sgns, strs, IM.insert (cons, n, x)) 990 | SgiDatatypeImp (x, n, _, _, _, _, _) => (sgns, strs, IM.insert (cons, n, x))
991 | SgiVal _ => (sgns, strs, cons) 991 | SgiVal _ => (sgns, strs, cons)
992 | SgiSgn (x, n, _) => (IM.insert (sgns, n, x), strs, cons) 992 | SgiSgn (x, n, _) => (IM.insert (sgns, n, x), strs, cons)
993 | SgiStr (x, n, _) => (sgns, IM.insert (strs, n, x), cons) 993 | SgiStr (_, x, n, _) => (sgns, IM.insert (strs, n, x), cons)
994 | SgiConstraint _ => (sgns, strs, cons) 994 | SgiConstraint _ => (sgns, strs, cons)
995 | SgiClassAbs (x, n, _) => (sgns, strs, IM.insert (cons, n, x)) 995 | SgiClassAbs (x, n, _) => (sgns, strs, IM.insert (cons, n, x))
996 | SgiClass (x, n, _, _) => (sgns, strs, IM.insert (cons, n, x)) 996 | SgiClass (x, n, _, _) => (sgns, strs, IM.insert (cons, n, x))
997 997
998 fun sgnSeek f sgis = 998 fun sgnSeek f sgis =
1141 if List.null ms andalso x = x' then 1141 if List.null ms andalso x = x' then
1142 List.revAppend (pre, (SgiCon (x', n, k, c), loc) :: rest) 1142 List.revAppend (pre, (SgiCon (x', n, k, c), loc) :: rest)
1143 else 1143 else
1144 traverse (ms, sgi :: pre, rest) 1144 traverse (ms, sgi :: pre, rest)
1145 1145
1146 | (sgi as (SgiStr (x', n, sgn'), loc)) :: rest => 1146 | (sgi as (SgiStr (im, x', n, sgn'), loc)) :: rest =>
1147 (case ms of 1147 (case ms of
1148 [] => traverse (ms, sgi :: pre, rest) 1148 [] => traverse (ms, sgi :: pre, rest)
1149 | x :: ms' => 1149 | x :: ms' =>
1150 if x = x' then 1150 if x = x' then
1151 List.revAppend (pre, 1151 List.revAppend (pre,
1152 (SgiStr (x', n, 1152 (SgiStr (im, x', n,
1153 rewrite (sgn', ms')), loc) :: rest) 1153 rewrite (sgn', ms')), loc) :: rest)
1154 else 1154 else
1155 traverse (ms, sgi :: pre, rest)) 1155 traverse (ms, sgi :: pre, rest))
1156 1156
1157 | sgi :: rest => traverse (ms, sgi :: pre, rest) 1157 | sgi :: rest => traverse (ms, sgi :: pre, rest)
1184 env) 1184 env)
1185 1185
1186 fun default () = (classes, newClasses, sgiSeek (#1 sgi, fmap), env) 1186 fun default () = (classes, newClasses, sgiSeek (#1 sgi, fmap), env)
1187 in 1187 in
1188 case #1 sgi of 1188 case #1 sgi of
1189 SgiStr (x, _, sgn) => 1189 SgiStr (Import, x, _, sgn) =>
1190 let 1190 let
1191 val str = manifest (m1, ms, #2 sgi) 1191 val str = manifest (m1, ms, #2 sgi)
1192 val sgn' = sgnSubSgn (str, fmap) sgn 1192 val sgn' = sgnSubSgn (str, fmap) sgn
1193 in 1193 in
1194 (enrichClasses env classes (m1, ms @ [x]) sgn', 1194 (enrichClasses env classes (m1, ms @ [x]) sgn',
1358 pushENamedAs env x' n' t 1358 pushENamedAs env x' n' t
1359 end) 1359 end)
1360 env xncs 1360 env xncs
1361 end 1361 end
1362 | SgiVal (x, n, t) => pushENamedAs env x n t 1362 | SgiVal (x, n, t) => pushENamedAs env x n t
1363 | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn 1363 | SgiStr (_, x, n, sgn) => pushStrNamedAs env x n sgn
1364 | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn 1364 | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
1365 | SgiConstraint _ => env 1365 | SgiConstraint _ => env
1366 1366
1367 | SgiClassAbs (x, n, k) => pushCNamedAs env x n k NONE 1367 | SgiClassAbs (x, n, k) => pushCNamedAs env x n k NONE
1368 | SgiClass (x, n, k, c) => pushCNamedAs env x n k (SOME c) 1368 | SgiClass (x, n, k, c) => pushCNamedAs env x n k (SOME c)
1372 con = sgnS_con x} 1372 con = sgnS_con x}
1373 1373
1374 fun projectStr env {sgn, str, field} = 1374 fun projectStr env {sgn, str, field} =
1375 case #1 (hnormSgn env sgn) of 1375 case #1 (hnormSgn env sgn) of
1376 SgnConst sgis => 1376 SgnConst sgis =>
1377 (case sgnSeek (fn SgiStr (x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of 1377 (case sgnSeek (fn SgiStr (_, x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of
1378 NONE => NONE 1378 NONE => NONE
1379 | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn)) 1379 | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn))
1380 | SgnError => SOME (SgnError, ErrorMsg.dummySpan) 1380 | SgnError => SOME (SgnError, ErrorMsg.dummySpan)
1381 | _ => NONE 1381 | _ => NONE
1382 1382
1542 | SgiDatatype dts => seek (sgis, sgns, strs, 1542 | SgiDatatype dts => seek (sgis, sgns, strs,
1543 foldl (fn ((x, n, _, _), cons) => IM.insert (cons, n, x)) cons dts, acc) 1543 foldl (fn ((x, n, _, _), cons) => IM.insert (cons, n, x)) cons dts, acc)
1544 | SgiDatatypeImp (x, n, _, _, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) 1544 | SgiDatatypeImp (x, n, _, _, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
1545 | SgiVal _ => seek (sgis, sgns, strs, cons, acc) 1545 | SgiVal _ => seek (sgis, sgns, strs, cons, acc)
1546 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc) 1546 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc)
1547 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc) 1547 | SgiStr (_, x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc)
1548 | SgiClassAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) 1548 | SgiClassAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
1549 | SgiClass (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) 1549 | SgiClass (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
1550 in 1550 in
1551 seek (sgis, IM.empty, IM.empty, IM.empty, []) 1551 seek (sgis, IM.empty, IM.empty, IM.empty, [])
1552 end 1552 end