Mercurial > urweb

comparison src/elab_util.sml @ 2280:985c8016b592

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Merge.
author Ziv Scully <ziv@mit.edu>
date Thu, 12 Nov 2015 08:46:51 -0500
parents 22117edf8fd3
children 1091227f535a
comparison
equal deleted inserted replaced
2279:32a407902d3b 2280:985c8016b592
686 (SgiDatatypeImp (x, n, m1, ms, s, xs, xncs'), loc)) 686 (SgiDatatypeImp (x, n, m1, ms, s, xs, xncs'), loc))
687 | SgiVal (x, n, c) => 687 | SgiVal (x, n, c) =>
688 S.map2 (con ctx c, 688 S.map2 (con ctx c,
689 fn c' => 689 fn c' =>
690 (SgiVal (x, n, c'), loc)) 690 (SgiVal (x, n, c'), loc))
691 | SgiStr (x, n, s) => 691 | SgiStr (im, x, n, s) =>
692 S.map2 (sg ctx s, 692 S.map2 (sg ctx s,
693 fn s' => 693 fn s' =>
694 (SgiStr (x, n, s'), loc)) 694 (SgiStr (im, x, n, s'), loc))
695 | SgiSgn (x, n, s) => 695 | SgiSgn (x, n, s) =>
696 S.map2 (sg ctx s, 696 S.map2 (sg ctx s,
697 fn s' => 697 fn s' =>
698 (SgiSgn (x, n, s'), loc)) 698 (SgiSgn (x, n, s'), loc))
699 | SgiConstraint (c1, c2) => 699 | SgiConstraint (c1, c2) =>
736 end) ctx dts 736 end) ctx dts
737 | SgiDatatypeImp (x, n, m1, ms, s, _, _) => 737 | SgiDatatypeImp (x, n, m1, ms, s, _, _) =>
738 bind (ctx, NamedC (x, n, (KType, loc), 738 bind (ctx, NamedC (x, n, (KType, loc),
739 SOME (CModProj (m1, ms, s), loc))) 739 SOME (CModProj (m1, ms, s), loc)))
740 | SgiVal _ => ctx 740 | SgiVal _ => ctx
741 | SgiStr (x, n, sgn) => 741 | SgiStr (_, x, n, sgn) =>
742 bind (ctx, Str (x, n, sgn)) 742 bind (ctx, Str (x, n, sgn))
743 | SgiSgn (x, n, sgn) => 743 | SgiSgn (x, n, sgn) =>
744 bind (ctx, Sgn (x, n, sgn)) 744 bind (ctx, Sgn (x, n, sgn))
745 | SgiConstraint _ => ctx 745 | SgiConstraint _ => ctx
746 | SgiClassAbs (x, n, k) => 746 | SgiClassAbs (x, n, k) =>
1268 (Int.max (n, max)) ns) 0 dts 1268 (Int.max (n, max)) ns) 0 dts
1269 | SgiDatatypeImp (_, n1, n2, _, _, _, ns) => 1269 | SgiDatatypeImp (_, n1, n2, _, _, _, ns) =>
1270 foldl (fn ((_, n', _), m) => Int.max (n', m)) 1270 foldl (fn ((_, n', _), m) => Int.max (n', m))
1271 (Int.max (n1, n2)) ns 1271 (Int.max (n1, n2)) ns
1272 | SgiVal (_, n, _) => n 1272 | SgiVal (_, n, _) => n
1273 | SgiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn) 1273 | SgiStr (_, _, n, sgn) => Int.max (n, maxNameSgn sgn)
1274 | SgiSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn) 1274 | SgiSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn)
1275 | SgiConstraint _ => 0 1275 | SgiConstraint _ => 0
1276 | SgiClassAbs (_, n, _) => n 1276 | SgiClassAbs (_, n, _) => n
1277 | SgiClass (_, n, _, _) => n 1277 | SgiClass (_, n, _, _) => n
1278 1278