Stub WHERE support

6 files changed, 66 insertions, 10 deletions

diff --git a/lib/basis.lig b/lib/basis.lig
index 0655c2b7..6fe847b9 100644
--- a/lib/basis.lig
+++ b/lib/basis.lig
@@ -14,14 +14,26 @@ con sql_table :: {Type} -> Type
 (*** Queries *)
 
 con sql_query :: {{Type}} -> Type
+con sql_exp :: {{Type}} -> Type -> Type
 
 val sql_query : tables :: {({Type} * {Type})}
-        -> $(fold (fn nm => fn selected_unselected :: ({Type} * {Type}) => fn acc =>
+        -> {From : $(fold (fn nm => fn selected_unselected :: ({Type} * {Type}) => fn acc =>
                 [nm] ~ acc => selected_unselected.1 ~ selected_unselected.2 =>
-                [nm = sql_table (selected_unselected.1 ++ selected_unselected.2)] ++ acc) [] tables)
+                [nm = sql_table (selected_unselected.1 ++ selected_unselected.2)] ++ acc) [] tables),
+            Where : sql_exp (fold (fn nm => fn selected_unselected :: ({Type} * {Type}) => fn acc =>
+                [nm] ~ acc => selected_unselected.1 ~ selected_unselected.2 =>
+                [nm = selected_unselected.1 ++ selected_unselected.2] ++ acc) [] tables) bool}
         -> sql_query (fold (fn nm => fn selected_unselected :: ({Type} * {Type}) => fn acc => [nm] ~ acc =>
                 [nm = selected_unselected.1] ++ acc) [] tables)
 
+con sql_type :: Type -> Type
+val sql_bool : sql_type bool
+val sql_int : sql_type int
+val sql_float : sql_type float
+val sql_string : sql_type string
+
+val sql_inject : tables ::: {{Type}} -> t ::: Type -> t -> sql_type t -> sql_exp tables t
+
 
 (** XML *)
 
