fix string parsing

dsl/CosetteParser.lhs

@@ -786,7 +786,13 @@ In this pass, we collect all string literals, and make constant declarations for
 > closeParen = lexeme $ char ')'
 
 > stringToken :: Parser String
-> stringToken = lexeme (char '\'' *> manyTill anyChar (char '\''))
+> stringToken =
+>     let repl ' ' = "_"
+>         repl '_' = "__"
+>         repl x = [x]
+>     in lexeme $ do
+>     s <- (char '\'' *> manyTill anyChar (char '\''))
+>     return (concatMap repl s)
 
 > dot :: Parser Char
 > dot = lexeme $ char '.'
@@ -795,6 +801,7 @@ In this pass, we collect all string literals, and make constant declarations for
 > eq = lexeme $ char '='
 
 > gt :: Parser Char
+> 
 > gt = lexeme $ char '>'
 
 > lt :: Parser Char

examples/inequal_queries/string_ex1.cos

@@ -0,0 +1,11 @@
+schema s1(x:int, ya:int, yx:string);
+
+table a(s1);            -- define table a using schema s1
+
+query q1                -- define query q1 on tables a and b
+`select x.x as ax from a x where x.yx = 'hello'`;
+
+query q2                -- define query q2 likewise
+`select x.x as ax from a x where x.yx = 'hello hi'`;
+
+verify q1 q2;           -- does q1 equal to q2?

solver_test.py

@@ -152,6 +152,11 @@ def test_union_empty(self):
         """ test union empty, for now at least it should not be NEQ, wait Coq part to return EQ """
         self.assertNotEqual(
             get_status("./examples/sqlrewrites/unionEmpty.cos"), 'NEQ', "union_empty")
+
+    def test_string_with_space(self):
+        """ test string with space"""
+        self.assertEqual(
+            get_status("./examples/inequal_queries/string_ex1.cos"), 'NEQ', "string_ex1")
 
 if __name__ == '__main__':
     unittest.main()

uexp/src/uexp/congruence.lean

@@ -2,17 +2,110 @@ import .u_semiring
 
 open tactic
 
+private meta def walk_product : expr → tactic unit
+| `(%%a * %%b) := walk_product a >> walk_product b
+| `(%%t₁ ≃ %%t₂) :=
+  if t₁ > t₂
+    then return ()
+    else do h ← to_expr ``(eq_symm %%t₁ %%t₂),
+            try $ rewrite_target h,
+            tactic.trace $ "rewriting " ++ h.to_string,
+            return ()
+| _ := return ()
+
+-- walk the product and normalize equal pred
+meta def unify_eq : tactic unit := do
+  t ← tactic.target,
+  match t with
+  | `(%%a = %%b) := walk_product a >> walk_product b
+  | _ := failed
+  end
+
+meta def split_mult : expr → tactic (list expr)
+| `(eq %%a _) := split_mult a 
+| `(%%a * %%b) := 
+    do lhs ← split_mult a,
+       rhs ← split_mult b,
+       return (lhs ++ rhs)
+| e := match e with
+        | `(%%a ≃ %%b) := (fun x y, x :: y ::[]) 
+                        <$> to_expr ``(%%a ≃ %%b) 
+                        <*> to_expr ``(%%b ≃ %%a)
+        | _            := return []
+       end 
+
+meta def eq_exist : expr →  list expr → bool :=
+(λ e l, 
+match l with
+| [] := ff
+| (h :: t) := if h=e then tt else (eq_exist e t)
+end)
+
+meta def test_split_mul :=
+    do tgt ← tactic.target,
+       rs ← split_mult tgt,
+       tactic.trace rs,
+       return () 
+
+meta def trans_step :=
+    do t ← tactic.target,
+       rs ← split_mult t,
+       match t with 
+        | `(%%a * %%b) := if (eq_exist a rs) then applyc `eq_trans else return ()
+        | _ := return ()
+       end
+
+-- set_option pp. false
 -- set_option trace.simplify true
