diff src/elab_util.sml @ 459:f542bc3133dc

Cookies through elaborate
author Adam Chlipala <adamc@hcoop.net>
date Thu, 06 Nov 2008 10:29:55 -0500
parents 787d4931fb07
children d34834af4512
line wrap: on
line diff
--- a/src/elab_util.sml	Thu Nov 06 10:04:03 2008 -0500
+++ b/src/elab_util.sml	Thu Nov 06 10:29:55 2008 -0500
@@ -548,6 +548,10 @@
                 S.map2 (con ctx c,
                         fn c' =>
                            (SgiClass (x, n, c'), loc))
+              | SgiCookie (tn, x, n, c) =>
+                S.map2 (con ctx c,
+                        fn c' =>
+                           (SgiCookie (tn, x, n, c'), loc))
 
         and sg ctx s acc =
             S.bindP (sg' ctx s acc, sgn ctx)
@@ -576,7 +580,8 @@
                                                  | SgiClassAbs (x, n) =>
                                                    bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc)))
                                                  | SgiClass (x, n, _) =>
-                                                   bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc))),
+                                                   bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc)))
+                                                 | SgiCookie _ => ctx,
                                                sgi ctx si)) ctx sgis,
                      fn sgis' =>
                         (SgnConst sgis', loc))
@@ -720,7 +725,10 @@
                                                    bind (ctx, NamedE (x, (CModProj (n, [], "sql_sequence"), loc)))
                                                  | DClass (x, n, _) =>
                                                    bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc)))
-                                                 | DDatabase _ => ctx,
+                                                 | DDatabase _ => ctx
+                                                 | DCookie (tn, x, n, c) =>
+                                                   bind (ctx, NamedE (x, (CApp ((CModProj (n, [], "cookie"), loc),
+                                                                                c), loc))),
                                                mfd ctx d)) ctx ds,
                      fn ds' => (StrConst ds', loc))
               | StrVar _ => S.return2 strAll
@@ -821,6 +829,11 @@
 
               | DDatabase _ => S.return2 dAll
 
+              | DCookie (tn, x, n, c) =>
+                S.map2 (mfc ctx c,
+                        fn c' =>
+                           (DCookie (tn, x, n, c'), loc))
+
         and mfvi ctx (x, n, c, e) =
             S.bind2 (mfc ctx c,
                   fn c' =>
@@ -955,9 +968,10 @@
       | DConstraint _ => 0
       | DClass (_, n, _) => n
       | DExport _ => 0
-      | DTable (n, _, _, _) => n
-      | DSequence (n, _, _) => n
+      | DTable (n1, _, n2, _) => Int.max (n1, n2)
+      | DSequence (n1, _, n2) => Int.max (n1, n2)
       | DDatabase _ => 0
+      | DCookie (n1, _, n2, _) => Int.max (n1, n2)
 
 and maxNameStr (str, _) =
     case str of
@@ -991,10 +1005,11 @@
       | SgiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn)
       | SgiSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn)
       | SgiConstraint _ => 0
-      | SgiTable (n, _, _, _) => n
-      | SgiSequence (n, _, _) => n
+      | SgiTable (n1, _, n2, _) => Int.max (n1, n2)
+      | SgiSequence (n1, _, n2) => Int.max (n1, n2)
       | SgiClassAbs (_, n) => n
       | SgiClass (_, n, _) => n
+      | SgiCookie (n1, _, n2, _) => Int.max (n1, n2)
               
 end