Stream: Elpi users & devs

Topic: Accumulate to a database during execution


view this post on Zulip Enzo Crance (Sep 01 2022 at 12:55):

Hello.

I want to add a clause to a database in my program, knowing that the program might query the database for this specific clause later. As documented, coq.elpi.accumulate only adds the clause after executing the program, so the program does not find the expected value in the database.

What are my options? Should I write external predicates in ML to store these terms in an OCaml hash table, or is there an idiomatic solution in Elpi? Thanks.

view this post on Zulip Enrico Tassi (Sep 01 2022 at 14:12):

Yes, you can use implication. I mean C = predicate arguments, coq.elpi.accumulate .. C, C => code

view this post on Zulip Enrico Tassi (Sep 01 2022 at 14:12):

See the main loop in derive.elpi, I do it like that


Last updated: Feb 05 2023 at 14:02 UTC