Stream: Elpi users & devs

Topic: Using Conversion in Elpi's OCaml API


view this post on Zulip Antoine Séré (Nov 05 2021 at 14:41):

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!

view this post on Zulip Enrico Tassi (Nov 05 2021 at 16:02):

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).

view this post on Zulip Enrico Tassi (Nov 05 2021 at 16:07):

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

view this post on Zulip Antoine Séré (Nov 08 2021 at 09:51):

Thank you, I'll test it that way!


Last updated: Feb 05 2023 at 14:02 UTC