argumentcomputer / lurk

Lurk is a Turing-complete programming language for zk-SNARKs. It is a statically scoped dialect of Lisp, influenced by Scheme and Common Lisp.
https://docs.argument.xyz
MIT License
46 stars 3 forks source link

feat: Add initial OCaml support #348

Closed wwared closed 3 weeks ago

wwared commented 1 month ago

This PR introduces OCaml support by extracting the lambda IR from the ocaml compiler, parsing it into a rust enum, then transforming it into an equivalent lurk program. Note that a lot of the behavior will change and this is still experimental and incomplete.

This adds two new meta commands: !(load-ocaml) which functions like !(load) and !(load-ocaml-expr) which functions like !(load-expr). The former will run the program and print its result, while the latter returns the transformed lurk program.

You can do things like !(load-ocaml "file.ml") !(debug) !(prove), !(debug !(load-ocaml-expr "file.ml")) or !(defq program !(load-ocaml-expr "file.ml")). The file must end in a .ml extension, and currently we only support compiling a single file.

Due to the way individual .ml files are compiled, for now you will want a program like let result = 123 rather than 123. Otherwise the 123 is evaluated inside a begin and its result is not used.

The pipeline works as follows:

The process for supporting a new primitive is roughly:

Currently we support:

Records, arrays, lists, tuples and etc will initially be represented by simple lists and accessed with nth. A record [0: 123 "abc"] becomes (list 0 123 "abc"), so a record is a list of its tag followed by its members.

It's possible the -dno-unique-ids option could lead to issues in certain programs, but for now we're using it by default. We might need to revisit this and use a different solution if we find a problematic program with this flag.

OCaml tests can be added inline or as files to src/lurk/tests/ml/ and a corresponding test_file! call in tests/eval_ocaml.rs.

Known issues/limitations: