souffle

souffle copied to clipboard

Our project would like to use explain to generate a proof tree for our analysis. It appears that our use of ADTs is blocking us from being able to use explain, as it is unimplemented for ADTs:

https://github.com/souffle-lang/souffle/blob/d70cf1ec0568d7817de5dfecddf555647537ef89/src/ast2ram/provenance/SubproofGenerator.cpp#L238

Would it be possible to implement that branch and have ADT support in explain?

It would not be too hard to implement it. We would need to port part of the I/O system (i.e. type system description etc.).

I would be able to guide you. Would you like to implement it?

Hey @b-scholz, I'm Jay (J for short) and I work with @markww .

I'm having a look into this at the moment (scoping upcoming work in Raksha) and would love to hear from you about approaching this. Would you be able to summarize your thoughts here?

Alternatively, I'm in Sydney and would be able to sync over a video call if that would help :)

@Cypher1 i have sent Mark the first steps - please let me know whether you need more help.

Thank you!