Mercurial > urweb

comparison src/elaborate.sml @ 284:77a28e7430bf

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
intToString
author Adam Chlipala <adamc@hcoop.net>
date Sun, 07 Sep 2008 10:13:02 -0400
parents fdd7a698be01
children f387d12193ba
comparison
equal deleted inserted replaced
283:c0e4ac23522d 284:77a28e7430bf
1921 val (env, n) = E.pushCNamed env x k' NONE 1921 val (env, n) = E.pushCNamed env x k' NONE
1922 val t = (L'.CNamed n, loc) 1922 val t = (L'.CNamed n, loc)
1923 val nxs = length xs - 1 1923 val nxs = length xs - 1
1924 val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs 1924 val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs
1925 1925
1926 val (env', denv') = foldl (fn (x, (env', denv')) =>
1927 (E.pushCRel env' x k,
1928 D.enter denv')) (env, denv) xs
1929
1926 val (xcs, (used, env, gs)) = 1930 val (xcs, (used, env, gs)) =
1927 ListUtil.foldlMap 1931 ListUtil.foldlMap
1928 (fn ((x, to), (used, env, gs)) => 1932 (fn ((x, to), (used, env, gs)) =>
1929 let 1933 let
1930 val (to, t, gs') = case to of 1934 val (to, t, gs') = case to of
1931 NONE => (NONE, t, gs) 1935 NONE => (NONE, t, gs)
1932 | SOME t' => 1936 | SOME t' =>
1933 let 1937 let
1934 val (t', tk, gs') = elabCon (env, denv) t' 1938 val (t', tk, gs') = elabCon (env', denv') t'
1935 in 1939 in
1936 checkKind env t' tk k; 1940 checkKind env' t' tk k;
1937 (SOME t', (L'.TFun (t', t), loc), gs' @ gs) 1941 (SOME t', (L'.TFun (t', t), loc), gs' @ gs)
1938 end 1942 end
1939 val t = foldl (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) t xs 1943 val t = foldl (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) t xs
1940 1944
1941 val (env, n') = E.pushENamed env x t 1945 val (env, n') = E.pushENamed env x t