From d912c9cd09c3c9079a121dcd23bf5d25056d4300 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 9 Sep 2013 09:19:49 -0700
Subject: [PATCH] Add more 'bad' examples

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 tests/lean/bad/t4.lean | 16 ++++++++++++++++
 tests/lean/bad/t6.lean | 23 +++++++++++++++++++++++
 tests/lean/bad/t7.lean | 27 +++++++++++++++++++++++++++
 3 files changed, 66 insertions(+)
 create mode 100644 tests/lean/bad/t4.lean
 create mode 100644 tests/lean/bad/t6.lean
 create mode 100644 tests/lean/bad/t7.lean

diff --git a/tests/lean/bad/t4.lean b/tests/lean/bad/t4.lean
new file mode 100644
index 0000000000..b6eebaf27c
--- /dev/null
+++ b/tests/lean/bad/t4.lean
@@ -0,0 +1,16 @@
+Variable f {A : Type} (a : A) : A
+Variable a : Int
+Definition tst : Bool := (fun x, (f x) > 10) a
+(*
+The definition above should create the following problem for the new elaborator engine:
+
+Definition tst : Int := (fun x : _, ((choice Nat::lt Int::lt Real::lt) (f _ x) ((choice id nat_to_int real_to_int) 10))) a
+
+The first choice is generated because > is an overloaded notation.
+
+The second choice is generated because we have coercions from nat->int
+and nat->real, and it is unclear which one we need until we select the overload.
+*)
+
+(* Workaround: again add coercion manually *)
+Definition tst : Bool := (fun x, (f x) > (nat_to_int 10)) a
diff --git a/tests/lean/bad/t6.lean b/tests/lean/bad/t6.lean
new file mode 100644
index 0000000000..42efd01bff
--- /dev/null
+++ b/tests/lean/bad/t6.lean
@@ -0,0 +1,23 @@
+Variable f {A : Type} (a : A) : A
+Variable a : Int
+Variable b : Real
+Definition tst : Bool := (fun x y, (f x) > (f y)) a b
+(*
+In the current version, the example above does not work without user's help.
+We can compile this example into the following elaborator problem:
+
+Definition tst : Bool := (fun (x : _) (y : _),
+                           ((choice Nat::lt Int::lt Real::lt)
+                            ((choice id nat_to_int nat_to_real int_to_real) (f _ x))
+                            ((choice id nat_to_int nat_to_real int_to_real) (f _ y))))
+                         a b
+
+The first choice construct is generated because > is overloaded notation.
+
+The second and third choices are selected because Nat::lt, Int::lt and
+Real::lt expect Nat, Int and Real arguments respectively.
+The type of the expressions (f _ x) and (f _ y) is unknown at problem generation time.
+So, we create a choice with all relevant coercions. The choice `id` represents "no coercion" is
+needed.
+*)
+Definition tst : Bool := (fun x y, (int_to_real (f x)) > (f y)) a b
diff --git a/tests/lean/bad/t7.lean b/tests/lean/bad/t7.lean
new file mode 100644
index 0000000000..a5e4369e2b
--- /dev/null
+++ b/tests/lean/bad/t7.lean
@@ -0,0 +1,27 @@
+Variable f {A : Type} (a b : A) : Bool
+Variable a : Int
+Variable b : Real
+Definition tst : Bool := (fun x y, f x y) a b
+(*
+The example above demonstrates that may not be easy to eagerly create
+choice constructs that cover all needed coercions.
+
+The variables `a` and `b` have type Int and Real respectively.
+Since the type of the function is not known at compilation time, we
+add choice constructs that accomodate possible coercions.
+So, we get the problem:
+
+Definition tst : Bool := (fun (x : _) (y : _), f _ x y)
+                         ((choice id int_to_real a))
+                         b
+*)
+Definition tst1 : Bool := (fun x y, f x y) (int_to_real a) b
+Set pp::coercion true
+Set pp::implicit true
+Show Environment 1
+(*
+It is unclear how to implement a simple elaboration problem generator that will produce
+a problem that has the following solution.
+*)
+Definition tst2 : Bool := (fun x y, f (int_to_real x) y) a b
+Show Environment 1