Hello everyone!
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 typ Elpi__API.Conversion.t
.
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 Elpi__API.Utils.clause_of_term
.
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 Elpi__API.Data.state
.
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.
Here [ , ]
is really mkNil
and mkCons
and =>
is mkGlobal Global_symbols.implc
Thank you, I'll test it that way!
Last updated: Oct 13 2024 at 01:02 UTC