diff --git a/src/elab_ops.sml b/src/elab_ops.sml
index a0fa0c18..50c95ac7 100644
--- a/src/elab_ops.sml
+++ b/src/elab_ops.sml
@@ -136,6 +136,7 @@ fun hnormCon env (cAll as (c, loc)) =
            | ((CRecord (_, []), _), c2') => c2'
            | ((CConcat (c11, c12), loc), c2') =>
              hnormCon env (CConcat (c11, (CConcat (c12, c2'), loc)), loc)
+           | (c1', (CRecord (_, []), _)) => c1'
            | _ => cAll)
 
       | CProj (c, n) =>
diff --git a/src/elaborate.sml b/src/elaborate.sml
index beea1a76..41c9e6df 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -682,9 +682,14 @@ and recordSummary (env, denv) c =
     end
 
 and consEq (env, denv) (c1, c2) =
-    (case unifyCons (env, denv) c1 c2 of
-         [] => true
-       | _ => false)
+    let
+        val gs = unifyCons (env, denv) c1 c2
+    in
+        List.all (fn (loc, env, denv, c1, c2) =>
+                     case D.prove env denv (c1, c2, loc) of
+                         [] => true
+                       | _ => false) gs
+    end
     handle CUnify _ => false
 
 and consNeq env (c1, c2) =
@@ -857,7 +862,9 @@ and unifyCons' (env, denv) c1 c2 =
     
 and unifyCons'' (env, denv) (c1All as (c1, loc)) (c2All as (c2, _)) =
     let
-        fun err f = raise CUnify' (f (c1All, c2All))
+        fun err f = (prefaces "unifyCons'' fails" [("c1All", p_con env c1All),
+                                                   ("c2All", p_con env c2All)];
+                     raise CUnify' (f (c1All, c2All)))
 
         fun isRecord () = unifyRecordCons (env, denv) (c1All, c2All)
     in
@@ -956,7 +963,6 @@ and unifyCons'' (env, denv) (c1All as (c1, loc)) (c2All as (c2, _)) =
              unifyKinds ran1 ran2;
              [])
 
-
           | _ => err CIncompatible
     end
 
diff --git a/src/lacweb.grm b/src/lacweb.grm
index 73d79c52..13e464c4 100644
--- a/src/lacweb.grm
+++ b/src/lacweb.grm
@@ -72,6 +72,13 @@ fun amend_select loc (si, tabs) =
         tabs
     end
 
+fun sql_inject (v, t, loc) =
+    let
+        val e = (EApp ((EVar (["Basis"], "sql_inject"), loc), (v, loc)), loc)
+    in
+        (EApp (e, (t, loc)), loc)
+    end
+
 %%
 %header (functor LacwebLrValsFn(structure Token : TOKEN))
 
@@ -95,7 +102,8 @@ fun amend_select loc (si, tabs) =
  | NOTAGS of string 
  | BEGIN_TAG of string | END_TAG of string
 
- | SELECT | FROM | AS
+ | SELECT | FROM | AS | CWHERE
+ | TRUE | FALSE
 
 %nonterm
    file of decl list
@@ -166,6 +174,8 @@ fun amend_select loc (si, tabs) =
  | seli of select_item
  | selis of select_item list
  | select of select
+ | sqlexp of exp
+ | wopt of exp
 
 
 %verbose                                (* print summary of errors *)
@@ -554,7 +564,8 @@ attrv  : INT                            (EPrim (Prim.Int INT), s (INTleft, INTri
        | STRING                         (EPrim (Prim.String STRING), s (STRINGleft, STRINGright))
        | LBRACE eexp RBRACE             (eexp)
                 
-query  : SELECT select FROM tables      (let
+query  : SELECT select FROM tables wopt
+                                        (let
                                              val loc = s (SELECTleft, tablesright)
 
                                              val sel =
@@ -579,7 +590,11 @@ query  : SELECT select FROM tables      (let
 
                                              val e = (EVar (["Basis"], "sql_query"), loc)
                                              val e = (ECApp (e, sel), loc)
-                                             val e = (EApp (e, (ERecord tables, loc)), loc)
+                                             val re = (ERecord [((CName "From", loc),
+                                                                 (ERecord tables, loc)),
+                                                                ((CName "Where", loc),
+                                                                 wopt)], loc)
+                                             val e = (EApp (e, re), loc)
                                          in
                                              e
                                          end)
@@ -609,3 +624,15 @@ selis  : seli                           ([seli])
 
 select : STAR                           (Star)
        | selis                          (Items selis)
+
+sqlexp : TRUE                           (sql_inject (EVar (["Basis"], "True"),
+                                                     EVar (["Basis"], "sql_bool"),
+                                                     s (TRUEleft, TRUEright)))
+       | FALSE                          (sql_inject (EVar (["Basis"], "False"),
+                                                     EVar (["Basis"], "sql_bool"),
+                                                     s (FALSEleft, FALSEright)))
+
+wopt   :                                (sql_inject (EVar (["Basis"], "True"),
+                                                     EVar (["Basis"], "sql_bool"),
+                                                     ErrorMsg.dummySpan))
+       | CWHERE sqlexp                  (sqlexp)
diff --git a/src/lacweb.lex b/src/lacweb.lex
index 50fe7f26..9e994b27 100644
--- a/src/lacweb.lex
+++ b/src/lacweb.lex
@@ -288,6 +288,10 @@ notags = [^<{\n]+;
 <INITIAL> "SELECT"    => (Tokens.SELECT (pos yypos, pos yypos + size yytext));
 <INITIAL> "FROM"      => (Tokens.FROM (pos yypos, pos yypos + size yytext));
 <INITIAL> "AS"        => (Tokens.AS (pos yypos, pos yypos + size yytext));
+<INITIAL> "WHERE"     => (Tokens.CWHERE (pos yypos, pos yypos + size yytext));
+
+<INITIAL> "TRUE"      => (Tokens.TRUE (pos yypos, pos yypos + size yytext));
+<INITIAL> "FALSE"     => (Tokens.FALSE (pos yypos, pos yypos + size yytext));
 
 <INITIAL> {id}        => (Tokens.SYMBOL (yytext, pos yypos, pos yypos + size yytext));
 <INITIAL> {cid}       => (Tokens.CSYMBOL (yytext, pos yypos, pos yypos + size yytext));
diff --git a/tests/where.lac b/tests/where.lac
new file mode 100644
index 00000000..1454583b
--- /dev/null
+++ b/tests/where.lac
@@ -0,0 +1,6 @@
+table t1 : {A : int, B : string, C : float}
+table t2 : {A : float, D : int}
+
+val q1 = (SELECT * FROM t1)
+val q2 = (SELECT * FROM t1 WHERE TRUE)
+val q3 = (SELECT * FROM t1 WHERE FALSE)