From ea2a1c974cd2643aba616609a93785797774e0de Mon Sep 17 00:00:00 2001 From: stechu Date: Thu, 12 Apr 2018 16:49:15 -0700 Subject: [PATCH] fix string parsing --- dsl/CosetteParser.lhs | 9 +- examples/inequal_queries/string_ex1.cos | 11 ++ solver_test.py | 5 + uexp/src/uexp/congruence.lean | 109 ++++++++++++++++-- uexp/src/uexp/u_semiring.lean | 4 +- .../cancellation_solver.lean | 11 ++ 6 files changed, 138 insertions(+), 11 deletions(-) create mode 100644 examples/inequal_queries/string_ex1.cos diff --git a/dsl/CosetteParser.lhs b/dsl/CosetteParser.lhs index 7b42bde..e9ea71f 100644 --- a/dsl/CosetteParser.lhs +++ b/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 diff --git a/examples/inequal_queries/string_ex1.cos b/examples/inequal_queries/string_ex1.cos new file mode 100644 index 0000000..d01e14a --- /dev/null +++ b/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? \ No newline at end of file diff --git a/solver_test.py b/solver_test.py index e1aae73..0d9fbf8 100644 --- a/solver_test.py +++ b/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() diff --git a/uexp/src/uexp/congruence.lean b/uexp/src/uexp/congruence.lean index b3153ad..5ea1efe 100644 --- a/uexp/src/uexp/congruence.lean +++ b/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 diff --git a/uexp/src/uexp/u_semiring.lean b/uexp/src/uexp/u_semiring.lean index 2a5f4c8..4eb618d 100644 --- a/uexp/src/uexp/u_semiring.lean +++ b/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₂) diff --git a/uexp/tactic_paper_supplemental_material/monoid_cancellation/cancellation_solver.lean b/uexp/tactic_paper_supplemental_material/monoid_cancellation/cancellation_solver.lean index 2dba20a..312b57c 100644 --- a/uexp/tactic_paper_supplemental_material/monoid_cancellation/cancellation_solver.lean +++ b/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 \ No newline at end of file