Mercurial > urweb

comparison src/elaborate.sml @ 1527:cccf8bf64b30

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix opening of shadowing, principal-signatured modules that open other modules
author Adam Chlipala <adam@chlipala.net>
date Thu, 04 Aug 2011 16:44:05 -0400
parents 18d18a70821e
children a8a538800278
comparison
equal deleted inserted replaced
1526:b5d78407886d 1527:cccf8bf64b30
2721 | SOME (str, strs) => selfify env {sgn = sgn, str = str, strs = strs} 2721 | SOME (str, strs) => selfify env {sgn = sgn, str = str, strs = strs}
2722 end 2722 end
2723 2723
2724 and dopen env {str, strs, sgn} = 2724 and dopen env {str, strs, sgn} =
2725 let 2725 let
2726 fun isVisible x = x <> "" andalso String.sub (x, 0) <> #"?"
2727
2726 val m = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn)) 2728 val m = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn))
2727 (L'.StrVar str, #2 sgn) strs 2729 (L'.StrVar str, #2 sgn) strs
2728 in 2730 in
2729 case #1 (hnormSgn env sgn) of 2731 case #1 (hnormSgn env sgn) of
2730 L'.SgnConst sgis => 2732 L'.SgnConst sgis =>
2732 (fn ((sgi, loc), env') => 2734 (fn ((sgi, loc), env') =>
2733 let 2735 let
2734 val d = 2736 val d =
2735 case sgi of 2737 case sgi of
2736 L'.SgiConAbs (x, n, k) => 2738 L'.SgiConAbs (x, n, k) =>
2737 let 2739 if isVisible x then
2738 val c = (L'.CModProj (str, strs, x), loc) 2740 let
2739 in 2741 val c = (L'.CModProj (str, strs, x), loc)
2740 [(L'.DCon (x, n, k, c), loc)] 2742 in
2741 end 2743 [(L'.DCon (x, n, k, c), loc)]
2744 end
2745 else
2746 []
2742 | L'.SgiCon (x, n, k, c) => 2747 | L'.SgiCon (x, n, k, c) =>
2743 [(L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)] 2748 if isVisible x then
2749 [(L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)]
2750 else
2751 []
2744 | L'.SgiDatatype dts => 2752 | L'.SgiDatatype dts =>
2745 map (fn (x, n, xs, xncs) => (L'.DDatatypeImp (x, n, str, strs, x, xs, xncs), loc)) dts 2753 List.mapPartial (fn (x, n, xs, xncs) => if isVisible x then
2754 SOME (L'.DDatatypeImp (x, n, str, strs, x, xs, xncs), loc)
2755 else
2756 NONE) dts
2746 | L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) => 2757 | L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
2747 [(L'.DDatatypeImp (x, n, m1, ms, x', xs, xncs), loc)] 2758 if isVisible x then
2759 [(L'.DDatatypeImp (x, n, m1, ms, x', xs, xncs), loc)]
2760 else
2761 []
2748 | L'.SgiVal (x, n, t) => 2762 | L'.SgiVal (x, n, t) =>
2749 [(L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc)] 2763 if isVisible x then
2764 [(L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc)]
2765 else
2766 []
2750 | L'.SgiStr (x, n, sgn) => 2767 | L'.SgiStr (x, n, sgn) =>
2751 [(L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc)] 2768 if isVisible x then
2769 [(L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc)]
2770 else
2771 []
2752 | L'.SgiSgn (x, n, sgn) => 2772 | L'.SgiSgn (x, n, sgn) =>
2753 [(L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc)] 2773 if isVisible x then
2774 [(L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc)]
2775 else
2776 []
2754 | L'.SgiConstraint (c1, c2) => 2777 | L'.SgiConstraint (c1, c2) =>
2755 [(L'.DConstraint (c1, c2), loc)] 2778 [(L'.DConstraint (c1, c2), loc)]
2756 | L'.SgiClassAbs (x, n, k) => 2779 | L'.SgiClassAbs (x, n, k) =>
2757 let 2780 if isVisible x then
2758 val c = (L'.CModProj (str, strs, x), loc) 2781 let
2759 in 2782 val c = (L'.CModProj (str, strs, x), loc)
2760 [(L'.DCon (x, n, k, c), loc)] 2783 in
2761 end 2784 [(L'.DCon (x, n, k, c), loc)]
2785 end
2786 else
2787 []
2762 | L'.SgiClass (x, n, k, _) => 2788 | L'.SgiClass (x, n, k, _) =>
2763 let 2789 if isVisible x then
2764 val c = (L'.CModProj (str, strs, x), loc) 2790 let
2765 in 2791 val c = (L'.CModProj (str, strs, x), loc)
2766 [(L'.DCon (x, n, k, c), loc)] 2792 in
2767 end 2793 [(L'.DCon (x, n, k, c), loc)]
2794 end
2795 else
2796 []
2768 in 2797 in
2769 (d, foldl (fn (d, env') => E.declBinds env' d) env' d) 2798 (d, foldl (fn (d, env') => E.declBinds env' d) env' d)
2770 end) 2799 end)
2771 env sgis 2800 env sgis
2772 | _ => (strError env (UnOpenable sgn); 2801 | _ => (strError env (UnOpenable sgn);