CLeanGo: Lean bindings and DSL for Answer Set Programming

Stream: general

[Kiran]

Hi, yall!! I just wanted to share a cool project that I've been working on (I hope this is the right channel to share it, lmk if not).

Anyway, I've implemented some FFI bindings to the Clingo ASP solver (libclingo) (https://potassco.org/). If you're not familiar with it, answer set programming is a particular family of programming languages that are a mix between prolog and datalog that are particularly suited for solving certain scheduling programs (the full description of the differences are out of scope for this post, but if you're interested, do check it out, it's very interesting).

I wanted to share them here if anyone is interested in either trying them out, or looking at them for inspiration. It's available here: https://github.com/kiranandcode/cleango

here's what a program in the DSL looks like:

def main : IO Unit := do

   let control <- Clingo.makeControl

   add_clingo_query! control :

     p(X) :- q(X).
     q(a).
     q(b).


   Clingo.ground control
   Clingo.solve control

   println! "finished!"

image.png

(and the output: )

found model:
 - q(a)
 - q(b)
 - p(a)
 - p(b)
finished!

image.png

A couple of cool things about the DSL:

• firstly, unlike some other Clingo bindings (mostly those written by me in other languages lol), this DSL does not actually convert user input to strings -- I've set up the DSL macros to actually expand to an AST term with locations corresponding to the original syntax in lean (this means that if the solver encounters an error, it will report it in terms of your DSL in lean, which I thought was really cool!!). This AST is then sent to the C FFI and sent directly to the clingo solver.
• The FFI is pretty comprehensive and also contains a collection of functions to translate the lean encoding of the datatypes into the C encoding expected by the FFI.

I also made a tweet about it!! (https://x.com/kirancodes/status/1856699430227136525). Anyway, I've really fallen in love with Lean's metaprogramming facilities, they're so amazingly ergonomic and maintainable. This is fun!