Mercurial > urweb
comparison src/elaborate.sml @ 2190:22117edf8fd3
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 | 1ecef02f67c5 |
children | fb113569519e |
comparison
equal
deleted
inserted
replaced
2189:43393a4a66ce | 2190:22117edf8fd3 |
---|---|
2479 | SOME cs => | 2479 | SOME cs => |
2480 case #1 (hnormSgn env sgn) of | 2480 case #1 (hnormSgn env sgn) of |
2481 L'.SgnConst sgis => | 2481 L'.SgnConst sgis => |
2482 foldl (fn (sgi, cs) => | 2482 foldl (fn (sgi, cs) => |
2483 case #1 sgi of | 2483 case #1 sgi of |
2484 L'.SgiStr (x, _, _) => | 2484 L'.SgiStr (L'.Import, x, _, _) => |
2485 (case E.projectStr env {sgn = sgn, str = st, field = x} of | 2485 (case E.projectStr env {sgn = sgn, str = st, field = x} of |
2486 NONE => raise Fail "Elaborate: projectStr in collect" | 2486 NONE => raise Fail "Elaborate: projectStr in collect" |
2487 | SOME sgn' => | 2487 | SOME sgn' => |
2488 List.revAppend (collect false ((L'.StrProj (st, x), loc), sgn'), | 2488 List.revAppend (collect false ((L'.StrProj (st, x), loc), sgn'), |
2489 cs)) | 2489 cs)) |
2491 | _ => cs | 2491 | _ => cs |
2492 in | 2492 in |
2493 foldl (fn ((c1, c2), denv) => | 2493 foldl (fn ((c1, c2), denv) => |
2494 D.assert env denv (c1, c2)) denv (collect true (st, sgn)) | 2494 D.assert env denv (c1, c2)) denv (collect true (st, sgn)) |
2495 end | 2495 end |
2496 | |
2497 fun tcdump env = | |
2498 Print.preface("Instances", p_list_sep Print.PD.newline | |
2499 (fn (cl, ls) => | |
2500 box [p_con env cl, | |
2501 box [Print.PD.string "{", | |
2502 p_list (fn (t, e) => | |
2503 box [p_exp env e, | |
2504 Print.PD.string " : ", | |
2505 p_con env t]) ls, | |
2506 Print.PD.string "}"]]) | |
2507 (E.listClasses env)) | |
2496 | 2508 |
2497 fun elabSgn_item ((sgi, loc), (env, denv, gs)) = | 2509 fun elabSgn_item ((sgi, loc), (env, denv, gs)) = |
2498 ((*Print.preface ("elabSgi", SourcePrint.p_sgn_item (sgi, loc));*) | 2510 ((*Print.preface ("elabSgi", SourcePrint.p_sgn_item (sgi, loc));*) |
2499 case sgi of | 2511 case sgi of |
2500 L.SgiConAbs (x, k) => | 2512 L.SgiConAbs (x, k) => |
2693 let | 2705 let |
2694 val (sgn', gs') = elabSgn (env, denv) sgn | 2706 val (sgn', gs') = elabSgn (env, denv) sgn |
2695 val (env', n) = E.pushStrNamed env x sgn' | 2707 val (env', n) = E.pushStrNamed env x sgn' |
2696 val denv' = dopenConstraints (loc, env', denv) {str = x, strs = []} | 2708 val denv' = dopenConstraints (loc, env', denv) {str = x, strs = []} |
2697 in | 2709 in |
2698 ([(L'.SgiStr (x, n, sgn'), loc)], (env', denv', gs' @ gs)) | 2710 ([(L'.SgiStr (L'.Import, x, n, sgn'), loc)], (env', denv', gs' @ gs)) |
2699 end | 2711 end |
2700 | 2712 |
2701 | L.SgiSgn (x, sgn) => | 2713 | L.SgiSgn (x, sgn) => |
2702 let | 2714 let |
2703 val (sgn', gs') = elabSgn (env, denv) sgn | 2715 val (sgn', gs') = elabSgn (env, denv) sgn |
2812 (if SS.member (sgns, x) then | 2824 (if SS.member (sgns, x) then |
2813 sgnError env (DuplicateSgn (loc, x)) | 2825 sgnError env (DuplicateSgn (loc, x)) |
2814 else | 2826 else |
2815 (); | 2827 (); |
2816 (cons, vals, SS.add (sgns, x), strs)) | 2828 (cons, vals, SS.add (sgns, x), strs)) |
2817 | L'.SgiStr (x, _, _) => | 2829 | L'.SgiStr (_, x, _, _) => |
2818 (if SS.member (strs, x) then | 2830 (if SS.member (strs, x) then |
2819 sgnError env (DuplicateStr (loc, x)) | 2831 sgnError env (DuplicateStr (loc, x)) |
2820 else | 2832 else |
2821 (); | 2833 (); |
2822 (cons, vals, sgns, SS.add (strs, x))) | 2834 (cons, vals, sgns, SS.add (strs, x))) |
2863 List.exists (fn (L'.SgiConAbs (x', _, k), _) => | 2875 List.exists (fn (L'.SgiConAbs (x', _, k), _) => |
2864 List.null ms andalso x' = x andalso | 2876 List.null ms andalso x' = x andalso |
2865 (unifyKinds env k ck | 2877 (unifyKinds env k ck |
2866 handle KUnify x => sgnError env (WhereWrongKind x); | 2878 handle KUnify x => sgnError env (WhereWrongKind x); |
2867 true) | 2879 true) |
2868 | (L'.SgiStr (x', _, sgn''), _) => | 2880 | (L'.SgiStr (_, x', _, sgn''), _) => |
2869 (case ms of | 2881 (case ms of |
2870 [] => false | 2882 [] => false |
2871 | m :: ms' => | 2883 | m :: ms' => |
2872 m = x' andalso | 2884 m = x' andalso |
2873 checkPath (ms', sgn'')) | 2885 checkPath (ms', sgn'')) |
2912 [(L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)] | 2924 [(L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)] |
2913 | (L'.SgiDatatype dts, loc) => | 2925 | (L'.SgiDatatype dts, loc) => |
2914 map (fn (x, n, xs, xncs) => (L'.SgiDatatypeImp (x, n, str, strs, x, xs, xncs), loc)) dts | 2926 map (fn (x, n, xs, xncs) => (L'.SgiDatatypeImp (x, n, str, strs, x, xs, xncs), loc)) dts |
2915 | (L'.SgiClassAbs (x, n, k), loc) => | 2927 | (L'.SgiClassAbs (x, n, k), loc) => |
2916 [(L'.SgiClass (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)] | 2928 [(L'.SgiClass (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)] |
2917 | (L'.SgiStr (x, n, sgn), loc) => | 2929 | (L'.SgiStr (im, x, n, sgn), loc) => |
2918 [(L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc)] | 2930 [(L'.SgiStr (im, x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc)] |
2919 | x => [x], | 2931 | x => [x], |
2920 E.sgiBinds env sgi)) env sgis)), #2 sgn) | 2932 E.sgiBinds env sgi)) env sgis)), #2 sgn) |
2921 | L'.SgnFun _ => sgn | 2933 | L'.SgnFun _ => sgn |
2922 | L'.SgnWhere _ => sgn | 2934 | L'.SgnWhere _ => sgn |
2923 | L'.SgnProj (m, ms, x) => | 2935 | L'.SgnProj (m, ms, x) => |
2985 | L'.SgiVal (x, n, t) => | 2997 | L'.SgiVal (x, n, t) => |
2986 if isVisible x then | 2998 if isVisible x then |
2987 [(L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc)] | 2999 [(L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc)] |
2988 else | 3000 else |
2989 [] | 3001 [] |
2990 | L'.SgiStr (x, n, sgn) => | 3002 | L'.SgiStr (_, x, n, sgn) => |
2991 if isVisible x then | 3003 if isVisible x then |
2992 [(L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc)] | 3004 [(L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc)] |
2993 else | 3005 else |
2994 [] | 3006 [] |
2995 | L'.SgiSgn (x, n, sgn) => | 3007 | L'.SgiSgn (x, n, sgn) => |
3031 | L'.DDatatype x => [(L'.SgiDatatype x, loc)] | 3043 | L'.DDatatype x => [(L'.SgiDatatype x, loc)] |
3032 | L'.DDatatypeImp x => [(L'.SgiDatatypeImp x, loc)] | 3044 | L'.DDatatypeImp x => [(L'.SgiDatatypeImp x, loc)] |
3033 | L'.DVal (x, n, t, _) => [(L'.SgiVal (x, n, t), loc)] | 3045 | L'.DVal (x, n, t, _) => [(L'.SgiVal (x, n, t), loc)] |
3034 | L'.DValRec vis => map (fn (x, n, t, _) => (L'.SgiVal (x, n, t), loc)) vis | 3046 | L'.DValRec vis => map (fn (x, n, t, _) => (L'.SgiVal (x, n, t), loc)) vis |
3035 | L'.DSgn (x, n, sgn) => [(L'.SgiSgn (x, n, sgn), loc)] | 3047 | L'.DSgn (x, n, sgn) => [(L'.SgiSgn (x, n, sgn), loc)] |
3036 | L'.DStr (x, n, sgn, _) => [(L'.SgiStr (x, n, sgn), loc)] | 3048 | L'.DStr (x, n, sgn, _) => [(L'.SgiStr (L'.Import, x, n, sgn), loc)] |
3037 | L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (x, n, sgn), loc)] | 3049 | L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (L'.Import, x, n, sgn), loc)] |
3038 | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)] | 3050 | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)] |
3039 | L'.DExport _ => [] | 3051 | L'.DExport _ => [] |
3040 | L'.DTable (tn, x, n, c, _, pc, _, cc) => | 3052 | L'.DTable (tn, x, n, c, _, pc, _, cc) => |
3041 [(L'.SgiVal (x, n, (L'.CApp ((L'.CApp (tableOf (), c), loc), | 3053 [(L'.SgiVal (x, n, (L'.CApp ((L'.CApp (tableOf (), c), loc), |
3042 (L'.CConcat (pc, cc), loc)), loc)), loc)] | 3054 (L'.CConcat (pc, cc), loc)), loc)), loc)] |
3342 SOME env) | 3354 SOME env) |
3343 else | 3355 else |
3344 NONE | 3356 NONE |
3345 | _ => NONE) | 3357 | _ => NONE) |
3346 | 3358 |
3347 | L'.SgiStr (x, n2, sgn2) => | 3359 | L'.SgiStr (_, x, n2, sgn2) => |
3348 seek (fn (env, sgi1All as (sgi1, loc)) => | 3360 seek (fn (env, sgi1All as (sgi1, loc)) => |
3349 case sgi1 of | 3361 case sgi1 of |
3350 L'.SgiStr (x', n1, sgn1) => | 3362 L'.SgiStr (_, x', n1, sgn1) => |
3351 if x = x' then | 3363 if x = x' then |
3352 let | 3364 let |
3353 (* Don't forget to save & restore the | 3365 (* Don't forget to save & restore the |
3354 * counterparts map around recursive calls! | 3366 * counterparts map around recursive calls! |
3355 * Otherwise, all sorts of mayhem may result. *) | 3367 * Otherwise, all sorts of mayhem may result. *) |
3747 if should t then | 3759 if should t then |
3748 naddVal (nd, x) | 3760 naddVal (nd, x) |
3749 else | 3761 else |
3750 nd | 3762 nd |
3751 end | 3763 end |
3752 | L'.SgiStr (x, _, s) => | 3764 | L'.SgiStr (_, x, _, s) => |
3753 (case #1 (hnormSgn env' s) of | 3765 (case #1 (hnormSgn env' s) of |
3754 L'.SgnConst sgis' => naddMod (nd, x, (env', buildNeeded env' sgis')) | 3766 L'.SgnConst sgis' => naddMod (nd, x, (env', buildNeeded env' sgis')) |
3755 | _ => nd) | 3767 | _ => nd) |
3756 | _ => nd, | 3768 | _ => nd, |
3757 E.sgiBinds env' (sgi, loc))) | 3769 E.sgiBinds env' (sgi, loc))) |
4494 (SS.add (sgns, x), x) | 4506 (SS.add (sgns, x), x) |
4495 in | 4507 in |
4496 ((L'.SgiSgn (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs) | 4508 ((L'.SgiSgn (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs) |
4497 end | 4509 end |
4498 | 4510 |
4499 | L'.SgiStr (x, n, sgn) => | 4511 | L'.SgiStr (im, x, n, sgn) => |
4500 let | 4512 let |
4501 val (strs, x) = | 4513 val (strs, x) = |
4502 if SS.member (strs, x) then | 4514 if SS.member (strs, x) then |
4503 (strs, "?" ^ x) | 4515 (strs, "?" ^ x) |
4504 else | 4516 else |
4505 (SS.add (strs, x), x) | 4517 (SS.add (strs, x), x) |
4506 in | 4518 in |
4507 ((L'.SgiStr (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs) | 4519 ((L'.SgiStr (im, x, n, sgn), loc) :: sgis, cons, vals, sgns, strs) |
4508 end | 4520 end |
4509 | L'.SgiConstraint _ => ((sgi, loc) :: sgis, cons, vals, sgns, strs) | 4521 | L'.SgiConstraint _ => ((sgi, loc) :: sgis, cons, vals, sgns, strs) |
4510 | L'.SgiClassAbs (x, n, k) => | 4522 | L'.SgiClassAbs (x, n, k) => |
4511 let | 4523 let |
4512 val (cons, x) = | 4524 val (cons, x) = |
4608 * arbitarily many question marks before the module name to | 4620 * arbitarily many question marks before the module name to |
4609 * avoid a clash, since some other code might depend on | 4621 * avoid a clash, since some other code might depend on |
4610 * question-mark identifiers generated previously by this | 4622 * question-mark identifiers generated previously by this |
4611 * very code fragment. *) | 4623 * very code fragment. *) |
4612 fun mungeName m = | 4624 fun mungeName m = |
4613 if List.exists (fn (L'.SgiStr (x, _, _), _) => x = m | 4625 if List.exists (fn (L'.SgiStr (_, x, _, _), _) => x = m |
4614 | _ => false) sgis then | 4626 | _ => false) sgis then |
4615 mungeName ("?" ^ m) | 4627 mungeName ("?" ^ m) |
4616 else | 4628 else |
4617 m | 4629 m |
4618 | 4630 |
4619 val m = mungeName m | 4631 val m = mungeName m |
4620 in | 4632 in |
4621 ((L'.StrApp (str1', str2'), loc), | 4633 ((L'.StrApp (str1', str2'), loc), |
4622 (L'.SgnConst ((L'.SgiStr (m, n, selfifyAt env {str = str2', sgn = sgn2}), loc) :: sgis), loc), | 4634 (L'.SgnConst ((L'.SgiStr (L'.Skip, m, n, selfifyAt env {str = str2', sgn = sgn2}), loc) :: sgis), loc), |
4623 gs1 @ gs2) | 4635 gs1 @ gs2) |
4624 end | 4636 end |
4625 | _ => raise Fail "Unable to hnormSgn in functor application") | 4637 | _ => raise Fail "Unable to hnormSgn in functor application") |
4626 | _ => (strError env (NotFunctor sgn1); | 4638 | _ => (strError env (NotFunctor sgn1); |
4627 (strerror, sgnerror, [])) | 4639 (strerror, sgnerror, [])) |
4999 ModDb.revert () | 5011 ModDb.revert () |
5000 else | 5012 else |
5001 (); | 5013 (); |
5002 | 5014 |
5003 (*Print.preface("File", ElabPrint.p_file env file);*) | 5015 (*Print.preface("File", ElabPrint.p_file env file);*) |
5004 | 5016 |
5005 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) | 5017 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) |
5006 :: ds | 5018 :: ds |
5007 @ (L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan) | 5019 @ (L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan) |
5008 :: ds' @ file | 5020 :: ds' @ file |
5009 end | 5021 end |