diff options
Diffstat (limited to 'test-suite/success/Typeclasses.v')
-rw-r--r-- | test-suite/success/Typeclasses.v | 188 |
1 files changed, 185 insertions, 3 deletions
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index 30a2a742..6b1f0315 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -1,3 +1,117 @@ +Module onlyclasses. + +(* In 8.6 we still allow non-class subgoals *) + Variable Foo : Type. + Variable foo : Foo. + Hint Extern 0 Foo => exact foo : typeclass_instances. + Goal Foo * Foo. + split. shelve. + Set Typeclasses Debug. + typeclasses eauto. + Unshelve. typeclasses eauto. + Qed. + + Module RJung. + Class Foo (x : nat). + + Instance foo x : x = 2 -> Foo x. + Hint Extern 0 (_ = _) => reflexivity : typeclass_instances. + Typeclasses eauto := debug. + Check (_ : Foo 2). + + + Fail Definition foo := (_ : 0 = 0). + + End RJung. +End onlyclasses. + +Module shelve_non_class_subgoals. + Variable Foo : Type. + Variable foo : Foo. + Hint Extern 0 Foo => exact foo : typeclass_instances. + Class Bar := {}. + Instance bar1 (f:Foo) : Bar := {}. + + Typeclasses eauto := debug. + Set Typeclasses Debug Verbosity 2. + Goal Bar. + (* Solution has shelved subgoals (of non typeclass type) *) + typeclasses eauto. + Abort. +End shelve_non_class_subgoals. + +Module RefineVsNoTceauto. + + Class Foo (A : Type) := foo : A. + Instance: Foo nat := { foo := 0 }. + Instance: Foo nat := { foo := 42 }. + Hint Extern 0 (_ = _) => refine eq_refl : typeclass_instances. + Goal exists (f : Foo nat), @foo _ f = 0. + Proof. + unshelve (notypeclasses refine (ex_intro _ _ _)). + Set Typeclasses Debug. Set Printing All. + all:once (typeclasses eauto). + Fail idtac. (* Check no subgoals are left *) + Undo 3. + (** In this case, the (_ = _) subgoal is not considered + by typeclass resolution *) + refine (ex_intro _ _ _). Fail reflexivity. + Abort. + +End RefineVsNoTceauto. + +Module Leivantex2PR339. + (** Was a bug preventing to find hints associated with no pattern *) + Class Bar := {}. + Instance bar1 (t:Type) : Bar. + Hint Extern 0 => exact True : typeclass_instances. + Typeclasses eauto := debug. + Goal Bar. + Set Typeclasses Debug Verbosity 2. + typeclasses eauto. (* Relies on resolution of a non-class subgoal *) + Undo 1. + typeclasses eauto with typeclass_instances. + Qed. +End Leivantex2PR339. + +Module bt. +Require Import Equivalence. + +Record Equ (A : Type) (R : A -> A -> Prop). +Definition equiv {A} R (e : Equ A R) := R. +Record Refl (A : Type) (R : A -> A -> Prop). +Axiom equ_refl : forall A R (e : Equ A R), Refl _ (@equiv A R e). +Hint Extern 0 (Refl _ _) => unshelve class_apply @equ_refl; [shelve|] : foo. + +Variable R : nat -> nat -> Prop. +Lemma bas : Equ nat R. +Admitted. +Hint Resolve bas : foo. +Hint Extern 1 => match goal with |- (_ -> _ -> Prop) => shelve end : foo. + +Goal exists R, @Refl nat R. + eexists. + Set Typeclasses Debug. + (* Fail solve [unshelve eauto with foo]. *) + Set Typeclasses Debug Verbosity 1. + Test Typeclasses Depth. + solve [typeclasses eauto with foo]. +Qed. + +Set Typeclasses Compatibility "8.5". +Parameter f : nat -> Prop. +Parameter g : nat -> nat -> Prop. +Parameter h : nat -> nat -> nat -> Prop. +Axiom a : forall x y, g x y -> f x -> f y. +Axiom b : forall x (y : Empty_set), g (fst (x,y)) x. +Axiom c : forall x y z, h x y z -> f x -> f y. +Hint Resolve a b c : mybase. +Goal forall x y z, h x y z -> f x -> f y. + intros. + Fail Timeout 1 typeclasses eauto with mybase. (* Loops now *) + Unshelve. +Abort. +End bt. Generalizable All Variables. Module mon. @@ -23,8 +137,15 @@ Notation "'return' t" := (unit t). Class A `(e: T) := { a := True }. Class B `(e_: T) := { e := e_; sg_ass :> A e }. -Goal forall `{B T}, a. - intros. exact I. +(* Set Typeclasses Debug. *) +(* Set Typeclasses Debug Verbosity 2. *) + +Goal forall `{B T}, Prop. + intros. apply a. +Defined. + +Goal forall `{B T}, Prop. + intros. refine (@a _ _ _). Defined. Class B' `(e_: T) := { e' := e_; sg_ass' :> A e_ }. @@ -57,4 +178,65 @@ Section sec. let's try to get rid of the intermediate constant foo. Surely we can just expand it inline, right? Wrong!: *) Check U (fun x => e x) _. -End sec.
\ No newline at end of file +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. + Class B. + Class C. + + Instance: B -> A | 0. + Instance: C -> A | 0. + Instance: C -> B -> A | 0. + Instance: A -> A | 0. + + Goal C -> A. + intros. + Set Typeclasses Debug. + Fail Timeout 1 typeclasses eauto. + Set Typeclasses Iterative Deepening. + Fail typeclasses eauto 1. + typeclasses eauto 2. + Undo. + Unset Typeclasses Iterative Deepening. + Fail Timeout 1 typeclasses eauto. + Set Typeclasses Iterative Deepening. + typeclasses eauto. + Qed. + +End IterativeDeepening. |