Mercurial > urweb

comparison src/elab_util.sml @ 705:e6706a1df013

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Track uniqueness sets in table types
author Adam Chlipala <adamc@hcoop.net>
date Tue, 07 Apr 2009 14:11:32 -0400
parents 70cbdcf5989b
children d8217b4cb617
comparison
equal deleted inserted replaced
704:70cbdcf5989b 705:e6706a1df013
764 bind (ctx, Str (x, sgn)) 764 bind (ctx, Str (x, sgn))
765 | DFfiStr (x, _, sgn) => 765 | DFfiStr (x, _, sgn) =>
766 bind (ctx, Str (x, sgn)) 766 bind (ctx, Str (x, sgn))
767 | DConstraint _ => ctx 767 | DConstraint _ => ctx
768 | DExport _ => ctx 768 | DExport _ => ctx
769 | DTable (tn, x, n, c, _) => 769 | DTable (tn, x, n, c, _, cc) =>
770 bind (ctx, NamedE (x, (CApp ((CModProj (n, [], "sql_table"), loc), 770 let
771 c), loc))) 771 val ct = (CModProj (n, [], "sql_table"), loc)
772 val ct = (CApp (ct, c), loc)
773 val ct = (CApp (ct, cc), loc)
774 in
775 bind (ctx, NamedE (x, ct))
776 end
772 | DSequence (tn, x, n) => 777 | DSequence (tn, x, n) =>
773 bind (ctx, NamedE (x, (CModProj (n, [], "sql_sequence"), loc))) 778 bind (ctx, NamedE (x, (CModProj (n, [], "sql_sequence"), loc)))
774 | DClass (x, n, k, _) => 779 | DClass (x, n, k, _) =>
775 bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc))) 780 bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc)))
776 | DDatabase _ => ctx 781 | DDatabase _ => ctx
862 fn sgn' => 867 fn sgn' =>
863 S.map2 (mfst ctx str, 868 S.map2 (mfst ctx str,
864 fn str' => 869 fn str' =>
865 (DExport (en, sgn', str'), loc))) 870 (DExport (en, sgn', str'), loc)))
866 871
867 | DTable (tn, x, n, c, e) => 872 | DTable (tn, x, n, c, e, cc) =>
868 S.bind2 (mfc ctx c, 873 S.bind2 (mfc ctx c,
869 fn c' => 874 fn c' =>
870 S.map2 (mfe ctx e, 875 S.bind2 (mfe ctx e,
871 fn e' => 876 fn e' =>
872 (DTable (tn, x, n, c', e'), loc))) 877 S.map2 (mfc ctx cc,
878 fn cc' =>
879 (DTable (tn, x, n, c', e', cc'), loc))))
873 | DSequence _ => S.return2 dAll 880 | DSequence _ => S.return2 dAll
874 881
875 | DClass (x, n, k, c) => 882 | DClass (x, n, k, c) =>
876 S.bind2 (mfk ctx k, 883 S.bind2 (mfk ctx k,
877 fn k' => 884 fn k' =>
1018 | DSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn) 1025 | DSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn)
1019 | DFfiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn) 1026 | DFfiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn)
1020 | DConstraint _ => 0 1027 | DConstraint _ => 0
1021 | DClass (_, n, _, _) => n 1028 | DClass (_, n, _, _) => n
1022 | DExport _ => 0 1029 | DExport _ => 0
1023 | DTable (n1, _, n2, _, _) => Int.max (n1, n2) 1030 | DTable (n1, _, n2, _, _, _) => Int.max (n1, n2)
1024 | DSequence (n1, _, n2) => Int.max (n1, n2) 1031 | DSequence (n1, _, n2) => Int.max (n1, n2)
1025 | DDatabase _ => 0 1032 | DDatabase _ => 0
1026 | DCookie (n1, _, n2, _) => Int.max (n1, n2) 1033 | DCookie (n1, _, n2, _) => Int.max (n1, n2)
1027 1034
1028 and maxNameStr (str, _) = 1035 and maxNameStr (str, _) =