Stream: Hierarchy Builder devs & users

Topic: Adding an elpi clause immediately after predicate definition


view this post on Zulip Quentin VERMANDE (Nov 09 2023 at 15:33):

This is probably an issue with elpi, but there might be a solution within HB. I am trying to modify HB/structure.elpi in order to declare the axioms_ record defined by HB.structure as a class and adding instances of it to tc.db. However, this fails with an allocating new global symbol ... at runtime error. According to [at]Davide F, this fails because the elpi query needs to end before the predicate I am trying to add a clause to is known by elpi. Is it possible to change or work around this behaviour? Otherwise, is there something I can do in HB, while still declaring the class and the clause inside the Exports module defined by HB, so that everything works as intended and without asking too much of the user?

view this post on Zulip Cyril Cohen (Nov 09 2023 at 15:48):

What @Davide F says about adding clauses to a db is true, except it means that the new clause won't be taken into account until the current query ends. The solution to this is to pass around clauses in the current program (e.g. make your program return a CL of type list prop, and use CL => your-program is subsequent calls.
However, this failure "allocating new global symbol ... at runtime", seems to be a quite different problem. Does your current program know the predicate (and its signature) that your are trying to accumulate to the db? i.e. did you accumulate the db file before you make your elpi query?
(@Enrico Tassi did I get this error message right?)

view this post on Zulip Quentin VERMANDE (Nov 09 2023 at 15:54):

I did accumulate the db. I declare the class with coq.TC.declare-class. This leads some code by [at]Davide F to declare the predicate. Then on the next line I do coq.elpi.accumulate, so the predicate should be known at this point.
I am not sure I understand your suggestion, everything happens in the declare predicate of structure.elpi.

view this post on Zulip Enrico Tassi (Nov 09 2023 at 16:25):

This is probably the add-predicate API which is too hackish and has no runtime equivalent yet.


Last updated: Apr 21 2024 at 01:02 UTC