From 7cf8be66f4215dabb1c072c589299283e4134d4c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 20 Aug 2016 16:52:12 +0200
Subject: Trying a no-inversion no-dependency heuristic for match return
 clause.

The no-inversion no-dependency heuristic was used only in the absence
of type constraint. We may now use it also in the presence of a type
constraint.

See previous commit for discussion.
---
 test-suite/success/Case13.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

(limited to 'test-suite/success')

diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v
index 8f95484cfd..e388acdcb0 100644
--- a/test-suite/success/Case13.v
+++ b/test-suite/success/Case13.v
@@ -87,3 +87,17 @@ Check fun (x : E) => match x with c => e c end.
 Inductive C' : bool -> Set := c' : C' true.
 Inductive E' (b : bool) : Set := e' :> C' b -> E' b.
 Check fun (x : E' true) => match x with c' => e' true c' end.
+
+(* Check use of the no-dependency strategy when a type constraint is
+   given (and when the "inversion-and-dependencies-as-evars" strategy
+   is not strong enough because of a constructor with a type whose
+   pattern structure is not refined enough for it to be captured by
+   the inversion predicate) *)
+
+Inductive K : bool -> bool -> Type := F : K true true | G x : K x x.
+
+Check fun z P Q (y:K true z) (H1 H2:P y) (f:forall y, P y -> Q y z) =>
+        match y with
+        | F  => f y H1
+        | G _ => f y H2
+        end : Q y z.
-- 
cgit v1.2.3


From 29f749d87aebb8226bb9da624c57f83942881a99 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 20 Aug 2016 17:13:58 +0200
Subject: Trying an abstracting dependencies heuristic for the match return
 clause even when no type constraint is given.

This no-inversion and maximal abstraction over dependencies in (rel)
variables heuristic was used only when a type constraint was given.

By doing so, we ensure that all three strategies "inversion with
dependencies as evars", "no-inversion and maximal abstraction over
dependencies in (rel) variables", "no-inversion and no abstraction
over dependencies" are tried in all situations where a return clause
has to be inferred.

See penultimate commit for discussion.
---
 test-suite/success/Case13.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'test-suite/success')

diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v
index e388acdcb0..8fad41cd8f 100644
--- a/test-suite/success/Case13.v
+++ b/test-suite/success/Case13.v
@@ -101,3 +101,15 @@ Check fun z P Q (y:K true z) (H1 H2:P y) (f:forall y, P y -> Q y z) =>
         | F  => f y H1
         | G _ => f y H2
         end : Q y z.
+
+(* Check use of the maximal-dependency-in-variable strategy even when
+   no explicit type constraint is given (and when the
+   "inversion-and-dependencies-as-evars" strategy is not strong enough
+   because of a constructor with a type whose pattern structure is not
+   refined enough for it to be captured by the inversion predicate) *)
+
+Check fun z P Q (y:K true z) (H1 H2:P y) (f:forall y z, P y -> Q y z) =>
+        match y with
+        | F  => f y true H1
+        | G b => f y b H2
+        end.
-- 
cgit v1.2.3


From b2361208a1242a92af7d18cb723ef3b7b55d79b5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 20 Aug 2016 17:29:26 +0200
Subject: Possible abstractions over goal variables when inferring match return
 clause.

The no-inversion and maximal abstraction over dependencies now
supports abstraction over goal variables rather than only on "rel"
variables. In particular, it now works consistently using
"intro H; refine (match H with ... end)" or
"refine (fun H => match H with ... end)".

By doing so, we ensure that all three strategies are tried in all
situations where a return clause has to be inferred, even in the
context of a "refine".

See antepenultimate commit for discussion.
---
 test-suite/success/Case13.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'test-suite/success')

diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v
index 8fad41cd8f..356a67efec 100644
--- a/test-suite/success/Case13.v
+++ b/test-suite/success/Case13.v
@@ -113,3 +113,15 @@ Check fun z P Q (y:K true z) (H1 H2:P y) (f:forall y z, P y -> Q y z) =>
         | F  => f y true H1
         | G b => f y b H2
         end.
+
+(* Check use of the maximal-dependency-in-variable strategy for "Var"
+   variables *)
+
+Goal forall z P Q (y:K true z) (H1 H2:P y) (f:forall y z, P y -> Q y z), Q y z.
+intros z P Q y H1 H2 f.
+Show.
+refine (match y with
+        | F  => f y true H1
+        | G b => f y b H2
+        end).
+Qed.
-- 
cgit v1.2.3