test(library/simplifier): add test for the single_pass option in the simplifier

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

tests/lean/simp12.lean

@@ -0,0 +1,18 @@
+variables a b c d e f : Nat
+rewrite_set simple
+add_rewrite Nat::add_assoc Nat::add_comm Nat::add_left_comm Nat::distributer Nat::distributel : simple
+(*
+local opts   = options({"simplifier", "single_pass"}, true)
+local t      = parse_lean("f + (c + f + d) + (e * (a + c) + (d + a))")
+print(t)
+for i = 1, 10 do
+  local t2, pr = simplify(t, "simple", get_environment(), context(), opts)
+  print("i: " .. i .. " ====>")
+  print(t2)
+  if t == t2 then
+    break
+  end
+  t = t2
+end
+*)
+

tests/lean/simp12.lean.expected.out

@@ -0,0 +1,21 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: a
+  Assumed: b
+  Assumed: c
+  Assumed: d
+  Assumed: e
+  Assumed: f
+f + (c + f + d) + (e * (a + c) + (d + a))
+i: 1 ====>
+d + (f + (c + f) + (a + d + (e * a + e * c)))
+i: 2 ====>
+a + (d + (c + (f + f) + (d + (e * a + e * c))))
+i: 3 ====>
+a + (d + (d + (c + (f + f) + (e * a + e * c))))
+i: 4 ====>
+a + (c + (d + (d + (f + f + (e * a + e * c)))))
+i: 5 ====>
+a + (c + (d + (d + (f + (f + (e * a + e * c))))))
+i: 6 ====>
+a + (c + (d + (d + (f + (f + (e * a + e * c))))))