Parsing inductive data structures via FFI

Stream: lean4

[Leni Aniva]

Is there a way to parse inductive data structures (e.g. Expr objects) via the FFI?

For example if lean_object *obj is an Expr, how can I read which constructor produced it and read the arguments to that constructor?

[Abdalrhman M Mohamed]

lean_is_ctor and lean_ptr_tag are probably the functions you're looking for. I would recommend you follow the kernel's approach of defining an enum class for the datatype (e.g., expr_kind) and a function (e.g., expr::kind) that returns the enum directly.

[James Gallicchio]

honestly https://docs.rs/lean-sys/latest/lean_sys/ might be helpful if only for having generated docs :P

[Leni Aniva]

James Gallicchio said:

honestly https://docs.rs/lean-sys/latest/lean_sys/ might be helpful if only for having generated docs :P

I'm kind of skeptical about this project since it doesn't pin down the Lean version and also it doesn't really encapsulate the interface in lean.h. I find that bindgen is good enough for my purposes

[Mario Carneiro]

I have a project which does a higher level interface but it's a lot more work to design that

[Mario Carneiro]

it doesn't pin the lean version because this would cause rust versioning issues, but lean.h doesn't change much

[Mario Carneiro]

I'm not really sure how best to do versioning in lean-sys. The lean version pin should happen in the project using lean-sys

[Mario Carneiro]

updated to lean 4.6.0