Stub WHERE support

4 files changed, 46 insertions, 8 deletions

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));