Add builtin to the tc app - #1042
Conversation
| In(Elpi.API.BuiltInData.list Elpi.API.BuiltInData.string, "GR", | ||
| Easy("Declares that goals on GR should be solved using elpi's typeclass solver.")), | ||
| (fun gr ~depth -> | ||
| set_solver_mode AAdd ["TC.Solver"] (List.map Libnames.qualid_of_string gr))), |
There was a problem hiding this comment.
I think that the tc solver should not be hardcoded
|
You should also add the new opam package to the ci job making the release, and add changelog entries |
|
Davide we need a little doc for the filter api, in particular what happens if two tc problems are to be solved and a tc solver only handles one kind. The use case of Quentin is that HB uses a very specific solver for classes it generates. It is really an ad hoc solver to implement some notations without hacking too much. |
|
IIRC when you have a cluster of typeclass goals, the custom solver is used only if it overrides all the class evars in it, otherwise, it uses rocq solver. |
|
cluster means interdependent goals? like |
|
So I think it makes sense for this specific application, all classes are generated by HB, hence solved by the same solver. |
|
|
||
| let tc_builtins = [ | ||
| Elpi.API.BuiltIn.MLCode(Pred("coq.TC.override-solver", | ||
| In(Elpi.API.BuiltInData.string, "GR", |
There was a problem hiding this comment.
| In(Elpi.API.BuiltInData.string, "GR", | |
| In(Elpi.API.BuiltInData.string, "SolverName", |
| let tc_builtins = [ | ||
| Elpi.API.BuiltIn.MLCode(Pred("coq.TC.override-solver", | ||
| In(Elpi.API.BuiltInData.string, "GR", | ||
| In(Elpi.API.BuiltInData.list Elpi.API.BuiltInData.string, "GR", |
There was a problem hiding this comment.
| In(Elpi.API.BuiltInData.list Elpi.API.BuiltInData.string, "GR", | |
| In(Elpi.API.BuiltInData.list Elpi.API.BuiltInData.string, "ClassGR", |
There was a problem hiding this comment.
Or even ClassNames since it is a list of strings.
| Elpi.API.BuiltIn.MLCode(Pred("coq.TC.override-solver", | ||
| In(Elpi.API.BuiltInData.string, "GR", | ||
| In(Elpi.API.BuiltInData.list Elpi.API.BuiltInData.string, "GR", | ||
| Easy("Declares that goals on GR should be solved using elpi's typeclass solver."))), |
There was a problem hiding this comment.
| Easy("Declares that goals on GR should be solved using elpi's typeclass solver."))), | |
| Easy("Declares that instances of class ClassGR should be solved using elpi's typeclass solver SolverName."))), |
There was a problem hiding this comment.
I kept the word goal because of the verb solve.
|
We had a discussion this morning with Yves, is it mandatory to have a doc folder in a plugin? |
| (package | ||
| (name rocq-elpi-typeclasses) | ||
| (synopsis "TC bindings for rocq-elpi") | ||
| (description "This package provides a typeclass solver written in Elpi for Rocq") |
There was a problem hiding this comment.
| (description "This package provides a typeclass solver written in Elpi for Rocq") | |
| (description "This package provides a typeclas solver written in Elpi, as well as the infrastructure for writing custom ones") |
Also in the .opam file
|
|
||
| (package | ||
| (name rocq-elpi-typeclasses) | ||
| (synopsis "TC bindings for rocq-elpi") |
There was a problem hiding this comment.
| (synopsis "TC bindings for rocq-elpi") | |
| (synopsis "Typeclass solver in rocq-elpi") |
Yes, I guess, but by which tool? It should be documented, that is for sure. |
Not sure how it works, but could we label the function declaring builtins with a custom |
3 participants
Dependency of math-comp/hierarchy-builder#596