Mercurial > urweb

comparison src/elab_util.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 403f0cc65b9c
children 1091227f535a
comparison
equal deleted inserted replaced
2189:43393a4a66ce 2190:22117edf8fd3
686 (SgiDatatypeImp (x, n, m1, ms, s, xs, xncs'), loc)) 686 (SgiDatatypeImp (x, n, m1, ms, s, xs, xncs'), loc))
687 | SgiVal (x, n, c) => 687 | SgiVal (x, n, c) =>
688 S.map2 (con ctx c, 688 S.map2 (con ctx c,
689 fn c' => 689 fn c' =>
690 (SgiVal (x, n, c'), loc)) 690 (SgiVal (x, n, c'), loc))
691 | SgiStr (x, n, s) => 691 | SgiStr (im, x, n, s) =>
692 S.map2 (sg ctx s, 692 S.map2 (sg ctx s,
693 fn s' => 693 fn s' =>
694 (SgiStr (x, n, s'), loc)) 694 (SgiStr (im, x, n, s'), loc))
695 | SgiSgn (x, n, s) => 695 | SgiSgn (x, n, s) =>
696 S.map2 (sg ctx s, 696 S.map2 (sg ctx s,
697 fn s' => 697 fn s' =>
698 (SgiSgn (x, n, s'), loc)) 698 (SgiSgn (x, n, s'), loc))
699 | SgiConstraint (c1, c2) => 699 | SgiConstraint (c1, c2) =>
736 end) ctx dts 736 end) ctx dts
737 | SgiDatatypeImp (x, n, m1, ms, s, _, _) => 737 | SgiDatatypeImp (x, n, m1, ms, s, _, _) =>
738 bind (ctx, NamedC (x, n, (KType, loc), 738 bind (ctx, NamedC (x, n, (KType, loc),
739 SOME (CModProj (m1, ms, s), loc))) 739 SOME (CModProj (m1, ms, s), loc)))
740 | SgiVal _ => ctx 740 | SgiVal _ => ctx
741 | SgiStr (x, n, sgn) => 741 | SgiStr (_, x, n, sgn) =>
742 bind (ctx, Str (x, n, sgn)) 742 bind (ctx, Str (x, n, sgn))
743 | SgiSgn (x, n, sgn) => 743 | SgiSgn (x, n, sgn) =>
744 bind (ctx, Sgn (x, n, sgn)) 744 bind (ctx, Sgn (x, n, sgn))
745 | SgiConstraint _ => ctx 745 | SgiConstraint _ => ctx
746 | SgiClassAbs (x, n, k) => 746 | SgiClassAbs (x, n, k) =>
1268 (Int.max (n, max)) ns) 0 dts 1268 (Int.max (n, max)) ns) 0 dts
1269 | SgiDatatypeImp (_, n1, n2, _, _, _, ns) => 1269 | SgiDatatypeImp (_, n1, n2, _, _, _, ns) =>
1270 foldl (fn ((_, n', _), m) => Int.max (n', m)) 1270 foldl (fn ((_, n', _), m) => Int.max (n', m))
1271 (Int.max (n1, n2)) ns 1271 (Int.max (n1, n2)) ns
1272 | SgiVal (_, n, _) => n 1272 | SgiVal (_, n, _) => n
1273 | SgiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn) 1273 | SgiStr (_, _, n, sgn) => Int.max (n, maxNameSgn sgn)
1274 | SgiSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn) 1274 | SgiSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn)
1275 | SgiConstraint _ => 0 1275 | SgiConstraint _ => 0
1276 | SgiClassAbs (_, n, _) => n 1276 | SgiClassAbs (_, n, _) => n
1277 | SgiClass (_, n, _, _) => n 1277 | SgiClass (_, n, _, _) => n
1278 1278