+section
+variables {s: Schema} {t₁ t₂ t₃: Tuple s} {a b c d: usr} 
+private meta def simp_solve :=
+    `[intros, simp, assumption <|> ac_refl ]
 
-lemma congr_ex1 {s: Schema} (a b c d: Tuple s):
-    (d ≃ c) * (d ≃ d) * (d ≃ a) * (d ≃ b) = (a ≃ b) * (b ≃ c) * (c ≃ d) :=
+lemma prod_unit_p1: c = d → 1 * c = d := by simp_solve
+
+lemma plus_assoc_p1: a * (b * c) = d → (a * b) * c = d := by simp_solve
+
+lemma prod_assoc_p2: 
+b * (a * c) = d → (a * b) * c = d := 
 begin
-    simp,
-    sorry
+    intros,
+    rw ← a_1,
+    ac_refl
 end
 
-meta def ueq_solve :=
-    ac_refl
+lemma plus_comm_p : a * b = c → b * a = c := by simp_solve
+
+lemma plus_unit_c : a = b → a = 1 * b := by simp_solve
 
-meta def ueq_congr :=
-    applyc `eq_unit >> ueq_solve
+lemma plus_assoc_c1 : d = a * (b * c) → (a * b) * c = d := 
+begin
+    intros,
+    rw a_1,
+    ac_refl,
+end
+
+lemma plus_assoc_c2 : d = b * (a * c) → (a * b) * c = d :=
+begin
+    intros,
+    rw a_1,
+    ac_refl,
+end    
+
+lemma plus_comm_c : c = a * b → c = b * a := by simp_solve
+
+lemma plus_cancel : 
+(t₁ ≃ t₂) * ((t₂ ≃ t₃) * c) = d  := 
+begin
+    intros,
+    rw a_1,
+    rw a_2,
+end
+end
+
+lemma congr_ex1 {s: Schema} (a b c d: Tuple s):
+     (a ≃ b) * (b ≃ c) * (a ≃ c) = (a ≃ c) * (b ≃ c)   :=
+begin
+    unify_eq,
+    sorry
+end

uexp/src/uexp/u_semiring.lean

@@ -117,8 +117,8 @@ end
     (t₁ ≃ t₂) = (t₂ ≃ t₁)
 axiom eq_pair {s₁ s₂: Schema} (t₁: Tuple s₁) (t₂: Tuple s₂) (t: Tuple (s₁ ++ s₂)): 
     (t ≃ (t₁, t₂)) = (t₁ ≃ t.1) * (t₂ ≃ t.2)
-@[simp] axiom eq_trans {s: Schema} (t₁ t₂ t₃ : Tuple s):
-    (t₁ ≃ t₂) * (t₂ ≃ t₃) * (t₁ ≃ t₃) = (t₁ ≃ t₂) * (t₂ ≃ t₃)
+axiom eq_trans {s: Schema} (t₁ t₂ t₃ : Tuple s):
+    (t₁ ≃ t₂) * (t₂ ≃ t₃) = (t₁ ≃ t₂) * (t₂ ≃ t₃) * (t₁ ≃ t₃) 
 -- TODO: the following could be a lemma
 @[simp] axiom eq_cancel {s: Schema} (t₁ t₂ : Tuple s):
     (t₁ ≃ t₂) * (t₁ ≃ t₂) = (t₁ ≃ t₂)

uexp/tactic_paper_supplemental_material/monoid_cancellation/cancellation_solver.lean

@@ -45,3 +45,14 @@ repeat $ reflexivity <|> cancel
 
 meta def solve_single :=
 reflexivity <|> cancel
+
+lemma monoid_ex1 (a b c d: m):
+    (a * b * c) * c = c * (b * c) * a :=
+begin
+    applyc `plus_assoc_p1,
+    applyc `plus_assoc_p1,
+    applyc `plus_comm_p,
+    applyc `plus_assoc_c1,
+    applyc `plus_assoc_c1,
+    sorry
+end