Mercurial > urweb

comparison src/elab_util.sml @ 459:f542bc3133dc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Cookies through elaborate
author Adam Chlipala <adamc@hcoop.net>
date Thu, 06 Nov 2008 10:29:55 -0500
parents 787d4931fb07
children d34834af4512
comparison
equal deleted inserted replaced
458:8f65b0fa3b29 459:f542bc3133dc
546 | SgiClassAbs _ => S.return2 siAll 546 | SgiClassAbs _ => S.return2 siAll
547 | SgiClass (x, n, c) => 547 | SgiClass (x, n, c) =>
548 S.map2 (con ctx c, 548 S.map2 (con ctx c,
549 fn c' => 549 fn c' =>
550 (SgiClass (x, n, c'), loc)) 550 (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))
551 555
552 and sg ctx s acc = 556 and sg ctx s acc =
553 S.bindP (sg' ctx s acc, sgn ctx) 557 S.bindP (sg' ctx s acc, sgn ctx)
554 558
555 and sg' ctx (sAll as (s, loc)) = 559 and sg' ctx (sAll as (s, loc)) =
574 | SgiTable _ => ctx 578 | SgiTable _ => ctx
575 | SgiSequence _ => ctx 579 | SgiSequence _ => ctx
576 | SgiClassAbs (x, n) => 580 | SgiClassAbs (x, n) =>
577 bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc))) 581 bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc)))
578 | SgiClass (x, n, _) => 582 | SgiClass (x, n, _) =>
579 bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc))), 583 bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc)))
584 | SgiCookie _ => ctx,
580 sgi ctx si)) ctx sgis, 585 sgi ctx si)) ctx sgis,
581 fn sgis' => 586 fn sgis' =>
582 (SgnConst sgis', loc)) 587 (SgnConst sgis', loc))
583 588
584 | SgnVar _ => S.return2 sAll 589 | SgnVar _ => S.return2 sAll
718 c), loc))) 723 c), loc)))
719 | DSequence (tn, x, n) => 724 | DSequence (tn, x, n) =>
720 bind (ctx, NamedE (x, (CModProj (n, [], "sql_sequence"), loc))) 725 bind (ctx, NamedE (x, (CModProj (n, [], "sql_sequence"), loc)))
721 | DClass (x, n, _) => 726 | DClass (x, n, _) =>
722 bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc))) 727 bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc)))
723 | DDatabase _ => ctx, 728 | DDatabase _ => ctx
729 | DCookie (tn, x, n, c) =>
730 bind (ctx, NamedE (x, (CApp ((CModProj (n, [], "cookie"), loc),
731 c), loc))),
724 mfd ctx d)) ctx ds, 732 mfd ctx d)) ctx ds,
725 fn ds' => (StrConst ds', loc)) 733 fn ds' => (StrConst ds', loc))
726 | StrVar _ => S.return2 strAll 734 | StrVar _ => S.return2 strAll
727 | StrProj (str, x) => 735 | StrProj (str, x) =>
728 S.map2 (mfst ctx str, 736 S.map2 (mfst ctx str,
819 fn c' => 827 fn c' =>
820 (DClass (x, n, c'), loc)) 828 (DClass (x, n, c'), loc))
821 829
822 | DDatabase _ => S.return2 dAll 830 | DDatabase _ => S.return2 dAll
823 831
832 | DCookie (tn, x, n, c) =>
833 S.map2 (mfc ctx c,
834 fn c' =>
835 (DCookie (tn, x, n, c'), loc))
836
824 and mfvi ctx (x, n, c, e) = 837 and mfvi ctx (x, n, c, e) =
825 S.bind2 (mfc ctx c, 838 S.bind2 (mfc ctx c,
826 fn c' => 839 fn c' =>
827 S.map2 (mfe ctx e, 840 S.map2 (mfe ctx e,
828 fn e' => 841 fn e' =>
953 | DSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn) 966 | DSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn)
954 | DFfiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn) 967 | DFfiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn)
955 | DConstraint _ => 0 968 | DConstraint _ => 0
956 | DClass (_, n, _) => n 969 | DClass (_, n, _) => n
957 | DExport _ => 0 970 | DExport _ => 0
958 | DTable (n, _, _, _) => n 971 | DTable (n1, _, n2, _) => Int.max (n1, n2)
959 | DSequence (n, _, _) => n 972 | DSequence (n1, _, n2) => Int.max (n1, n2)
960 | DDatabase _ => 0 973 | DDatabase _ => 0
974 | DCookie (n1, _, n2, _) => Int.max (n1, n2)
961 975
962 and maxNameStr (str, _) = 976 and maxNameStr (str, _) =
963 case str of 977 case str of
964 StrConst ds => maxName ds 978 StrConst ds => maxName ds
965 | StrVar n => n 979 | StrVar n => n
989 (Int.max (n1, n2)) ns 1003 (Int.max (n1, n2)) ns
990 | SgiVal (_, n, _) => n 1004 | SgiVal (_, n, _) => n
991 | SgiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn) 1005 | SgiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn)
992 | SgiSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn) 1006 | SgiSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn)
993 | SgiConstraint _ => 0 1007 | SgiConstraint _ => 0
994 | SgiTable (n, _, _, _) => n 1008 | SgiTable (n1, _, n2, _) => Int.max (n1, n2)
995 | SgiSequence (n, _, _) => n 1009 | SgiSequence (n1, _, n2) => Int.max (n1, n2)
996 | SgiClassAbs (_, n) => n 1010 | SgiClassAbs (_, n) => n
997 | SgiClass (_, n, _) => n 1011 | SgiClass (_, n, _) => n
1012 | SgiCookie (n1, _, n2, _) => Int.max (n1, n2)
998 1013
999 end 1014 end
1000 1015
1001 end 1016 end