From 8463f0a3f34aa1ca314bde1f3d19a3895df9dcaa Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 24 Sep 2016 17:48:28 +0200
Subject: Adding a test for bug #5096.

---
 test-suite/bugs/closed/5096.v | 219 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 219 insertions(+)
 create mode 100644 test-suite/bugs/closed/5096.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5096.v b/test-suite/bugs/closed/5096.v
new file mode 100644
index 0000000000..20a537ab3c
--- /dev/null
+++ b/test-suite/bugs/closed/5096.v
@@ -0,0 +1,219 @@
+Require Import Coq.FSets.FMapPositive Coq.PArith.BinPos Coq.Lists.List.
+
+Set Asymmetric Patterns.
+
+Notation eta x := (fst x, snd x).
+
+Inductive expr {var : Type} : Type :=
+| Const : expr
+| LetIn : expr -> (var -> expr) -> expr.
+
+Definition Expr := forall var, @expr var.
+
+Fixpoint count_binders (e : @expr unit) : nat :=
+match e with
+| LetIn _ eC => 1 + @count_binders (eC tt)
+| _ => 0
+end.
+
+Definition CountBinders (e : Expr) : nat := count_binders (e _).
+
+Class Context (Name : Type) (var : Type) :=
+  { ContextT : Type;
+    extendb : ContextT -> Name -> var -> ContextT;
+    empty : ContextT }.
+Coercion ContextT : Context >-> Sortclass.
+Arguments ContextT {_ _ _}, {_ _} _.
+Arguments extendb {_ _ _} _ _ _.
+Arguments empty {_ _ _}.
+
+Module Export Named.
+Inductive expr Name : Type :=
+| Const : expr Name
+| LetIn : Name -> expr Name -> expr Name -> expr Name.
+End Named.
+
+Global Arguments Const {_}.
+Global Arguments LetIn {_} _ _ _.
+
+Definition split_onames {Name : Type} (ls : list (option Name))
+  : option (Name) * list (option Name)
+  := match ls with
+          | cons n ls'
+            => (n, ls')
+          | nil => (None, nil)
+     end.
+
+Section internal.
+  Context (InName OutName : Type)
+          {InContext : Context InName (OutName)}
+          {ReverseContext : Context OutName (InName)}
+          (InName_beq : InName -> InName -> bool).
+
+  Fixpoint register_reassign (ctxi : InContext) (ctxr : ReverseContext)
+           (e : expr InName) (new_names : list (option OutName))
+    : option (expr OutName)
+    := match e in Named.expr _ return option (expr _) with
+       | Const => Some Const
+       | LetIn n ex eC
+         => let '(n', new_names') := eta (split_onames new_names) in
+            match n', @register_reassign ctxi ctxr ex nil with
+            | Some n', Some x
+              => let ctxi := @extendb _ _ _ ctxi n n' in
+                 let ctxr := @extendb _ _ _ ctxr n' n in
+                 option_map (LetIn n' x) (@register_reassign ctxi ctxr eC new_names')
+            | None, Some x
+              => let ctxi := ctxi in
+                 @register_reassign ctxi ctxr eC new_names'
+            | _, None => None
+            end
+       end.
+
+End internal.
+
+Global Instance pos_context (var : Type) : Context positive var
+  := { ContextT := PositiveMap.t var;
+       extendb ctx key v := PositiveMap.add key v ctx;
+       empty := PositiveMap.empty _ }.
+
+Global Arguments register_reassign {_ _ _ _} ctxi ctxr e _.
+
+Section language5.
+  Context (Name : Type).
+
+  Local Notation expr := (@Top.expr Name).
+  Local Notation nexpr := (@Named.expr Name).
+
+  Fixpoint ocompile (e : expr) (ls : list (option Name)) {struct e}
+    : option (nexpr)
+    := match e in @Top.expr _ return option (nexpr) with
+       | Top.Const => Some Named.Const
+       | Top.LetIn ex eC
+         => match @ocompile ex nil, split_onames ls with
+            | Some x, (Some n, ls')%core
+              => option_map (fun C => Named.LetIn n x C) (@ocompile (eC n) ls')
+            | _, _ => None
+            end
+       end.
+
+  Definition compile (e : expr) (ls : list Name) := @ocompile e (List.map (@Some _) ls).
+End language5.
+
+Global Arguments compile {_} e ls.
+
+Fixpoint merge_liveness (ls1 ls2 : list unit) :=
+  match ls1, ls2 with
+  | cons x xs, cons y ys => cons tt (@merge_liveness xs ys)
+  | nil, ls | ls, nil => ls
+  end.
+
+Section internal1.
+  Context (Name : Type)
+          (OutName : Type)
+          {Context : Context Name (list unit)}.
+
+  Definition compute_livenessf_step
+             (compute_livenessf : forall (ctx : Context) (e : expr Name) (prefix : list unit), list unit)
+             (ctx : Context)
+             (e : expr Name) (prefix : list unit)
+    : list unit
+    := match e with
+       | Const => prefix
+       | LetIn n ex eC
+         => let lx := @compute_livenessf ctx ex prefix in
+            let lx := merge_liveness lx (prefix ++ repeat tt 1) in
+            let ctx := @extendb _ _ _ ctx n (lx) in
+            @compute_livenessf ctx eC (prefix ++ repeat tt 1)
+       end.
+
+  Fixpoint compute_liveness ctx e prefix
+    := @compute_livenessf_step (@compute_liveness) ctx e prefix.
+
+  Fixpoint insert_dead_names_gen def (ls : list unit) (lsn : list OutName)
+    : list (option OutName)
+    := match ls with
+       | nil => nil
+       | cons live xs
+         => match lsn with
+            | cons n lsn' => Some n :: @insert_dead_names_gen def xs lsn'
+            | nil => def :: @insert_dead_names_gen def xs nil
+            end
+       end.
+  Definition insert_dead_names def (e : expr Name)
+    := insert_dead_names_gen def (compute_liveness empty e nil).
+End internal1.
+
+Global Arguments insert_dead_names {_ _ _} def e lsn.
+
+Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x := let y := x in f y.
+
+Section language7.
+  Context {Context : Context unit (positive)}.
+
+  Local Notation nexpr := (@Named.expr unit).
+
+  Definition CompileAndEliminateDeadCode (e : Expr) (ls : list unit)
+    : option (nexpr)
+    := let e := compile (Name:=positive) (e _) (List.map Pos.of_nat (seq 1 (CountBinders e))) in
+       match e with
+       | Some e => Let_In (insert_dead_names None e ls) (* help vm_compute by factoring this out *)
+                          (fun names => register_reassign empty empty e names)
+       | None => None
+       end.
+End language7.
+
+Global Arguments CompileAndEliminateDeadCode {_} e ls.
+
+Definition ContextOn {Name1 Name2} f {var} (Ctx : Context Name1 var) : Context Name2 var
+  := {| ContextT := Ctx;
+        extendb ctx n v := extendb ctx (f n) v;
+        empty := empty |}.
+
+Definition Register := Datatypes.unit.
+
+Global Instance RegisterContext {var : Type} : Context Register var
+  := ContextOn (fun _ => 1%positive) (pos_context var).
+
+Definition syntax := Named.expr Register.
+
+Definition AssembleSyntax e ls (res := CompileAndEliminateDeadCode e ls)
+  := match res return match res with None => _ | _ => _ end with
+     | Some v => v
+     | None => I
+     end.
+
+Definition dummy_registers (n : nat) : list Register
+  := List.map (fun _ => tt) (seq 0 n).
+Definition DefaultRegisters (e : Expr) : list Register
+  := dummy_registers (CountBinders e).
+
+Definition DefaultAssembleSyntax e := @AssembleSyntax e (DefaultRegisters e).
+
+Notation "'slet' x := A 'in' b" := (Top.LetIn A (fun x => b)) (at level 200, b at level 200).
+Notation "#[ var ]#" := (@Top.Const var).
+
+Definition compiled_syntax : Expr := fun (var : Type) =>
+(
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+ @Top.Const var).
+
+Definition v :=
+  Eval cbv [compiled_syntax] in (DefaultAssembleSyntax (compiled_syntax)).
+
+Timeout 2 Eval vm_compute in v.
-- 
cgit v1.2.3


From c8ca50f0cf961c9e31489f095463a99fc005c5de Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 26 Sep 2016 00:06:16 +0200
Subject: Fix bug #5093: typeclasses eauto depth arg does not accept a var.

---
 test-suite/bugs/closed/5093.v | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 test-suite/bugs/closed/5093.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5093.v b/test-suite/bugs/closed/5093.v
new file mode 100644
index 0000000000..3ded4dd304
--- /dev/null
+++ b/test-suite/bugs/closed/5093.v
@@ -0,0 +1,11 @@
+Axiom P : nat -> Prop.
+Axiom PS : forall n, P n -> P (S n).
+Axiom P0 : P 0.
+
+Hint Resolve PS : foobar.
+Hint Resolve P0 : foobar.
+
+Goal P 100.
+Proof.
+Fail typeclasses eauto 100 with foobar.
+typeclasses eauto 101 with foobar.
-- 
cgit v1.2.3


From 2422aeb2b59229891508f35890653a9737988c00 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')

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 292f365185b7acdee79f3ff7b158551c2764c548 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')

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 0658ba7b908dad946200f872f44260d0e4893a94 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 20 Aug 2016 17:29:26 +0200
Subject: Posssible 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')

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


From 7bc04ff2cc9d511c4b8552a3e5f9ad416917fb95 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sat, 11 Jun 2016 17:23:08 -0400
Subject: Fix bug #4785 (use [ ] for vector nil)

Also delimit vector_scope with vector, so that people can write %vector
without having to delimit it themselves.
---
 test-suite/bugs/closed/4785.v | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)
 create mode 100644 test-suite/bugs/closed/4785.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4785.v b/test-suite/bugs/closed/4785.v
new file mode 100644
index 0000000000..b844af68a9
--- /dev/null
+++ b/test-suite/bugs/closed/4785.v
@@ -0,0 +1,26 @@
+Require Import Coq.Lists.List Coq.Vectors.Vector.
+Import ListNotations.
+Check [ ]%list : list _.
+Import VectorNotations ListNotations.
+Delimit Scope vector_scope with vector.
+Check [ ]%vector : Vector.t _ _.
+Check []%vector : Vector.t _ _.
+Check [ ]%list : list _.
+Check []%list : list _.
+
+Inductive mylist A := mynil | mycons (x : A) (xs : mylist A).
+Delimit Scope mylist_scope with mylist.
+Bind Scope mylist_scope with mylist.
+Arguments mynil {_}, _.
+Arguments mycons {_} _ _.
+Notation " [] " := mynil : mylist_scope.
+Notation " [ ] " := mynil (format "[ ]") : mylist_scope.
+Notation " [ x ] " := (mycons x nil) : mylist_scope.
+Notation " [ x ; y ; .. ; z ] " :=  (mycons x (mycons y .. (mycons z nil) ..)) : mylist_scope.
+
+Require Import Coq.Compat.Coq85.
+
+Check []%vector : Vector.t _ _.
+Check []%mylist : mylist _.
+Check [ ]%mylist : mylist _.
+Check [ ]%list : list _.
-- 
cgit v1.2.3


From f8745b1dbc87a8fee4943a91f517dc2afcd7804b Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sat, 11 Jun 2016 18:09:01 -0400
Subject: Unbreak Ltac [ | .. | ] notation in -compat 8.5

Importing VectorNotations breaks `; []`.  So we make sure it's not
imported by defualt.  Some files might be required to `Import
VectorDef.VectorNotations` rather than just `Import VectorNotations`.
---
 test-suite/bugs/closed/4785.v | 23 +++++++++++++++++++++--
 1 file changed, 21 insertions(+), 2 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4785.v b/test-suite/bugs/closed/4785.v
index b844af68a9..14af2d91df 100644
--- a/test-suite/bugs/closed/4785.v
+++ b/test-suite/bugs/closed/4785.v
@@ -1,4 +1,8 @@
-Require Import Coq.Lists.List Coq.Vectors.Vector.
+Require Coq.Lists.List Coq.Vectors.Vector.
+Require Coq.Compat.Coq85.
+
+Module A.
+Import Coq.Lists.List Coq.Vectors.Vector.
 Import ListNotations.
 Check [ ]%list : list _.
 Import VectorNotations ListNotations.
@@ -8,6 +12,10 @@ Check []%vector : Vector.t _ _.
 Check [ ]%list : list _.
 Check []%list : list _.
 
+Goal True.
+  idtac; []. (* Check that vector notations don't break the [ | .. | ] syntax of Ltac *)
+Abort.
+
 Inductive mylist A := mynil | mycons (x : A) (xs : mylist A).
 Delimit Scope mylist_scope with mylist.
 Bind Scope mylist_scope with mylist.
@@ -18,9 +26,20 @@ Notation " [ ] " := mynil (format "[ ]") : mylist_scope.
 Notation " [ x ] " := (mycons x nil) : mylist_scope.
 Notation " [ x ; y ; .. ; z ] " :=  (mycons x (mycons y .. (mycons z nil) ..)) : mylist_scope.
 
-Require Import Coq.Compat.Coq85.
+Import Coq.Compat.Coq85.
+Locate Module VectorNotations.
+Import VectorDef.VectorNotations.
 
 Check []%vector : Vector.t _ _.
 Check []%mylist : mylist _.
 Check [ ]%mylist : mylist _.
 Check [ ]%list : list _.
+End A.
+
+Module B.
+Import Coq.Compat.Coq85.
+
+Goal True.
+  idtac; []. (* Check that importing the compat file doesn't break the [ | .. | ] syntax of Ltac *)
+Abort.
+End B.
-- 
cgit v1.2.3