Mercurial > urweb

comparison src/elab_util.sml @ 563:44958d74c43f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Initial conversion to arbitrary-kind classes
author Adam Chlipala <adamc@hcoop.net>
date Fri, 19 Dec 2008 10:03:31 -0500
parents ae03d09043c1
children 8998114760c1
comparison
equal deleted inserted replaced
562:6daa59a55c43 563:44958d74c43f
545 S.bind2 (con ctx c1, 545 S.bind2 (con ctx c1,
546 fn c1' => 546 fn c1' =>
547 S.map2 (con ctx c2, 547 S.map2 (con ctx c2,
548 fn c2' => 548 fn c2' =>
549 (SgiConstraint (c1', c2'), loc))) 549 (SgiConstraint (c1', c2'), loc)))
550 | SgiClassAbs _ => S.return2 siAll 550 | SgiClassAbs (x, n, k) =>
551 | SgiClass (x, n, c) => 551 S.map2 (kind k,
552 S.map2 (con ctx c, 552 fn k' =>
553 fn c' => 553 (SgiClassAbs (x, n, k'), loc))
554 (SgiClass (x, n, c'), loc)) 554 | SgiClass (x, n, k, c) =>
555 S.bind2 (kind k,
556 fn k' =>
557 S.map2 (con ctx c,
558 fn c' =>
559 (SgiClass (x, n, k', c'), loc)))
555 560
556 and sg ctx s acc = 561 and sg ctx s acc =
557 S.bindP (sg' ctx s acc, sgn ctx) 562 S.bindP (sg' ctx s acc, sgn ctx)
558 563
559 and sg' ctx (sAll as (s, loc)) = 564 and sg' ctx (sAll as (s, loc)) =
573 | SgiStr (x, _, sgn) => 578 | SgiStr (x, _, sgn) =>
574 bind (ctx, Str (x, sgn)) 579 bind (ctx, Str (x, sgn))
575 | SgiSgn (x, _, sgn) => 580 | SgiSgn (x, _, sgn) =>
576 bind (ctx, Sgn (x, sgn)) 581 bind (ctx, Sgn (x, sgn))
577 | SgiConstraint _ => ctx 582 | SgiConstraint _ => ctx
578 | SgiClassAbs (x, n) => 583 | SgiClassAbs (x, n, k) =>
579 bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc))) 584 bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc)))
580 | SgiClass (x, n, _) => 585 | SgiClass (x, n, k, _) =>
581 bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc))), 586 bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc))),
582 sgi ctx si)) ctx sgis, 587 sgi ctx si)) ctx sgis,
583 fn sgis' => 588 fn sgis' =>
584 (SgnConst sgis', loc)) 589 (SgnConst sgis', loc))
585 590
586 | SgnVar _ => S.return2 sAll 591 | SgnVar _ => S.return2 sAll
718 | DTable (tn, x, n, c) => 723 | DTable (tn, x, n, c) =>
719 bind (ctx, NamedE (x, (CApp ((CModProj (n, [], "sql_table"), loc), 724 bind (ctx, NamedE (x, (CApp ((CModProj (n, [], "sql_table"), loc),
720 c), loc))) 725 c), loc)))
721 | DSequence (tn, x, n) => 726 | DSequence (tn, x, n) =>
722 bind (ctx, NamedE (x, (CModProj (n, [], "sql_sequence"), loc))) 727 bind (ctx, NamedE (x, (CModProj (n, [], "sql_sequence"), loc)))
723 | DClass (x, n, _) => 728 | DClass (x, n, k, _) =>
724 bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc))) 729 bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc)))
725 | DDatabase _ => ctx 730 | DDatabase _ => ctx
726 | DCookie (tn, x, n, c) => 731 | DCookie (tn, x, n, c) =>
727 bind (ctx, NamedE (x, (CApp ((CModProj (n, [], "cookie"), loc), 732 bind (ctx, NamedE (x, (CApp ((CModProj (n, [], "cookie"), loc),
728 c), loc))), 733 c), loc))),
729 mfd ctx d)) ctx ds, 734 mfd ctx d)) ctx ds,
817 S.map2 (mfc ctx c, 822 S.map2 (mfc ctx c,
818 fn c' => 823 fn c' =>
819 (DTable (tn, x, n, c'), loc)) 824 (DTable (tn, x, n, c'), loc))
820 | DSequence _ => S.return2 dAll 825 | DSequence _ => S.return2 dAll
821 826
822 | DClass (x, n, c) => 827 | DClass (x, n, k, c) =>
823 S.map2 (mfc ctx c, 828 S.bind2 (mfk k,
824 fn c' => 829 fn k' =>
825 (DClass (x, n, c'), loc)) 830 S.map2 (mfc ctx c,
831 fn c' =>
832 (DClass (x, n, k', c'), loc)))
826 833
827 | DDatabase _ => S.return2 dAll 834 | DDatabase _ => S.return2 dAll
828 835
829 | DCookie (tn, x, n, c) => 836 | DCookie (tn, x, n, c) =>
830 S.map2 (mfc ctx c, 837 S.map2 (mfc ctx c,
961 | DValRec vis => foldl (fn ((_, n, _, _), count) => Int.max (n, count)) 0 vis 968 | DValRec vis => foldl (fn ((_, n, _, _), count) => Int.max (n, count)) 0 vis
962 | DStr (_, n, sgn, str) => Int.max (n, Int.max (maxNameSgn sgn, maxNameStr str)) 969 | DStr (_, n, sgn, str) => Int.max (n, Int.max (maxNameSgn sgn, maxNameStr str))
963 | DSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn) 970 | DSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn)
964 | DFfiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn) 971 | DFfiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn)
965 | DConstraint _ => 0 972 | DConstraint _ => 0
966 | DClass (_, n, _) => n 973 | DClass (_, n, _, _) => n
967 | DExport _ => 0 974 | DExport _ => 0
968 | DTable (n1, _, n2, _) => Int.max (n1, n2) 975 | DTable (n1, _, n2, _) => Int.max (n1, n2)
969 | DSequence (n1, _, n2) => Int.max (n1, n2) 976 | DSequence (n1, _, n2) => Int.max (n1, n2)
970 | DDatabase _ => 0 977 | DDatabase _ => 0
971 | DCookie (n1, _, n2, _) => Int.max (n1, n2) 978 | DCookie (n1, _, n2, _) => Int.max (n1, n2)
1000 (Int.max (n1, n2)) ns 1007 (Int.max (n1, n2)) ns
1001 | SgiVal (_, n, _) => n 1008 | SgiVal (_, n, _) => n
1002 | SgiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn) 1009 | SgiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn)
1003 | SgiSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn) 1010 | SgiSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn)
1004 | SgiConstraint _ => 0 1011 | SgiConstraint _ => 0
1005 | SgiClassAbs (_, n) => n 1012 | SgiClassAbs (_, n, _) => n
1006 | SgiClass (_, n, _) => n 1013 | SgiClass (_, n, _, _) => n
1007 1014
1008 end 1015 end
1009 1016
1010 end 1017 end