Mercurial > urweb

comparison src/elab_util.sml @ 1864:1aa9629e3a4c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Allow [where con] to descend within submodule structure; open submodule constraints while checking later signature items
author Adam Chlipala <adam@chlipala.net>
date Mon, 19 Aug 2013 12:25:32 -0400
parents bb942416bf1c
children 403f0cc65b9c
comparison
equal deleted inserted replaced
1863:32784d27b5bc 1864:1aa9629e3a4c
757 fn s1' => 757 fn s1' =>
758 S.map2 (sg (bind (ctx, Str (m, n, s1'))) s2, 758 S.map2 (sg (bind (ctx, Str (m, n, s1'))) s2,
759 fn s2' => 759 fn s2' =>
760 (SgnFun (m, n, s1', s2'), loc))) 760 (SgnFun (m, n, s1', s2'), loc)))
761 | SgnProj _ => S.return2 sAll 761 | SgnProj _ => S.return2 sAll
762 | SgnWhere (sgn, x, c) => 762 | SgnWhere (sgn, ms, x, c) =>
763 S.bind2 (sg ctx sgn, 763 S.bind2 (sg ctx sgn,
764 fn sgn' => 764 fn sgn' =>
765 S.map2 (con ctx c, 765 S.map2 (con ctx c,
766 fn c' => 766 fn c' =>
767 (SgnWhere (sgn', x, c'), loc))) 767 (SgnWhere (sgn', ms, x, c'), loc)))
768 | SgnError => S.return2 sAll 768 | SgnError => S.return2 sAll
769 in 769 in
770 sg 770 sg
771 end 771 end
772 772
1246 and maxNameSgn (sgn, _) = 1246 and maxNameSgn (sgn, _) =
1247 case sgn of 1247 case sgn of
1248 SgnConst sgis => foldl (fn (sgi, count) => Int.max (maxNameSgi sgi, count)) 0 sgis 1248 SgnConst sgis => foldl (fn (sgi, count) => Int.max (maxNameSgi sgi, count)) 0 sgis
1249 | SgnVar n => n 1249 | SgnVar n => n
1250 | SgnFun (_, n, dom, ran) => Int.max (n, Int.max (maxNameSgn dom, maxNameSgn ran)) 1250 | SgnFun (_, n, dom, ran) => Int.max (n, Int.max (maxNameSgn dom, maxNameSgn ran))
1251 | SgnWhere (sgn, _, _) => maxNameSgn sgn 1251 | SgnWhere (sgn, _, _, _) => maxNameSgn sgn
1252 | SgnProj (n, _, _) => n 1252 | SgnProj (n, _, _) => n
1253 | SgnError => 0 1253 | SgnError => 0
1254 1254
1255 and maxNameSgi (sgi, _) = 1255 and maxNameSgi (sgi, _) =
1256 case sgi of 1256 case sgi of