diff options
author | Matthieu Sozeau <mattam@mattam.org> | 2016-10-26 18:34:13 +0200 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2016-11-03 16:26:40 +0100 |
commit | c5802966f23b9a8dc34f55961d4861997a3df01f (patch) | |
tree | 25a5665165bfc0435c680b5d6aff640a14346a69 /test-suite | |
parent | 8aa945902d40765f69cd16ce7647d3c28248eb54 (diff) |
Test new syntax for hints and typeclass options
Diffstat (limited to 'test-suite')
-rw-r--r-- | test-suite/success/Hints.v | 81 | ||||
-rw-r--r-- | test-suite/success/Typeclasses.v | 47 |
2 files changed, 121 insertions, 7 deletions
diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v index 91edc06bf..1abe14774 100644 --- a/test-suite/success/Hints.v +++ b/test-suite/success/Hints.v @@ -1,4 +1,12 @@ (* Checks syntax of Hints commands *) +(* Old-style syntax *) +Hint Resolve eq_refl eq_sym. +Hint Resolve eq_refl eq_sym: foo. +Hint Immediate eq_refl eq_sym. +Hint Immediate eq_refl eq_sym: foo. +Hint Unfold fst eq_sym. +Hint Unfold fst eq_sym: foo. + (* Checks that qualified names are accepted *) (* New-style syntax *) @@ -8,17 +16,76 @@ Hint Unfold eq_sym: core. Hint Constructors eq: foo bar. Hint Extern 3 (_ = _) => apply eq_refl: foo bar. +(* Extended new syntax with patterns *) Hint Resolve eq_refl | 4 (_ = _) : baz. Hint Resolve eq_sym eq_trans : baz. Hint Extern 3 (_ = _) => apply eq_sym : baz. -(* Old-style syntax *) -Hint Resolve eq_refl eq_sym. -Hint Resolve eq_refl eq_sym: foo. -Hint Immediate eq_refl eq_sym. -Hint Immediate eq_refl eq_sym: foo. -Hint Unfold fst eq_sym. -Hint Unfold fst eq_sym: foo. +Parameter pred : nat -> Prop. +Parameter pred0 : pred 0. +Parameter f : nat -> nat. +Parameter predf : forall n, pred n -> pred (f n). + +(* No conversion on let-bound variables and constants in pred (the default) *) +Hint Resolve pred0 | 1 (pred _) : pred. +Hint Resolve predf | 0 : pred. + +(* Allow full conversion on let-bound variables and constants *) +Create HintDb predconv discriminated. +Hint Resolve pred0 | 1 (pred _) : predconv. +Hint Resolve predf | 0 : predconv. + +Goal exists n, pred n. + eexists. + Fail Timeout 1 typeclasses eauto with pred. + Set Typeclasses Filtered Unification. + Set Typeclasses Debug Verbosity 2. + (* predf is not tried as it doesn't match the goal *) + typeclasses eauto with pred. +Qed. + +Parameter predconv : forall n, pred n -> pred (0 + S n). + +(* The inferred pattern contains 0 + ?n, syntactic match will fail to see convertible + terms *) +Hint Resolve pred0 : pred2. +Hint Resolve predconv : pred2. + +(** In this database we allow predconv to apply to pred (S _) goals, more generally + than the inferred pattern (pred (0 + S _)). *) +Create HintDb pred2conv discriminated. +Hint Resolve pred0 : pred2conv. +Hint Resolve predconv | 1 (pred (S _)) : pred2conv. + +Goal pred 3. + Fail typeclasses eauto with pred2. + typeclasses eauto with pred2conv. +Abort. + +Set Typeclasses Filtered Unification. +Set Typeclasses Debug Verbosity 2. +Hint Resolve predconv | 1 (pred _) : pred. +Hint Resolve predconv | 1 (pred (S _)) : predconv. +Test Typeclasses Limit Intros. +Goal pred 3. + (* predf is not tried as it doesn't match the goal *) + (* predconv is tried but fails as the transparent state doesn't allow + unfolding + *) + Fail typeclasses eauto with pred. + (* Here predconv succeeds as it matches (pred (S _)) and then + full unification is allowed *) + typeclasses eauto with predconv. +Qed. + +(** The other way around: goal contains redexes instead of instances *) +Goal exists n, pred (0 + n). + eexists. + (* predf is applied indefinitely *) + Fail Timeout 1 typeclasses eauto with pred. + (* pred0 (pred _) matches the goal *) + typeclasses eauto with predconv. +Qed. + (* Checks that local names are accepted *) Section A. diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index 3eaa04144..651bbf7d2 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -1,3 +1,16 @@ +Module onlyclasses. + + Variable Foo : Type. + Variable foo : Foo. + Hint Extern 0 Foo => exact foo : typeclass_instances. + Goal Foo * Foo. + split. shelve. + Fail typeclasses eauto. + typeclasses eauto with typeclass_instances. + Unshelve. typeclasses eauto with typeclass_instances. + Abort. +End onlyclasses. + Module bt. Require Import Equivalence. @@ -104,6 +117,40 @@ Section sec. Check U (fun x => e x) _. End sec. +Module UniqueSolutions. + Set Typeclasses Unique Solutions. + Class Eq (A : Type) : Set. + Instance eqa : Eq nat := {}. + Instance eqb : Eq nat := {}. + + Goal Eq nat. + try apply _. + Fail exactly_once typeclasses eauto. + Abort. +End UniqueSolutions. + + +Module UniqueInstances. + (** Optimize proof search on this class by never backtracking on (closed) goals + for it. *) + Set Typeclasses Unique Instances. + Class Eq (A : Type) : Set. + Instance eqa : Eq nat := _. constructor. Qed. + Instance eqb : Eq nat := {}. + Class Foo (A : Type) (e : Eq A) : Set. + Instance fooa : Foo _ eqa := {}. + + Tactic Notation "refineu" open_constr(c) := unshelve refine c. + + Set Typeclasses Debug. + Goal { e : Eq nat & Foo nat e }. + unshelve refineu (existT _ _ _). + all:simpl. + (** Does not backtrack on the (wrong) solution eqb *) + Fail all:typeclasses eauto. + Abort. +End UniqueInstances. + Module IterativeDeepening. Class A. |