Landing the rust-interop features on master would have enormous benefits for the epfl-lara/rust-stainless project in terms of less maintenance for getting updates. This is under the condition that the features added/changed on the rust-interop branch can co-exist with the current master.
@samarion suggested the following changes to rust-interop before a potential merge:
[x] I would add an option optFormat which can be either “tip” or “binary”
[x] move deserializerMain into the Main object unless you need it in Stainless (and same for the optDeserialize option)
[x] Then I’d create a parsing method in the Main with return type (Program, Option[Expr]) (or maybe Symbols instead of Program, depending on the API of the TIP parser’s parseScript method)
[x] If the format option is “tip”, then call the current TIP parsing logic and return the resulting program and Some of the expression
[x] If the format option is “binary”, deserialize the input and check if there’s a boolean method with some pre-defined name in the program, e.g. check. Then return the deserialized program (minus the check method) and the check method’s body as the expression. If no such method exists in the program, return None for the Option[Expr].
[x] Then, if the returned option is Some, run solving on that expression.
[x] In addition, I would add a boolean option optPrintProgram which, if true, has Inox print the program (and potential expression) returned by either the “tip” or “binary” parser.
Landing the
rust-interopfeatures onmasterwould have enormous benefits for the epfl-lara/rust-stainless project in terms of less maintenance for getting updates. This is under the condition that the features added/changed on the rust-interop branch can co-exist with the current master.@samarion suggested the following changes to
rust-interopbefore a potential merge: