coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jonathan Leivent <jonikelee AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] multiple typeclass instance question
- Date: Wed, 9 Mar 2016 22:37:30 -0500
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qg0-f47.google.com
- Ironport-phdr: 9a23:pafGdxQZqXbTAIFbqA0Uu+8FEdpsv+yvbD5Q0YIujvd0So/mwa64Zx2N2/xhgRfzUJnB7Loc0qyN4/+mCTNLv8vJmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbvipNuDPE4W2XKUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGfayQ6NtRrtBST8iLmod5cvxtBCFQxHcyGEbVzA0lRxBHwjM6lneU5bvvy3m/r5/3y+bPsDyQL0cVjGr7qMtQxjt3nRUfwUl+X3a35QjxJlQpwis8kRy
On 03/09/2016 10:11 PM, Jason Gross wrote:
Axiom A : Type.
Existing Class A.
Axioms a a' : A.
Existing Instances a a'.
Class MultiA (n : nat) {x : A} := dummy : list A.
Hint Extern 0 (@MultiA 0 ?x) => (exact nil) : typeclass_instances.
Hint Extern 0 (@MultiA (S ?n) ?x) => (let prev := constr:(_ : @MultiA n _)
in
match eval cbv beta in prev with
| context[cons x _] => fail 1
| ?prev' => exact (cons x prev')
end) : typeclass_instances.
Goal True.
pose (_ : MultiA 2). (* m := ((a :: a' :: nil)%list : MultiA 2) : MultiA
2 *)
There's probably a way to do this without giving the length of the list
ahead of time, but I hope this gives a bit of insight into the model I'm
using of typeclass resolution hackery.
OK - I think I get it. So, the backtracking must occur entirely within the extern hints? The list is then needed to accumulate the results seen during backtracking. It's unfortunate that the context search is needed each time. This must get really slow when the number of A's gets large.
I think the length of the list could be eliminated by having a dedicated first (or highest cost) instance of A that the second hint uses to know to stop looking for more.
Thanks, Jason! Now I have to see if I can repackage this to use...
-- Jonathan
- [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/09/2016
- Re: [Coq-Club] multiple typeclass instance question, Vadim Zaliva, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Matthieu Sozeau, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Jason Gross, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Jason Gross, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Jason Gross, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Jason Gross, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Matthieu Sozeau, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/10/2016
- Re: [Coq-Club] multiple typeclass instance question, Arnaud Spiwack, 03/11/2016
- Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/11/2016
- Re: [Coq-Club] multiple typeclass instance question, Pierre-Marie Pédrot, 03/12/2016
- Re: [Coq-Club] multiple typeclass instance question, Arnaud Spiwack, 03/13/2016
- Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/13/2016
- Re: [Coq-Club] multiple typeclass instance question, Arnaud Spiwack, 03/15/2016
- Re: [Coq-Club] multiple typeclass instance question, Matthieu Sozeau, 03/15/2016
- Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/15/2016
- Re: [Coq-Club] multiple typeclass instance question, Arnaud Spiwack, 03/13/2016
- Re: [Coq-Club] multiple typeclass instance question, Vadim Zaliva, 03/10/2016
Archive powered by MHonArc 2.6.18.