Mercurial > urweb

comparison src/elab_util.sml @ 460:d34834af4512

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Cookies through explify
author Adam Chlipala <adamc@hcoop.net>
date Thu, 06 Nov 2008 10:43:48 -0500
parents f542bc3133dc
children ae03d09043c1
comparison
equal deleted inserted replaced
459:f542bc3133dc 460:d34834af4512
536 S.bind2 (con ctx c1, 536 S.bind2 (con ctx c1,
537 fn c1' => 537 fn c1' =>
538 S.map2 (con ctx c2, 538 S.map2 (con ctx c2,
539 fn c2' => 539 fn c2' =>
540 (SgiConstraint (c1', c2'), loc))) 540 (SgiConstraint (c1', c2'), loc)))
541 | SgiTable (tn, x, n, c) =>
542 S.map2 (con ctx c,
543 fn c' =>
544 (SgiTable (tn, x, n, c'), loc))
545 | SgiSequence _ => S.return2 siAll
546 | SgiClassAbs _ => S.return2 siAll 541 | SgiClassAbs _ => S.return2 siAll
547 | SgiClass (x, n, c) => 542 | SgiClass (x, n, c) =>
548 S.map2 (con ctx c, 543 S.map2 (con ctx c,
549 fn c' => 544 fn c' =>
550 (SgiClass (x, n, c'), loc)) 545 (SgiClass (x, n, c'), loc))
551 | SgiCookie (tn, x, n, c) =>
552 S.map2 (con ctx c,
553 fn c' =>
554 (SgiCookie (tn, x, n, c'), loc))
555 546
556 and sg ctx s acc = 547 and sg ctx s acc =
557 S.bindP (sg' ctx s acc, sgn ctx) 548 S.bindP (sg' ctx s acc, sgn ctx)
558 549
559 and sg' ctx (sAll as (s, loc)) = 550 and sg' ctx (sAll as (s, loc)) =
573 | SgiStr (x, _, sgn) => 564 | SgiStr (x, _, sgn) =>
574 bind (ctx, Str (x, sgn)) 565 bind (ctx, Str (x, sgn))
575 | SgiSgn (x, _, sgn) => 566 | SgiSgn (x, _, sgn) =>
576 bind (ctx, Sgn (x, sgn)) 567 bind (ctx, Sgn (x, sgn))
577 | SgiConstraint _ => ctx 568 | SgiConstraint _ => ctx
578 | SgiTable _ => ctx
579 | SgiSequence _ => ctx
580 | SgiClassAbs (x, n) => 569 | SgiClassAbs (x, n) =>
581 bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc))) 570 bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc)))
582 | SgiClass (x, n, _) => 571 | SgiClass (x, n, _) =>
583 bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc))) 572 bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc))),
584 | SgiCookie _ => ctx,
585 sgi ctx si)) ctx sgis, 573 sgi ctx si)) ctx sgis,
586 fn sgis' => 574 fn sgis' =>
587 (SgnConst sgis', loc)) 575 (SgnConst sgis', loc))
588 576
589 | SgnVar _ => S.return2 sAll 577 | SgnVar _ => S.return2 sAll
1003 (Int.max (n1, n2)) ns 991 (Int.max (n1, n2)) ns
1004 | SgiVal (_, n, _) => n 992 | SgiVal (_, n, _) => n
1005 | SgiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn) 993 | SgiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn)
1006 | SgiSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn) 994 | SgiSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn)
1007 | SgiConstraint _ => 0 995 | SgiConstraint _ => 0
1008 | SgiTable (n1, _, n2, _) => Int.max (n1, n2)
1009 | SgiSequence (n1, _, n2) => Int.max (n1, n2)
1010 | SgiClassAbs (_, n) => n 996 | SgiClassAbs (_, n) => n
1011 | SgiClass (_, n, _) => n 997 | SgiClass (_, n, _) => n
1012 | SgiCookie (n1, _, n2, _) => Int.max (n1, n2)
1013 998
1014 end 999 end
1015 1000
1016 end 1001 end