From 70c1dfc6ccc08309459b42046b75157ae784f670 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 25 Jun 2018 14:11:03 +0200
Subject: [PATCH] begin a test suite

---
 Makefile.coq.local     | 32 ++++++++++++++++++++++++++++++++
 tests/solve_proper.ref |  0
 tests/solve_proper.v   | 24 ++++++++++++++++++++++++
 tests/typeclasses.ref  |  0
 tests/typeclasses.v    | 17 +++++++++++++++++
 5 files changed, 73 insertions(+)
 create mode 100644 Makefile.coq.local
 create mode 100644 tests/solve_proper.ref
 create mode 100644 tests/solve_proper.v
 create mode 100644 tests/typeclasses.ref
 create mode 100644 tests/typeclasses.v

diff --git a/Makefile.coq.local b/Makefile.coq.local
new file mode 100644
index 00000000..0937c4a9
--- /dev/null
+++ b/Makefile.coq.local
@@ -0,0 +1,32 @@
+# run tests with main build
+real-all: test
+
+# the test suite
+TESTFILES=$(wildcard tests/*.v)
+
+test: $(TESTFILES:.v=.vo)
+.PHONY: test
+
+COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
+
+# Can't use pipes because that discards error codes and dash provides no way to control that.
+# Also egrep errors if it doesn't match anything, we have to ignore that.
+# Oh Unix...
+REF_FILTER=egrep -v '(^Welcome to Coq|^Skipping rcfile loading.$$)'
+
+tests/.coqdeps.d: $(TESTFILES)
+	$(SHOW)'COQDEP TESTFILES'
+	$(HIDE)$(COQDEP) -dyndep var $(COQMF_COQLIBS_NOML) $^ $(redir_if_ok)
+-include tests/.coqdeps.d
+
+$(TESTFILES:.v=.vo): %.vo: %.v $(if $(MAKE_REF),,%.ref)
+	$(SHOW)$(if $(MAKE_REF),COQTEST [ref],COQTEST) $<
+	$(HIDE)TEST="$$(basename -s .v $<)" && \
+	  TMPFILE="$$(mktemp)" && \
+	  $(TIMER) $(COQ_TEST) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) -load-vernac-source $< $(TIMING_EXTRA) > "$$TMPFILE" && \
+	  ($(REF_FILTER) < "$$TMPFILE" > "$$TMPFILE.filtered" || true) && \
+	  $(if $(MAKE_REF), \
+	    mv "$$TMPFILE.filtered" "tests/$$TEST.ref", \
+	    diff -u "tests/$$TEST.ref" "$$TMPFILE.filtered") && \
+	  rm -f "$$TMPFILE" "$$TMPFILE.filtered" && \
+	  touch $@
diff --git a/tests/solve_proper.ref b/tests/solve_proper.ref
new file mode 100644
index 00000000..e69de29b
diff --git a/tests/solve_proper.v b/tests/solve_proper.v
new file mode 100644
index 00000000..1f44e13d
--- /dev/null
+++ b/tests/solve_proper.v
@@ -0,0 +1,24 @@
+From stdpp Require Import prelude.
+
+(** Some tests for solve_proper. *)
+Section tests.
+  Context {A B : Type} `{!Equiv A, !Equiv B}.
+  Context (foo : A → A) (bar : A → B) (baz : B → A → A).
+  Context `{!Proper ((≡) ==> (≡)) foo,
+            !Proper ((≡) ==> (≡)) bar,
+            !Proper ((≡) ==> (≡) ==> (≡)) baz}.
+
+  Definition test1 (x : A) := baz (bar (foo x)) x.
+  Global Instance : Proper ((≡) ==> (≡)) test1.
+  Proof. solve_proper. Qed.
+
+  Definition test2 (b : bool) (x : A) :=
+    if b then bar (foo x) else bar x.
+  Global Instance : ∀ b, Proper ((≡) ==> (≡)) (test2 b).
+  Proof. solve_proper. Qed.
+
+  Definition test3 (f : nat → A) :=
+    baz (bar (f 0)) (f 2).
+  Global Instance : Proper (pointwise_relation nat (≡) ==> (≡)) test3.
+  Proof. solve_proper. Qed.
+End tests.
diff --git a/tests/typeclasses.ref b/tests/typeclasses.ref
new file mode 100644
index 00000000..e69de29b
diff --git a/tests/typeclasses.v b/tests/typeclasses.v
new file mode 100644
index 00000000..6e31f529
--- /dev/null
+++ b/tests/typeclasses.v
@@ -0,0 +1,17 @@
+From stdpp Require Import prelude.
+
+(** Check that [@Reflexive Prop ?r] picks the instance setoid_rewrite needs.
+    Really, we want to set [Hint Mode Reflexive] in a way that this fails, but
+    we cannot [1].  So at least we try to make sure the first solution found
+    is the right one, to not pay performance in the success case [2].
+
+    [1] https://github.com/coq/coq/issues/7916
+    [2] https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/merge_requests/38
+*)
+Lemma test_setoid_rewrite :
+  exists R, @Reflexive Prop R /\ R = iff.
+Proof.
+  eexists. split.
+  - apply _.
+  - reflexivity.
+Qed.
-- 
GitLab