Mercurial > urweb

comparison src/elaborate.sml @ 1640:dc986eb6113c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Order constructors properly in wildification, to avoid spuriously displeasing the new scoping check
author Adam Chlipala <adam@chlipala.net>
date Sun, 18 Dec 2011 12:00:36 -0500
parents 6c00d8af6239
children 2b7d3d99dc42
comparison
equal deleted inserted replaced
1639:6c00d8af6239 1640:dc986eb6113c
1898 | _ => NONE 1898 | _ => NONE
1899 in 1899 in
1900 findHead e 1900 findHead e
1901 end 1901 end
1902 1902
1903 datatype needed = Needed of {Cons : L'.kind SM.map, 1903 datatype needed = Needed of {Cons : (L'.kind * int) SM.map,
1904 NextCon : int,
1904 Constraints : (E.env * (L'.con * L'.con) * ErrorMsg.span) list, 1905 Constraints : (E.env * (L'.con * L'.con) * ErrorMsg.span) list,
1905 Vals : SS.set, 1906 Vals : SS.set,
1906 Mods : (E.env * needed) SM.map} 1907 Mods : (E.env * needed) SM.map}
1907 1908
1908 fun ncons (Needed r) = #Cons r 1909 fun ncons (Needed r) = map (fn (k, (v, _)) => (k, v))
1910 (ListMergeSort.sort (fn ((_, (_, n1)), (_, (_, n2))) => n1 > n2)
1911 (SM.listItemsi (#Cons r)))
1909 fun nconstraints (Needed r) = #Constraints r 1912 fun nconstraints (Needed r) = #Constraints r
1910 fun nvals (Needed r) = #Vals r 1913 fun nvals (Needed r) = #Vals r
1911 fun nmods (Needed r) = #Mods r 1914 fun nmods (Needed r) = #Mods r
1912 1915
1913 val nempty = Needed {Cons = SM.empty, 1916 val nempty = Needed {Cons = SM.empty,
1917 NextCon = 0,
1914 Constraints = nil, 1918 Constraints = nil,
1915 Vals = SS.empty, 1919 Vals = SS.empty,
1916 Mods = SM.empty} 1920 Mods = SM.empty}
1917 1921
1918 fun naddCon (r : needed, k, v) = 1922 fun naddCon (r : needed, k, v) =
1919 let 1923 let
1920 val Needed r = r 1924 val Needed r = r
1921 in 1925 in
1922 Needed {Cons = SM.insert (#Cons r, k, v), 1926 Needed {Cons = SM.insert (#Cons r, k, (v, #NextCon r)),
1927 NextCon = #NextCon r + 1,
1923 Constraints = #Constraints r, 1928 Constraints = #Constraints r,
1924 Vals = #Vals r, 1929 Vals = #Vals r,
1925 Mods = #Mods r} 1930 Mods = #Mods r}
1926 end 1931 end
1927 1932
1928 fun naddConstraint (r : needed, v) = 1933 fun naddConstraint (r : needed, v) =
1929 let 1934 let
1930 val Needed r = r 1935 val Needed r = r
1931 in 1936 in
1932 Needed {Cons = #Cons r, 1937 Needed {Cons = #Cons r,
1938 NextCon = #NextCon r,
1933 Constraints = v :: #Constraints r, 1939 Constraints = v :: #Constraints r,
1934 Vals = #Vals r, 1940 Vals = #Vals r,
1935 Mods = #Mods r} 1941 Mods = #Mods r}
1936 end 1942 end
1937 1943
1938 fun naddVal (r : needed, k) = 1944 fun naddVal (r : needed, k) =
1939 let 1945 let
1940 val Needed r = r 1946 val Needed r = r
1941 in 1947 in
1942 Needed {Cons = #Cons r, 1948 Needed {Cons = #Cons r,
1949 NextCon = #NextCon r,
1943 Constraints = #Constraints r, 1950 Constraints = #Constraints r,
1944 Vals = SS.add (#Vals r, k), 1951 Vals = SS.add (#Vals r, k),
1945 Mods = #Mods r} 1952 Mods = #Mods r}
1946 end 1953 end
1947 1954
1948 fun naddMod (r : needed, k, v) = 1955 fun naddMod (r : needed, k, v) =
1949 let 1956 let
1950 val Needed r = r 1957 val Needed r = r
1951 in 1958 in
1952 Needed {Cons = #Cons r, 1959 Needed {Cons = #Cons r,
1960 NextCon = #NextCon r,
1953 Constraints = #Constraints r, 1961 Constraints = #Constraints r,
1954 Vals = #Vals r, 1962 Vals = #Vals r,
1955 Mods = SM.insert (#Mods r, k, v)} 1963 Mods = SM.insert (#Mods r, k, v)}
1956 end 1964 end
1957 1965
1958 fun ndelCon (r : needed, k) = 1966 fun ndelCon (r : needed, k) =
1959 let 1967 let
1960 val Needed r = r 1968 val Needed r = r
1961 in 1969 in
1962 Needed {Cons = #1 (SM.remove (#Cons r, k)) handle NotFound => #Cons r, 1970 Needed {Cons = #1 (SM.remove (#Cons r, k)) handle NotFound => #Cons r,
1971 NextCon = #NextCon r,
1963 Constraints = #Constraints r, 1972 Constraints = #Constraints r,
1964 Vals = #Vals r, 1973 Vals = #Vals r,
1965 Mods = #Mods r} 1974 Mods = #Mods r}
1966 end 1975 end
1967 1976
1968 fun ndelVal (r : needed, k) = 1977 fun ndelVal (r : needed, k) =
1969 let 1978 let
1970 val Needed r = r 1979 val Needed r = r
1971 in 1980 in
1972 Needed {Cons = #Cons r, 1981 Needed {Cons = #Cons r,
1982 NextCon = #NextCon r,
1973 Constraints = #Constraints r, 1983 Constraints = #Constraints r,
1974 Vals = SS.delete (#Vals r, k) handle NotFound => #Vals r, 1984 Vals = SS.delete (#Vals r, k) handle NotFound => #Vals r,
1975 Mods = #Mods r} 1985 Mods = #Mods r}
1976 end 1986 end
1977 1987
3647 in 3657 in
3648 ds'' @ ds' 3658 ds'' @ ds'
3649 end 3659 end
3650 3660
3651 val ds' = 3661 val ds' =
3652 case SM.listItemsi (ncons nd) of 3662 case ncons nd of
3653 [] => ds' 3663 [] => ds'
3654 | xs => 3664 | xs =>
3655 map (fn (x, k) => 3665 map (fn (x, k) =>
3656 let 3666 let
3657 val k = 3667 val k =