I am trying to use Elpi's OCaml API to implement typeclass resolution in EasyCrypt.
I have defined a type :
type typ = | Ty of string | App of typ * typ
And a corresponding conversion
typ_conversion of type
I would like to use the
Elpi__API.Data.term corresponding to
Ty "int" to build a
Elpi__API.Data.term that I will turn into a program using
I seem to understand that
typ_conversion.embed is what I am looking for.
However it's type is:
typ Elpi__API.Conversion.embedding = depth:int -> Elpi__API.Data.state -> 'a -> Elpi__API.Data.state * Elpi__API.Data.term * Elpi__API.Conversion.extra_ocaml
And the API does not seem to provide any way to create anything of type
Am I supposed to use something outside of the API.mli file or did I miss something in the API?
Thank you in advance for any help you can provide!
Hi! I don't have that API because, so far it was not really needed. A state is initialized at compilation time, then skimmed down an threaded at runtime. If you implement a builtin, the code which runs at runtime will get a state.
In your case I think that the best option is to use https://github.com/LPCIC/elpi/blob/master/src/API.mli#L994 where the program is the "static" set of rules, and the query is something like
[clause1 , clause2 , clause3] => real_query.
Then, to avoid to recompile the clauses at each query invocation, we can add an API that lets you do what you want.
If you want we can look at the code next week together (next week).
In any case the API I could add would take in input something like
(depth:int -> State.t -> State.t * Data.term) and call it with the right compilation state in order to get the new clause. So it would be really similar.
[ , ] is really
Thank you, I'll test it that way!
Last updated: Feb 05 2023 at 14:02 UTC