Mercurial > urweb

comparison src/elaborate.sml @ 194:df5fd8f6913a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
A multi-parameter datatype all the way through
author Adam Chlipala <adamc@hcoop.net>
date Sat, 09 Aug 2008 08:47:36 -0400
parents aa54250f58ac
children dd82457fda82
comparison
equal deleted inserted replaced
193:8a70e2919e86 194:df5fd8f6913a
952 let 952 let
953 val ((p', pt), (env, bound)) = elabPat (p, (env, denv, bound)) 953 val ((p', pt), (env, bound)) = elabPat (p, (env, denv, bound))
954 954
955 val k = (L'.KType, loc) 955 val k = (L'.KType, loc)
956 val unifs = map (fn _ => cunif (loc, k)) xs 956 val unifs = map (fn _ => cunif (loc, k)) xs
957 val t = ListUtil.foldli (fn (i, u, t) => subConInCon (i, u) t) t unifs 957 val nxs = length unifs - 1
958 val t = ListUtil.foldli (fn (i, u, t) => subConInCon (nxs - i, u) t) t unifs
958 val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs 959 val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs
959 in 960 in
960 ignore (checkPatCon (env, denv) p' pt t); 961 ignore (checkPatCon (env, denv) p' pt t);
961 (((L'.PCon (dk, pc, unifs, SOME p'), loc), dn), 962 (((L'.PCon (dk, pc, unifs, SOME p'), loc), dn),
962 (env, bound)) 963 (env, bound))
1598 let 1599 let
1599 val k = (L'.KType, loc) 1600 val k = (L'.KType, loc)
1600 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs 1601 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
1601 val (env, n) = E.pushCNamed env x k' NONE 1602 val (env, n) = E.pushCNamed env x k' NONE
1602 val t = (L'.CNamed n, loc) 1603 val t = (L'.CNamed n, loc)
1603 val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel i, loc)), loc)) t xs 1604 val nxs = length xs - 1
1605 val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs
1604 1606
1605 val (xcs, (used, env, gs)) = 1607 val (xcs, (used, env, gs)) =
1606 ListUtil.foldlMap 1608 ListUtil.foldlMap
1607 (fn ((x, to), (used, env, gs)) => 1609 (fn ((x, to), (used, env, gs)) =>
1608 let 1610 let
2267 let 2269 let
2268 val k = (L'.KType, loc) 2270 val k = (L'.KType, loc)
2269 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs 2271 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
2270 val (env, n) = E.pushCNamed env x k' NONE 2272 val (env, n) = E.pushCNamed env x k' NONE
2271 val t = (L'.CNamed n, loc) 2273 val t = (L'.CNamed n, loc)
2272 val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel i, loc)), loc)) t xs 2274 val nxs = length xs - 1
2275 val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs
2273 2276
2274 val (env', denv') = foldl (fn (x, (env', denv')) => 2277 val (env', denv') = foldl (fn (x, (env', denv')) =>
2275 (E.pushCRel env' x k, 2278 (E.pushCRel env' x k,
2276 D.enter denv')) (env, denv) xs 2279 D.enter denv')) (env, denv) xs
2277 2280