Interest in contributions to expand IO builtins?

[shonfeder]

Hello! I love using elpi. Thanks for maintaining and continuing to evolve it!

I am working on a personal toy project and have occasion to considerably expand the builtins with bindings to ocaml functions form Filename, Sys, and Unix to expand its capabilities for OS interactions and file manipulations. The FFI extension mechanism is easy and works very well, so thanks for that!

To illustrate, at this point, I've just about a dozen declarations of this sort

    MLData (result (BuiltInData.poly "A") (BuiltInData.poly "B"));

    MLCode (Pred ("readdir",
      In  (BuiltInData.string, "DirPath",
      Out (result BuiltInData.(list string) BuiltInData.string, "Contents",
      Easy "get the contents of the directory at DirPath")),
      (fun path _ ~depth:_ ->
        try !: (Ok (Sys.readdir path |> Array.to_list))
        with Sys_error e -> !: (Error e))),
    DocAbove);

As I am accumulating this growing list of MLCode entries, it occurs to me it would be easy to contribute these back to the core elpi builtin.ml. Would you be interested in these contributions? (I can understand that you may well prefer not to bloat elpi with such features :) ).

[gares]

yes, please submit this code!

on the style side, I did not use result but rather the diagnostic type (in many rocq elpi APIs).
Eg coq.typecheck T Ty ok (success, assign Ty) and coq.typecheck T Ty (error Msg) does not assign Ty. And coq.typecheck T Ty D, if (D = error Msg) (print Msg) (print Ty) is also a possibility. The former became quickly an idiom, and if the builtin is coded properly you don't even need to generate the error message if the user calls it with ok (and the call fails). There are also a few combinators, like assert-ok! and co, that work with this "skema".

I don't know how weird this looks to you. But having both result and diagnostic would certainly look weirder IMO.

Another (debatable maybe) advantage is that by hoisting the datum out of the ok node, one can easily return multiple values (without the pairing, tripling,... construction) and have them documented separately. eg stat File Date Permissions More Diagnostic.