comparison src/elab_util.sml @ 707:d8217b4cb617

PRIMARY KEY
author Adam Chlipala <adamc@hcoop.net>
date Tue, 07 Apr 2009 16:14:31 -0400
parents e6706a1df013
children 7292bcb7c02d
comparison
equal deleted inserted replaced
706:1fb318c17546 707:d8217b4cb617
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, _, cc) => 769 | DTable (tn, x, n, c, _, pc, _, cc) =>
770 let 770 let
771 val ct = (CModProj (n, [], "sql_table"), loc) 771 val ct = (CModProj (n, [], "sql_table"), loc)
772 val ct = (CApp (ct, c), loc) 772 val ct = (CApp (ct, c), loc)
773 val ct = (CApp (ct, cc), loc) 773 val ct = (CApp (ct, (CConcat (pc, cc), loc)), loc)
774 in 774 in
775 bind (ctx, NamedE (x, ct)) 775 bind (ctx, NamedE (x, ct))
776 end 776 end
777 | DSequence (tn, x, n) => 777 | DSequence (tn, x, n) =>
778 bind (ctx, NamedE (x, (CModProj (n, [], "sql_sequence"), loc))) 778 bind (ctx, NamedE (x, (CModProj (n, [], "sql_sequence"), loc)))
867 fn sgn' => 867 fn sgn' =>
868 S.map2 (mfst ctx str, 868 S.map2 (mfst ctx str,
869 fn str' => 869 fn str' =>
870 (DExport (en, sgn', str'), loc))) 870 (DExport (en, sgn', str'), loc)))
871 871
872 | DTable (tn, x, n, c, e, cc) => 872 | DTable (tn, x, n, c, pe, pc, ce, cc) =>
873 S.bind2 (mfc ctx c, 873 S.bind2 (mfc ctx c,
874 fn c' => 874 fn c' =>
875 S.bind2 (mfe ctx e, 875 S.bind2 (mfe ctx pe,
876 fn e' => 876 fn pe' =>
877 S.map2 (mfc ctx cc, 877 S.bind2 (mfc ctx pc,
878 fn cc' => 878 fn pc' =>
879 (DTable (tn, x, n, c', e', cc'), loc)))) 879 S.bind2 (mfe ctx ce,
880 fn ce' =>
881 S.map2 (mfc ctx cc,
882 fn cc' =>
883 (DTable (tn, x, n, c', pe', pc', ce', cc'), loc))))))
880 | DSequence _ => S.return2 dAll 884 | DSequence _ => S.return2 dAll
881 885
882 | DClass (x, n, k, c) => 886 | DClass (x, n, k, c) =>
883 S.bind2 (mfk ctx k, 887 S.bind2 (mfk ctx k,
884 fn k' => 888 fn k' =>
1025 | DSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn) 1029 | DSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn)
1026 | DFfiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn) 1030 | DFfiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn)
1027 | DConstraint _ => 0 1031 | DConstraint _ => 0
1028 | DClass (_, n, _, _) => n 1032 | DClass (_, n, _, _) => n
1029 | DExport _ => 0 1033 | DExport _ => 0
1030 | DTable (n1, _, n2, _, _, _) => Int.max (n1, n2) 1034 | DTable (n1, _, n2, _, _, _, _, _) => Int.max (n1, n2)
1031 | DSequence (n1, _, n2) => Int.max (n1, n2) 1035 | DSequence (n1, _, n2) => Int.max (n1, n2)
1032 | DDatabase _ => 0 1036 | DDatabase _ => 0
1033 | DCookie (n1, _, n2, _) => Int.max (n1, n2) 1037 | DCookie (n1, _, n2, _) => Int.max (n1, n2)
1034 1038
1035 and maxNameStr (str, _) = 1039 and maxNameStr (str, _) =