diff src/elaborate.sml @ 338:e976b187d73a

SQL sequences
author Adam Chlipala <adamc@hcoop.net>
date Sun, 14 Sep 2008 11:02:18 -0400
parents 9601c717d2f3
children 075b36dbb1a4
line wrap: on
line diff
--- a/src/elaborate.sml	Sat Sep 13 20:15:30 2008 -0400
+++ b/src/elaborate.sml	Sun Sep 14 11:02:18 2008 -0400
@@ -1648,6 +1648,7 @@
 val hnormSgn = E.hnormSgn
 
 fun tableOf () = (L'.CModProj (!basis_r, [], "sql_table"), ErrorMsg.dummySpan)
+fun sequenceOf () = (L'.CModProj (!basis_r, [], "sql_sequence"), ErrorMsg.dummySpan)
 
 fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
     case sgi of
@@ -1828,6 +1829,13 @@
             ([(L'.SgiTable (!basis_r, x, n, c'), loc)], (env, denv, gs))
         end
 
+      | L.SgiSequence x =>
+        let
+            val (env, n) = E.pushENamed env x (sequenceOf ())
+        in
+            ([(L'.SgiSequence (!basis_r, x, n), loc)], (env, denv, gs))
+        end
+
       | L.SgiClassAbs x =>
         let
             val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
@@ -1915,6 +1923,12 @@
                                    else
                                        ();
                                    (cons, SS.add (vals, x), sgns, strs))
+                                | L'.SgiSequence (_, x, _) =>
+                                  (if SS.member (vals, x) then
+                                       sgnError env (DuplicateVal (loc, x))
+                                   else
+                                       ();
+                                   (cons, SS.add (vals, x), sgns, strs))
                                 | L'.SgiClassAbs (x, _) =>
                                   (if SS.member (cons, x) then
                                        sgnError env (DuplicateCon (loc, x))
@@ -2061,6 +2075,9 @@
                                             | L'.SgiTable (_, x, n, c) =>
                                               (L'.DVal (x, n, (L'.CApp (tableOf (), c), loc),
                                                         (L'.EModProj (str, strs, x), loc)), loc)
+                                            | L'.SgiSequence (_, x, n) =>
+                                              (L'.DVal (x, n, sequenceOf (),
+                                                        (L'.EModProj (str, strs, x), loc)), loc)
                                             | L'.SgiClassAbs (x, n) =>
                                               let
                                                   val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
@@ -2128,6 +2145,7 @@
       | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)]
       | L'.DExport _ => []
       | L'.DTable (tn, x, n, c) => [(L'.SgiTable (tn, x, n, c), loc)]
+      | L'.DSequence (tn, x, n) => [(L'.SgiSequence (tn, x, n), loc)]
       | L'.DClass (x, n, c) => [(L'.SgiClass (x, n, c), loc)]
       | L'.DDatabase _ => []
 
@@ -2355,6 +2373,16 @@
                                                  SOME (env, denv))
                                      else
                                          NONE
+                                   | L'.SgiSequence (_, x', n1) =>
+                                     if x = x' then
+                                         (case unifyCons (env, denv) (sequenceOf ()) c2 of
+                                              [] => SOME (env, denv)
+                                            | _ => NONE)
+                                         handle CUnify (c1, c2, err) =>
+                                                (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
+                                                 SOME (env, denv))
+                                     else
+                                         NONE
                                    | _ => NONE)
 
                       | L'.SgiStr (x, n2, sgn2) =>
@@ -2432,6 +2460,16 @@
                                          NONE
                                    | _ => NONE)
 
+                      | L'.SgiSequence (_, x, n2) =>
+                        seek (fn sgi1All as (sgi1, _) =>
+                                 case sgi1 of
+                                     L'.SgiSequence (_, x', n1) =>
+                                     if x = x' then
+                                         SOME (env, denv)
+                                     else
+                                         NONE
+                                   | _ => NONE)
+
                       | L'.SgiClassAbs (x, n2) =>
                         seek (fn sgi1All as (sgi1, _) =>
                                  let
@@ -3024,6 +3062,12 @@
                     checkKind env c' k (L'.KRecord (L'.KType, loc), loc);
                     ([(L'.DTable (!basis_r, x, n, c'), loc)], (env, denv, enD gs' @ gs))
                 end
+              | L.DSequence x =>
+                let
+                    val (env, n) = E.pushENamed env x (sequenceOf ())
+                in
+                    ([(L'.DSequence (!basis_r, x, n), loc)], (env, denv, gs))
+                end
 
               | L.DClass (x, c) =>
                 let
@@ -3147,6 +3191,16 @@
                               in
                                   ((L'.SgiTable (tn, x, n, c), loc) :: sgis, cons, vals, sgns, strs)
                               end
+                            | L'.SgiSequence (tn, x, n) =>
+                              let
+                                  val (vals, x) =
+                                      if SS.member (vals, x) then
+                                          (vals, "?" ^ x)
+                                      else
+                                          (SS.add (vals, x), x)
+                              in
+                                  ((L'.SgiSequence (tn, x, n), loc) :: sgis, cons, vals, sgns, strs)
+                              end
                             | L'.SgiClassAbs (x, n) =>
                               let
                                   val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)